|
|
Lehr- und Forschungsgebiet Informatik II | Fachgruppe Informatik |
|
|
Seminar: Verifikationsverfahren (S2, SS 2006) |
|
Prof. Dr. Jürgen Giesl, René Thiemann, Peter Schneider-Kamp
In diesem Seminar werden verschiedene Techniken und Verfahren zur Verifikation von Programmen vorgestellt.
Das Seminar wird als Blockseminar am 17. und 18. Juli veranstaltet. Die Vorbesprechung für das Seminar findet zu Beginn der Vorlesungszeit statt (April 2006); der genaue Termin wurde den Teilnehmern per E-Mail bekannt gegeben. Es gelten folgende Fristen:
Kenntnisse in Programmverifikation oder verwandten Gebieten (z.B. "Grundlagen der Funktionalen Programmierung", "Termersetzungssysteme", "Automatisierte Programmverifikation" oder Besuch der Vorlesung "Logikprogrammierung" in diesem Semester).
| Datum | Zeit | Thema | Betreuer | Referent |
|---|---|---|---|---|
| 17.07. | 09:30 | Reducing LPO to SAT | P. Schneider-Kamp | Christian Steffens |
| 17.07. | 10:30 | The DP-Framework | R. Thiemann | Patrick Stalljohann |
| 17.07. | 11:30 | Termination Proofs for a Lazy Functional Language | J. Giesl | Florian Witte |
| 17.07. | 13:30 | Termination Analysis for Logic Programs by Term Rewriting | J. Giesl | David Fürst |
| 17.07. | 14:30 | Liveness in Rewriting | P. Schneider-Kamp | Gabriel Martínez Magallón |
| 18.07. | 09:30 | SAT Solving for Theorem Proving | J. Giesl | Aleksandar Hitrov |
| 18.07. | 10:30 | Inductive Theorem Proving | J. Giesl | Christoph Lischkowitz |
| 18.07. | 11:30 | Verification of Protocols | R. Thiemann | Stefan Plücken |
| 18.07. | 13:30 | SAT Solving Algorithms | P. Schneider-Kamp | Philip Ritzkopf |
| 18.07. | 14:30 | LTL Model Checking | R. Thiemann | Jan Scherer |
| 18.07. | 15:30 | CTL Model Checking | P. Schneider-Kamp | Stephan Günnemann |
Alle Zeiten sind vorläufig.
Die Ausarbeitung sollte inkl. Deckblatt exakt 12 Seiten umfassen und der Vortrag etwa 40 Minuten dauern.
Theoretische Informatik, Informatik Vertiefung
|
 |