Relational Verification Through Horn Clause Transformation

We present a method for verifying relational program properties, that is, properties that relate the input and the output of two programs. Our verification method is parametric with respect to the definition of the operational semantics of the programming language in which the two programs are written. That definition of the semantics consists of a set Int of constrained Horn clauses (CHCs) that encode the interpreter of the programming language. Then, given the programs and the relational property we want to verify, we generate, by using Int, a set of constrained Horn clauses whose satisfiability is equivalent to the validity of the property. Unfortunately, state-of-the-art solvers for CHCs have severe limitations in proving the satisfiability, or the unsatisfiability, of such sets of clauses. We propose some transformation techniques that increase the power of CHC solvers when verifying relational properties. We show that these transformations, based on unfold/fold rules, preserve satisfiability. Through an experimental evaluation, we show that in many cases CHC solvers are able to prove the satisfiability (or the unsatisfiability) of sets of clauses obtained by applying the transformations we propose, whereas the same solvers are unable to perform those proofs when given as input the original, untransformed sets of CHCs.