Automating Regression Verification

Reviewed Paper In Proceedings

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.

BibTeX

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