We present a data-driven technique to solve Constrained Horn Clauses (CHCs) that encode verification conditions of programs containing unconstrained loops and recursions. Our CHC solver neither constrains the search space from which a predicate's components are inferred (e.g., by constraining the number of variables or the values of coefficients used to specify an invariant), nor fixes the shape of the predicate itself (e.g., by bounding the number and kind of logical connectives). Instead, our approach is based on a novel machine learning-inspired tool chain that synthesizes CHC solutions in terms of arbitrary Boolean combinations of unrestricted atomic predicates. A CEGAR-based verification loop inside the solver progressively samples representative positive and negative data from recursive CHCs, which is fed to the machine learning tool chain. Our solver is implemented as an LLVM pass in the SeaHorn verification framework and has been used to successfully verify a large number of nontrivial and challenging C programs from the literature and well-known benchmark suites (e.g., SV-COMP).
Fri 22 JunDisplayed time zone: Eastern Time (US & Canada) change
14:00 - 15:40 | |||
14:00 25mTalk | Active Learning of Points-To Specifications PLDI Research Papers Osbert Bastani Stanford University, Rahul Sharma Microsoft Research, Alex Aiken Stanford University, Percy Liang Stanford University Media Attached | ||
14:25 25mTalk | Pinpoint: Fast and Precise Sparse Value Flow Analysis for Million Lines of Code PLDI Research Papers Qingkai Shi Hong Kong University of Science and Technology, China, Xiao Xiao SourceBrella Inc., Rongxin Wu Department of Computer Science and Engineering, The Hong Kong University of Science and Technology, Jinguo Zhou Sourcebrella Inc., Gang Fan , Charles Zhang Media Attached | ||
14:50 25mTalk | A Data-Driven CHC Solver PLDI Research Papers Media Attached | ||
15:15 25mTalk | User-Guided Program Reasoning using Bayesian Inference PLDI Research Papers Mukund Raghothaman University of Pennsylvania, Sulekha Kulkarni Georgia Tech, Kihong Heo University of Pennsylvania, USA, Mayur Naik University of Pennsylvania Media Attached |