Skip to main content

Solving Constrained Horn Clauses Using Syntax and Data

Author(s): Fedyukovich, Grigory; Prabhu, Sumanth; Madhukar, Kumar; Gupta, Aarti

To refer to this page use:
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.
Publication Date: 2018
Citation: Fedyukovich, Grigory, Sumanth Prabhu, Kumar Madhukar, and Aarti Gupta. "Solving Constrained Horn Clauses Using Syntax and Data." In Formal Methods in Computer Aided Design (FMCAD) (2018): pp. 1-9. doi:10.23919/FMCAD.2018.8603011
DOI: 10.23919/FMCAD.2018.8603011
Pages: 1 - 9
Type of Material: Conference Article
Journal/Proceeding Title: Formal Methods in Computer Aided Design (FMCAD)
Version: Author's manuscript

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.