Solving Constrained Horn Clauses Using Syntax and Data

Grigory Fedyukovich, Sumanth Prabhu, Kumar Madhukar, Aarti Gupta

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

5 Scopus citations

Abstract

A Constrained Horn Clause (CHC) is a logical implication involving unknown predicates. Systems of CHCs are widely used to verify programs with arbitrary loop structures: interpretations of unknown predicates, which make every CHC in the system true, represent the program's inductive invariants. In order to find such solutions, we propose an algorithm based on Syntax-Guided Synthesis. For each unknown predicate, it generates a formal grammar from all relevant parts of the CHC system (i.e., using syntax). Grammars are further enriched by predicates and constants guessed from models of various unrollings of the CHC system (i.e., using data). We propose an iterative approach to guess and check candidates for multiple unknown predicates. At each iteration, only a candidate for one unknown predicate is sampled from its grammar, but then it gets propagated to candidates of the remaining unknowns through implications in the CHC system. Finally, an SMT solver is used to decide if the system of candidates contributes towards a solution or not. We present an evaluation of the algorithm on a range of benchmarks originating from program verification tasks and show that it is competitive with state-of-the-art in CHC solving.

Original languageEnglish (US)
Title of host publicationProceedings of the 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018
EditorsNikolaj Bjorner, Arie Gurfinkel
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages170-178
Number of pages9
ISBN (Electronic)9780983567882
DOIs
StatePublished - Jan 4 2019
Event18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018 - Austin, United States
Duration: Oct 30 2018Nov 2 2018

Publication series

NameProceedings of the 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018

Conference

Conference18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018
CountryUnited States
CityAustin
Period10/30/1811/2/18

All Science Journal Classification (ASJC) codes

  • Computer Graphics and Computer-Aided Design
  • Software

Fingerprint Dive into the research topics of 'Solving Constrained Horn Clauses Using Syntax and Data'. Together they form a unique fingerprint.

  • Cite this

    Fedyukovich, G., Prabhu, S., Madhukar, K., & Gupta, A. (2019). Solving Constrained Horn Clauses Using Syntax and Data. In N. Bjorner, & A. Gurfinkel (Eds.), Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018 (pp. 170-178). [8603011] (Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.23919/FMCAD.2018.8603011