IMPROVE
Regression Verification for Evolving Object-Oriented Software
The ProjectOne 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 CheckingRêve is a tool that automatically checks whether two C-like programs behave equally. You can try rêve online. The paper describing the method and the tool has appeared at ASE'2014. |
|
|
|
A Tool for Regression Verification of Programmable Logic Controller SoftwareWith 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 |
