Automating Regression Verification
Speaker
Mattias Ulbrich
, Karlsruhe Institute of Technology, Germany
Date and Time
Monday, September 15th, 2014 at 10:15.
Location
Polacksbacken, room 1245
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. 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.
Joint work with Dennis Felsing, Sarah Grebing, Vladimir Klebanov,
Philipp Ruemmer