Department of Information Technology

Automating Regression Verification


Mattias Ulbrich, Karlsruhe Institute of Technology, Germany

Date and Time

Monday, September 15th, 2014 at 10:15.


Polacksbacken, room 1245


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

Updated  2014-09-08 12:58:21 by Jari Stenman.