inf407 - Programmverifikation (Vollständige Modulbeschreibung)

inf407 - Programmverifikation (Vollständige Modulbeschreibung)

Originalfassung Englisch PDF Download
Modulbezeichnung Programmverifikation
Modulkürzel inf407
Kreditpunkte 6.0 KP
Workload 180 h
Einrichtungsverzeichnis Department für Informatik
Verwendbarkeit des Moduls
  • Fach-Bachelor Informatik (Bachelor) > Akzentsetzungsbereich - Wahlbereich Informatik
  • Master of Education (Gymnasium) Informatik (Master of Education) > Wahlpflichtmodule (Theoretische Informatik)
  • Zwei-Fächer-Bachelor Informatik (Bachelor) > Wahlpflicht Theoretische Informatik (30 KP)
Zuständige Personen
  • Wehrheim, Heike (Modulverantwortung)
  • Olderog, Ernst-Rüdiger (Modulverantwortung)
  • Lehrenden, Die im Modul (Prüfungsberechtigt)
Teilnahmevoraussetzungen
Theoretische Informatik I und II
Kompetenzziele
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      
Modulinhalte
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.
Literaturempfehlungen
Essentiel:
  • "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''
Links
Unterrichtssprache Deutsch
Dauer in Semestern 1 Semester
Angebotsrhythmus Modul Wintersemester
Aufnahmekapazität Modul unbegrenzt
Lehr-/Lernform 1VL + 1Ü
Vorkenntnisse Theoretische Informatik I und II
Lehrveranstaltungsform Kommentar SWS Angebotsrhythmus Workload Präsenz
Vorlesung 3 siehe Angebotsrhythmus Modul 42
Übung 1 siehe Angebotsrhythmus Modul 14
Präsenzzeit Modul insgesamt 56 h
Prüfung Prüfungszeiten Prüfungsform
Gesamtmodul
Am Ende des Semesters
Klausur oder mündliche Prüfung