Lehr- und Forschungsgebiet Informatik II | Fachgruppe Informatik |
Seminar: Verifikationsverfahren (S2, WS 2002/2003) |
Prof. Dr. Jürgen Giesl, Darius Dlugosz, René Thiemann
Das Seminar wird als Blockseminar am Ende der Vorlesungszeit (Februar 2003) veranstaltet. Die Vorbesprechung für das Seminar findet am Freitag, dem 25. 10. 2002, um 11:45-13.15 im AH I statt.
Interessenten melden sich bitte bei Prof. Dr. Jürgen Giesl ( giesl@informatik.rwth-aachen.de, Tel: 80-21230).
Kenntnisse in Programmverifikation oder verwandten Gebieten (z.B. "Termersetzungssysteme", "Automatisierte Programmverifikation" oder Besuch der Vorlesung "Grundlagen der Funktionalen Programmierung" in diesem Semester).
Wird bei der Vorbesprechung bekannt gegeben und verteilt.
In diesem Seminar werden verschiedene Techniken und Verfahren zur Verifikation von Programmen vorgestellt. Im einzelnen werden folgende Themen behandelt:
Zeit | Datum | Thema | Referent(in) |
---|---|---|---|
9:30 | Mo., 17.2. | Terminierungsanalyse von Termersetzungssystemen mit Dependency Pairs | Stephan Palm |
10:45 | Mo., 17.2. | Terminierungsanalyse von Higher-Order Termersetzungssystemen | Diego Biurrun |
12:00 | Mo., 17.2. | Terminierungsanalyse von funktionalen Programmen mit Lazy Evaluation | Frank Peiffer |
14:00 | Mo., 17.2. | Terminierungsanalyse von funktionalen Programmen durch Size-Change Graphen | Michael Sauren |
15:15 | Mo., 17.2. | Terminierungsanalyse von logischen Programmen | Niklas Mausberg |
9:30 | Di., 18.2. | Explizite Induktionsbeweisverfahren | Barbara Friemann |
10:45 | Di., 18.2. | Implizite Induktionsbeweisverfahren | Salaheddine Benyassine |
12:00 | Di., 18.2. | Induktionsverfahren zur Protokollverifikation | Christof Skrzypczyk |
14:00 | Di., 18.2. | Protokollverifikation mit Termersetzungstechniken | Thomas Schoenemann |
15:15 | Di., 18.2. | Verifikation von logischen Programmen | Nils Wilhelms |
16:30 | Di., 18.2. | Proof-Carrying Code | Ingo Zander |
Theoretische Informatik, Informatik Vertiefung
|