Lehr- und Forschungsgebiet Informatik II

Fachgruppe Informatik

Seminar: Verifikation von Programmen (S2, SS 2003)

Veranstalter

Prof. Dr. Jürgen Giesl, René Thiemann, Darius Dlugosz

Voraussetzungen

Kenntnisse in Programmverifikation oder verwandten Gebieten (z.B. "Termersetzungssysteme", "Grundlagen der Funktionalen Programmierung" und insbesondere Besuch der Vorlesung "Automatisierte Programmverifikation" in diesem Semester).

Inhalt

Um die Zuverlässigkeit und Korrektheit von Programmen (oder auch von Schaltungen) zu garantieren, wird eine formale Verifikation benötigt. Die Durchführung eines mathematischen Korrektheitsbeweises ist jedoch im allgemeinen sehr aufwendig - insbesondere bei umfangreichen Algorithmen, wie sie in der Praxis eingesetzt werden. Aus diesem Grund wird versucht, die Aufgabe der Programmverifikation weitgehend zu automatisieren. In dem Seminar werden verschiedene Techniken und Systeme vorgestellt, um Korrektheitseigenschaften von Programmen rechnergestützt zu untersuchen. Das erste Teilseminar beschäftigt sich mit der automatisierten Terminierungsanalyse. Die behandelten Programme und Verfahren des zweiten Seminars beruhen überwiegend auf Model Checking und Induktionsbeweisen.

Termine

Die Seminare werden als Blockseminar am 28. Juli und am 1. August 2003 im Seminarraum des Lehrstuhls (Raum 4201b) veranstaltet. Es gelten die folgenden Fristen:

• 6. 6.: Literatur abholen
• 23. 6.: Besprechung der Konzeption
• 7. 7.: Abgabe der Ausarbeitung
• 21. 7.: Kopien der überarbeiteten Ausarbeitung anfertigen

Verifikation von Programmen: Terminierung (28.7.)

Verifikation von Programmen: Model Checking, partielle Korrektheit und Beweisen mit Induktion (1.8.)

Zuordnung

Theoretische Informatik, Informatik Vertiefung

Last modified: Thu Jul 24 11:05:58 CEST 2003 / Lehr- und Forschungsgebiet Informatik II