Transforming Constrained Horn Clauses for Program Verification

Maurizio Proietti (IASI-CNR, Italy)

Constrained Horn Clauses (CHCs) have been advocated as a lingua franca for verifying program correctness, and a number of solvers for proving the satisfiability of such clauses have been recently developed. However, solving CHC satisfiability problems is a very hard (undecidable, in general) task, and the effectiveness of solvers depends very much on the syntactic form of the clauses. For this reason, recent work has suggested that transformation techniques that change the form of the clauses while preserving their satisfiability may be used to alleviate this problem.

In this talk we present recent and ongoing research on transformation techniques for CHCs that can be used to ease satisfiability proofs, and hence program verification. We first present a very general approach based on transformation rules such as unfolding, folding and constraint rewriting. Then we present the clause specialization and predicate tupling techniques that make use of these rules to improve the effectiveness of CHC solving. Clause specialization can be used for simplifying CHCs by exploiting information about the specific property to be verified and the semantics of the programming language. Predicate tupling consists in deriving new predicates that are equivalent to conjunctions of predicates occurring in a given set of CHCs to be solved. We show that predicate tupling is able to strictly improve the effectiveness of CHC solvers. Indeed, we consider CHC solvers based on Linear Arithmetic (LA-solvers) and we show that there are examples of CHCs that are satisfiable, and yet they cannot be solved by any LA-solver. Then we show that, by predicate tupling, we are able to transform the given CHCs into a new form that can be proved satisfiable by an LA-solver. Finally, we present some applications where complex program properties can be proved by transforming their specifications, using clause specialization and predicate tupling, into CHCs that can be solved by LA-solvers.

On Predicate Refinement Heuristics in Program Verification with CEGAR

Tachio Terauchi (Japan Advanced Institute of Science and Technology)

Many of the modern program verifiers are based on the predicate abstraction with CEGAR method, The method looks for a sufficient inductive invariant to prove the given property of the given program by iteratively accumulating predicates that are obtained by analyzing spurious counterexamples, and predicate refinement heuristics like Craig interpolation are used for this purpose. In this talk, we overview our recent work on predicate refinement heuristics in CEGAR. Specifically, we show that a certain strategy for choosing predicates can guarantee the convergence of CEGAR at a modest cost. We also show that choosing small refinements guarantees fast convergence under certain conditions.