Automated Verification of Relational Program Properties

We present a method for verifying relational program prop- erties, 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 semantics of the programming language in which the programs are written. That definition consists of a set Int of constrained Horn clauses (CHC) 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. Unfortu- nately, state-of-the-art solvers for CHC have severe limitations in proving the satisfiability, or the unsatisfiability, of such sets of clauses. We pro- pose some transformation techniques that increase the power of CHC solvers when verifying relational properties. We show that these trans- formations, based on unfolding and folding rules, preserve satisfiability. Through an experimental evaluation we show that in many cases CHC solvers are able to prove the (un)satisfiability 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 sets of constrained Horn clauses.