Automating Regression Verification of Pointer Programs by Predicate Abstraction

Journal Article

Author(s):Vladimir Klebanov, Philipp Rümmer, and Mattias Ulbrich
Journal:Formal Methods in System Design
Publisher:Springer
Number:3
Volume:52
Year:2018
Pages:229-259
DOI:10.1007/s10703-017-0293-8
Links:

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}
}