Constrained resolution advances program verification with symbolic execution
Symbolic Execution of Constrained Horn Clauses
Logic in Computer ScienceProgramming Languages
Summary
Verifying computer programs to ensure they behave correctly is a complex task. The authors study a method called constrained resolution, which uses logical rules to check if certain conditions hold true in program models. They show that forward and backward symbolic execution, techniques to simulate program behavior, fit into this framework and prove that their approach is complete and can efficiently avoid redundant checks. Their work helps improve verification tools and includes tests on benchmark problems.
What this means in practice
- •For software verification engineers: Verify program correctness by applying enhanced logical reasoning techniques to efficiently handle both linear and complex program properties.
- •For compiler tool developers: Incorporate advanced constrained resolution methods to improve intermediate program analysis and error detection during compilation.
Authors
Johannes Weiser, Zafer Esen, Philipp Rümmer
Abstract
Constrained Horn clauses (CHCs) are a fragment of first-order logic widely used as an intermediate language for verification. We study constrained resolution as a calculus for reasoning about the satisfiability of sets of CHCs. Constrained resolution forms a simple alternative to model checking algorithms such as CEGAR and IC3 and is here shown to exhibit complementary features. We show that, when CHCs encode programs, forward symbolic execution corresponds to positive unit hyper-resolution, and backward symbolic execution to SLD resolution, which are special cases of constrained resolution. We formalize forward and backward reasoning for linear and non-linear CHCs and transition systems, prove refutational completeness under fair strategies, and develop subsumption criteria for pruning redundant derivations. We moreover show that backward resolution with subsumption generalizes $k$-induction to non-linear CHCs, and that forward constrained resolution is related to the problem of constructing proofs in incorrectness logic. Lastly, we provide an experimental evaluation in the Eldarica CHC solver on benchmarks from CHC-COMP.