@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} }
Automating Regression Verification of Pointer Programs by Predicate Abstraction
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: | Preprint The final publication is available at Springer |
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.