Automating Regression Verification of Pointer Programs by Predicate Abstraction

Abstract

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.

BibTeX

@Article{KlebanovRuemmerUlbrich2017,
  title        = {Automating Regression Verification of Pointer
                  Programs by Predicate Abstraction},
  author       = {Vladimir Klebanov and Philipp R{\"u}mmer and Mattias Ulbrich},
  publisher    = {Springer},
  journal      = {Formal Methods in System Design},
  year         = {2018},
  month        = jun,
  volume       = 52,
  number       = 3,
  pages        = {229--259},
  issn         = {1572-8102},
  doi          = {10.1007/s10703-017-0293-8}
}