inf407 - Programmverifikation (Vollständige Modulbeschreibung)

Einführung in Methoden zum Nachweis der Korrektheit von sequentiellen und parallelen Programmen.
Fachkompetenzen
Die Studierenden:

• beschreiben operationelle Semantiken von sequentiellen und parallelen Programmen 
• kennen die Konzepte der partiellen und totalen Programmkorrektheit
• zeigen die Korrektheit und Vollständigkeit von Beweissystemen
• stellen Ein-Ausgabe-Spezifikationen von Programmen auf
• führen Korrektheitsbeweise für Programme verschiedener Klassen mit Hilfe von Beweisregeln durch
• überprüfen die Interferenz- und Deadlock-Freiheit paralleler Programme
• führen Korrektheitsbeweise für parallele Programme auf schwachen Speichermodellen durch 

Methodenkompetenzen
Die Studierenden:

• erkennen Korrektheit als einen wichtigen Aspekt von Programmen und Informatik-Systemen
• beherrschen Kalküle als Mittel der Spezifikation und Verifikation

Sozialkompetenzen

Die Studierenden:

• arbeiten in kleinen Gruppen an Lösungen von Aufgaben
• präsentieren Lösungen von Aufgaben vor Gruppen 

Selbstkompetenzen
Die Studierenden:

• erlernen Ausdauer bei der Bearbeitung schwieriger Aufgaben
• erlernen Präzision bei der Spezifikation von Problemen      

Programmverifikation ist ein systematischer Ansatz, die Fehlerfreiheit von Programmen zu zeigen. Dazu wird bewiesen, dass ein vorgegebenes Programm bestimmte wünschenswerte Verhaltenseigenschaften besitzt. Beispielsweise sollte ein Sortierprogramm nur sortierte Felder als Ergebnis abliefern. Bei sequentiellen Programmen geht es dabei vor allem um partielle Korrektheit, Terminierung und Abwesenheit von Laufzeitfehlern. Bei parallelen Programmen sind zusätzliche Verhaltenseigenschaften wichtig: Interferenz-Freiheit, Deadlock-Freiheit und faires Ablaufverhalten. In der Vorlesung geht es vornehmlich um die Verifikation paralleler Programme. Dazu werden klassische Methoden der Hoareschen Logik und ihre Erweiterung für parallele Programme, insbesondere auch für schwache Speichermodelle, studiert. Als Vorbereitung werden zunächst sequentielle Programme behandelt.

Essentiell:

• "K.R. Apt, E.-R. Olderog, Programmverifikation, Springer-Verlag, 1994''

Oder die erweiterte englische Version:

• "K.R. Apt, F.S. de Boer, E.-R. Olderog, Verfication of Sequential and Concurrent Programs, Third Edition, Springer-Verlag, 2008''

Am Ende des Semesters

Klausur oder mündliche Prüfung