Hauptseite von "Praxis der Forschung"

Sommersemester 2013 und Wintersemester 2013/14

Projektgruppe Regression Verification

Prof. Dr. Bernhard Beckert
Dr. Vladimir Klebanov
Sarah Grebing

Typ: Projektgruppe
Ort: Raum 211, Geb. 50.34
Zeit: n.V.
LV-Nr.: 2400066

Bekanntmachungen:

  • 23.03.2013: Die Informationsveranstaltung zur Projektgruppe findet um 12.45 Uhr in SR 301 (Gebäude 50.34) statt.


Ziel des Projekts ist es ein Werkzeug für eine einfache imperative Zielsprache zu entwickeln, mit dem es möglich ist Techniken der "Regression Verification" anzuwenden.

Regression Verification ist ein neuer Ansatz, mit dem sichergestellt wird, dass beim Änderungsgprozesses keine neuen Fehler in die Software einfließen.


Regression Verification vereint Ideen und Vorteile des Regression Testings mit der deduktiven Verifikation. Regression Testing ist die erfolgreichste Methode zum Finden von Fehlern in evolvierender Software. Die deduktive Verifikation ist eine etablierte Methode, um formal-logisch zu beweisen, das ein Programm bestimmte spezifizierte Eigenschaften erfüllt.

Bisher musste der Benutzer die Eigenschaften der Software spezifizieren und diese konnten dann mit der Hilfe eines Beweisers bewiesen werden. Bei der Regression Verification muss die Spezifikation nicht mehr vorhanden sein, da die funktionale Äquivalenz zweier Programme bewiesen wird -- so dient das Verhalten der originalen Version der Software als Spezifikation für die modifizierte Version der Software.


Für die Bearbeitung des Themas der Projektgruppe müssen sich die Teilnehmer des Projekts im Bereich der Regression Verification über den Stand der Technik informieren, eine Zielsprache entwickeln und die bestehende Methoden für diese Zielsprache adaptieren.


Regression Verifikation ist auch Thema eines aktuellen Projektes (IMPROVE) in der Arbeitsgruppe, in welchem eine Methode zur Regression Verification für die Programmiersprache Java entwickelt werden soll.


Bei Interesse bitte per E-Mail bei grebingFbp1∂mail informatik kit edu melden



Copyright and Licence of the Picture
This picture is a modified version of human_evolution.svg by Tkgd2007 [CC-BY-SA-3.0 or GFDL], via Wikimedia Commons.