Fri 22 Jun 2018 14:50 - 15:15 at Grand Ballroom CD - Program Analysis Chair(s): Isil Dillig

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 Jun
Times are displayed in time zone: Eastern Time (US & Canada) change

14:00 - 15:40
Program AnalysisPLDI Research Papers at Grand Ballroom CD
Chair(s): Isil DilligUT Austin
14:00
25m
Talk
Active Learning of Points-To Specifications
PLDI Research Papers
Osbert BastaniStanford University, Rahul SharmaMicrosoft Research, Alex AikenStanford University, Percy LiangStanford University
Media Attached
14:25
25m
Talk
Pinpoint: Fast and Precise Sparse Value Flow Analysis for Million Lines of Code
PLDI Research Papers
Qingkai ShiHong Kong University of Science and Technology, China, Xiao XiaoSourceBrella Inc., Rongxin WuDepartment of Computer Science and Engineering, The Hong Kong University of Science and Technology, Jinguo ZhouSourcebrella Inc., Gang Fan, Charles Zhang
Media Attached
14:50
25m
Talk
A Data-Driven CHC Solver
PLDI Research Papers
He ZhuRutgers University, USA, Stephen Magill, Suresh JagannathanPurdue University
Media Attached
15:15
25m
Talk
User-Guided Program Reasoning using Bayesian Inference
PLDI Research Papers
Mukund RaghotamanUniversity of Pennsylvania, Sulekha KulkarniGeorgia Tech, Kihong HeoUniversity of Pennsylvania, USA, Mayur NaikUniversity of Pennsylvania
Media Attached