Home  |  deutsch  |  Legals  |  Data Protection  |  Sitemap  |  KIT

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
DOI:10.1145/2642937.2642987
Keywords: formal methods invariant generation program equivalence regression verification IMPROVE
Links:

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