Regression verification is an approach complementing regression
testing with formal verification. The goal is to formally prove that
two versions of a program behave either equally or differently in a
precisely specified way. In this paper, we present a novel automated
approach for regression verification that reduces the equivalence of
two related imperative pointer programs to constrained Horn clauses
over uninterpreted predicates. Subsequently, state-of-the-art SMT
solvers are used to solve the clauses. We have implemented the
approach, and our experiments show that non-trivial programs with
integer and pointer arithmetic can now be proved equivalent without
further user input.