TY - GEN

T1 - Solving Constrained Horn Clauses Using Syntax and Data

AU - Fedyukovich, Grigory

AU - Prabhu, Sumanth

AU - Madhukar, Kumar

AU - Gupta, Aarti

PY - 2019/1/4

Y1 - 2019/1/4

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

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

UR - http://www.scopus.com/inward/record.url?scp=85061638765&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85061638765&partnerID=8YFLogxK

U2 - 10.23919/FMCAD.2018.8603011

DO - 10.23919/FMCAD.2018.8603011

M3 - Conference contribution

AN - SCOPUS:85061638765

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

SP - 170

EP - 178

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

A2 - Bjorner, Nikolaj

A2 - Gurfinkel, Arie

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 18th Conference on Formal Methods in Computer-Aided Design, FMCAD 2018

Y2 - 30 October 2018 through 2 November 2018

ER -