Automating Regression Verification

Begutachtete Veröffentlichung in Tagungsband

Autor(en):Dennis Felsing, Sarah Grebing, Vladimir Klebanov, Philipp Rümmer und Mattias Ulbrich
In:29th IEEE/ACM International Conference on Automated Software Engineering (ASE 2014)
Verleger:ACM
Reihe:ASE '14
Jahr:2014
Seiten:349-360
Preprint/PDF:ase2014.pdf
DOI:10.1145/2642937.2642987
Stichworte: 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}
}