Lehr- und Forschungsgebiet Informatik II | Fachgruppe Informatik |
Seminar: Verifikationsverfahren (S2, SS 2005) |
Prof. Dr. Jürgen Giesl, RenĂ© Thiemann, Peter Schneider-Kamp
Das Seminar wird am 1. und 2. August 2005 im Raum 4201b (Seminarraum des Lehrstuhls) als Blockseminar veranstaltet. Es gelten folgende Fristen:
13.5.: | Literatur abholen |
17.6.: | Konzeption absprechen |
15.7.: | Erste Version der vollständigen Ausarbeitung abgeben |
Kenntnisse in Programmverifikation oder verwandten Gebieten (z.B. "Termersetzungssysteme", "Automatisierte Programmverifikation" oder Besuch der Vorlesung "Grundlagen der Funktionalen Programmierung" in diesem Semester).
Zeit | Thema | Referent | Betreuer |
---|---|---|---|
Mo., 09:45 - 10:45 | Model Checking und Automaten | Michaela Slaats | Peter Schneider-Kamp |
Mo., 11:00 - 12:00 | Model Checking und BDDs | Andreas Röll | Peter Schneider-Kamp |
Mo., 12:15 - 13:15 | Software Model Checking durch Abstraktion | Markus Engelberth | Peter Schneider-Kamp |
Mo., 14:15 - 15:15 | Model Checking durch SAT-Algorithmen | Philipp Brauner | Peter Schneider-Kamp |
Mo., 15:30 - 16:30 | Theorem Proving durch SAT-Algorithmen | Philipp Trinius | Jürgen Giesl |
Mo., 16:45 - 17:45 | Explizite Induktion | David Thesing | René Thiemann |
Mo., 18:00 - 19:00 | Higher-Order Theorem Proving (mit Isabelle) | Marek Jawurek | René Thiemann |
Di., 09:00 - 10:00 | Protokollverifikation | Marion Beckers | René Thiemann |
Di., 10:15 - 11:15 | Terminierung von TES: Dependency Pair Framework | Matthias Baetzold | Jürgen Giesl |
Di., 11:30 - 12:30 | (Nicht-) Termininierung von Funktionen höherer Ordnung | Youness Harrak | Jürgen Giesl |
Di., 13:30 - 14:30 | Polynomordnungen | Nicolas Becker | René Thiemann |
Di., 14:45 - 15:45 | Query-Mapping Pairs | Sven Lilienthal | Peter Schneider-Kamp |
Di., 16:00 - 17:00 | Terminierungsanalyse imperativer Programme | Christian Lücking | Jürgen Giesl |
Alle Zeiten sind vorläufig.
Die Ausarbeitung sollte circa 15 Seiten umfassen und der Vortrag etwa 50 Minuten dauern.
Theoretische Informatik, Informatik Vertiefung
|