Home  |  Impressum  |  Datenschutz  |  Sitemap  |  KIT

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

Bekanntmachungen:

  • 16.12.2012: Update der Begleitveranstaltungen
  • 15.11.2012: Folien der Grundlagenveranstaltungen sind jetzt online
  • 13.11.2012: Update der Begleitveranstaltungen
  • 09.11.2012: Zeitplan für die Literaturrechereche und das Seminar online
  • 18.10.2012: Termin der Informationsveranstaltung, 13:15 - 14:00 Uhr in Raum -102 (Gebäude 50.34)
  • 28.09.2012: Webseite online


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∂ira uka de 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.