Regression Verification for Evolving Object-Oriented Software
One of the main concerns during software evolution is to prevent the introduction of unwanted behavior, commonly known as regressions, when implementing new features, fixing defects, or during optimization. Undetected regressions can have severe consequences and incur high cost, in particular in late stages of development, or in software that is already deployed.
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.
The project is led by Prof. Bernhard Beckert and Dr. Vladimir Klebanov. It is part of the DFG Priority Programme 1593 "Design for Future – Managed Software Evolution".
An Automated Tool for Regression Verification / Equivalence Checking
A Tool for Regression Verification of Programmable Logic Controller Software
With ReveForPLC we prove the equivalence between two sofware revision of control system for plants. ReveForPLC provides the transformation from Structured Text and Sequential Function Charts into SMV models. More information