Transforming Constrained Horn Clauses for Program Verification

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.