@inproceedings{FelsingGrebingKlebanov2014, author = {Dennis Felsing and Sarah Grebing and Vladimir Klebanov and Philipp R\"{u}mmer and Mattias Ulbrich}, title = {Automating Regression Verification}, booktitle = {29th IEEE/ACM International Conference on Automated Software Engineering (ASE 2014)}, series = {ASE '14}, month = sep, year = {2014}, pages = {349--360}, numpages = {12}, doi = {10.1145/2642937.2642987}, acmid = {2642987}, publisher = {ACM}, keywords = {formal methods, invariant generation, program equivalence, regression verification, IMPROVE} }
Automating Regression Verification
Author(s): | Dennis Felsing, Sarah Grebing, Vladimir Klebanov, Philipp Rümmer, and Mattias Ulbrich |
---|---|
In: | 29th IEEE/ACM International Conference on Automated Software Engineering (ASE 2014) |
Publisher: | ACM |
Series: | ASE '14 |
Year: | 2014 |
Pages: | 349-360 |
Preprint/PDF: | ase2014.pdf |
DOI: | 10.1145/2642937.2642987 |
Keywords: | formal methods invariant generation program equivalence regression verification IMPROVE |
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 automatic approach for regression verification that reduces the equivalence of two related imperative integer programs to Horn constraints over uninterpreted predicates. Subsequently, state-of-the-art SMT solvers are used to solve the constraints. We have implemented the approach, and our experiments show non-trivial integer programs that can now be proved equivalent without further user input.