A data-driven CHC solver

He Zhu, Stephen Magill, Suresh Jagannathan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

11 Scopus citations

Abstract

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).

Original languageEnglish (US)
Title of host publicationPLDI 2018 - Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation
EditorsJeffrey S. Foster, Dan Grossman
PublisherAssociation for Computing Machinery
Pages707-721
Number of pages15
ISBN (Electronic)9781450356985
DOIs
StatePublished - Jun 11 2018
Externally publishedYes
Event39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018 - Philadelphia, United States
Duration: Jun 18 2018Jun 22 2018

Publication series

NameProceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)

Conference

Conference39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018
CountryUnited States
CityPhiladelphia
Period6/18/186/22/18

All Science Journal Classification (ASJC) codes

  • Software

Keywords

  • Constrained horn clauses (CHCs)
  • Data-driven analysis
  • Invariant inference
  • Program verification

Fingerprint Dive into the research topics of 'A data-driven CHC solver'. Together they form a unique fingerprint.

Cite this