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,