kirancodes.me
To Proof Maintenance & Beyond!
ASE 2014

Automating regression verification

Dennis Felsing, Sarah Grebing, Vladimir Klebanov, Philipp Rümmer, Mattias Ulbrich

PDFDOI 10.1145/2642937.2642987dblp

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{Felsing-al:ASE14,
  author    = {Dennis Felsing and
               Sarah Grebing and
               Vladimir Klebanov and
               Philipp R{\"{u}}mmer and
               Mattias Ulbrich},
  title     = {Automating regression verification},
  booktitle = {ASE},
  pages     = {349--360},
  publisher = {{ACM}},
  year      = {2014},
}

Related papers