This page in English  Lehr- und Forschungsgebiet Informatik II  Fachgruppe Informatik RWTH

Seminar: Verifikation von Programmen

(S2, SS 2003)

LuFG Informatik II


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:

Verifikation von Programmen: Terminierung (28.7.)

ZeitThemaReferentBetreuer
10:15-11:15Knuth Bendix OrdnungMarius ScholtenRené Thiemann
11:30-12:30Dependency PairsAlexander AchterfeldJürgen Giesl
13:30-14:30Size-Change TerminationHenning KielRené Thiemann
14:45-15:45Monotone semantische PfadordnungKathrin GeilmannRené Thiemann
16:00-17:00Terminierungsanalyse von funktionalen Programmen mit Lazy EvaluationJoachim WielandRené Thiemann
17:15-18:15Terminierungsanalyse für MercuryHeike HaegertRené Thiemann

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

ZeitThemaReferentBetreuer
9:00-10:00Temporale Logik und Model CheckingSandra CüstersBenedikt Bollig
10:15-11:15Model Checking und Automaten, SPINPatrick WieheBenedikt Bollig
11:30-12:30Implizite Induktion, SPIKENina BeckmannDarius Dlugosz
13:30-14:30Induktionsverfahren zur ProtokollverifikationXin LiuJürgen Giesl
14:45-15:45PVSIlja BezrukovDarius Dlugosz
16:00-17:00Extended Static CheckingGego KuriakoseDarius Dlugosz
17:15-18:15Kollaborative Editier SystemeTobias HülsdauDarius Dlugosz

Zuordnung

Theoretische Informatik, Informatik Vertiefung



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