@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.