Wintersemester 2012/13

Projektgruppe Regression Verification

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

Typ:	Projektgruppe
Ort:	Raum 211
Zeit:	Montag, 14.00 - 15.30 Uhr Donnerstag, 15.45 - 17.15 Uhr

---

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 sicher gestellt 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.

Zeitplan für die Literaturrechereche und das Seminar

Zeitpunkt	Termin	Hinweise
12.11.2012	Erste Idee der Gliederung	Für Feedback
19.11.2012	Gliederung	Diese Version möglichst nicht mehr verändern
26.11.2012	Zwischenversion der Folien	Für Feedback
03.12.2012	Fertige Folien
10.12.2012	Vortrag
16.12.2012	Gliederung und Draft der Ausarbeitung	Für Feedback
10.01.2013	Ausarbeitung

Begleitveranstaltungen

Zeitpunkt	Termin	Hinweise/Folien
08.11.2012	Metavortrag zu (Seminar-) vorträgen: Foliengestaltung	Fr. Mattern (ETH Zürich): Seminarvortrag - Hinweise zur Präsentation
12.11.2012	Gliederung eines Vortrags und schriftliche Ausarbeitung	Folien von Fr. Mattern (ETH Zürich), A. Zeller: Der perfekte Seminarvortrag
15.11.2012	Grundlagen: Prädikatenlogik + Einführung Dynamische Logik	Folien PL, Folien DL
19.11.2012	Grundlagen: Dynamische Logik	Folien
03.12.2012	Metavortrag zu (Seminar-) vorträgen: Vortragen	Folien von Fr. Mattern (ETH Zürich)
06.12.2012	Ausarbeitungen schreiben
10.12.2012	Vortrag (Seminar)

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.