Einführung in Methoden zum Nachweis der Korrektheit von sequentiellen, parallelen und verteilten Programmen.

Fachkompetenzen
Die Studierenden:

• beschreiben operationelle Semantiken von sequentiellen, parallelen und verteilten 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 der Interferenz- und Deadlock-Freiheit paralleler Programme
• transformieren parallele und verteilte Programme in nichtdeterministische Programme

Methodenkompetenzen
Die Studierenden:

• erkennen Korrektheit als einen wichtigen Aspekt von Programmen und Informatik-Systemen

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 mit neueren Techniken der Programmtransformation kombiniert. Als Vorbereitung werden zunächst sequentielle Programme behandelt.

Am Ende des Semesters

Klausur oder mündliche Prüfung