Seminar: Verifikationsverfahren
(S2, WS 2014/15)
|
|
Veranstalter
Prof. Dr. Jürgen Giesl,
Cornelius Aschermann,
Florian Frohn,
Jera Hensel,
Thomas Ströder
Inhalt
In diesem Seminar werden verschiedene Techniken und Verfahren zur
Verifikation von Programmen vorgestellt.
Termine
Das Seminar wird als Blockseminar am Ende der Vorlesungszeit
durchgeführt. Der genaue Zeitpunkt wird über eine doodle Umfrage ermittelt und dann veröffentlicht.
Es gelten folgende Fristen:
- 31.10.2014: Literatur abholen
- 30.11.2014: Inhalt der Literatur verstanden haben und Konzeption absprechen
- 28.12.2014: Vollständige Ausarbeitung (10 Seiten inkl. Titel und Literaturverzeichnis) abgeben
- 19/20.02.2015: Tag des Seminars. Hierzu sollen
Sie die korrigierte Ausarbeitung in ausreichender Anzahl kopiert mitbringen;
die Kopien können am Lehr- und Forschungsgebiet angefertigt werden. Zwei Tage vorher sollten digitale Versionen an Cornelius Aschermann gemailt werden.
Vorgaben
Die Ausarbeitung darf nicht mehr als 10 Seiten inklusive
Titel und Literaturverzeichnis umfassen.
Bei diesem Umfang sind weder ein Index noch ein
Inhaltsverzeichnis erwünscht, allerdings sollte
ein Literaturverzeichnis vorhanden sein. Sollte die Ausarbeitung mehr als
fünf Rechtschreib- oder Grammatikfehler auf einer Seite oder mehr als
zehn insgesamt enthalten, wird die Bearbeitung abgebrochen.
Voraussetzungen
Kenntnisse in Programmverifikation oder verwandten Gebieten
(z.B. "Funktionale Programmierung", "Logikprogrammierung",
"Termersetzungssysteme", etc.).
Themen
| Datum | Zeit | Ort | Thema | Betreuer | Referent(in) |
|---|
| 19.02. | 09:00-09:45 | 4201b | Safety by Interpolation | T. Ströder | Spinrath, Christopher |
| 19.02. | 09:45-10:30 | 4201b | Heap Representation with Separation Logic | C. Aschermann | Kehler, Thibaud |
| 19.02. | 10:30-11:15 | 4201b | Abstract Regular Tree Model Checking | F. Frohn | Janson, Tom |
| 19.02. | 11:15-12:00 | 4201b | Forest Automata for Verification of Heap Manipulation | F. Frohn | Lekane Nimpa, Junior |
| 19.02. | 13:30-14:15 | 4201b | Liquid Types | C. Aschermann | Beaumont, Michael |
| 19.02. | 14:15-15:00 | 4201b | Finding Hard Bugs in C with Bounded Model Checking | C. Aschermann | Anwer, Meshkatul |
| 20.02. | 09:00-09:45 | 4201b | Deciding Bitvector Arithmetic with Abstraction | J. Hensel | Krueger, Andreas |
| 20.02. | 09:45-10:30 | 4201b | Termination Analysis using Bitvector Arithmetic | J. Hensel | Henn, Thomas |
| 20.02. | 10:30-11:15 | 4201b | Proving Termination of Imperative Programs Using MAX-SMT | J. Giesl | Karoff, Johannes |
| 20.02. | 11:15-11:30 | 4201b | AProVE Demo | | LuFG i2 Team |
| 20.02. | 11:30-12:15 | 4201b | Termination Analysis for Concurrent Programs | J. Giesl | Strothmann, Thies Yannik |
| 20.02. | 12:15-13:00 | 4201b | Complexity Analysis for Integer Programs | J. Giesl | Kielmann, Sabrina |
Die Vortragsdauer beträgt jeweils 25 Minuten.
Zuordnung
Theoretische Informatik
Rückfragen
Bitte wenden Sie sich an
Cornelius Aschermann.
