Stud.IP Uni Oldenburg
Universität Oldenburg
29.07.2021 11:10:31
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) > Mastermodule
  • Zwei-Fächer-Bachelor Informatik (Bachelor) > Wahlpflicht Theoretische Informatik (30 KP)
Zuständige Personen
Olderog, Ernst-Rüdiger (Prüfungsberechtigt)
Lehrenden, Die im Modul (Prüfungsberechtigt)
Teilnahmevoraussetzungen
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
  • K.R. Apt, E.-R. Olderog, Programmverifikation, Springer-Verlag, 1994 oder die erweiterte englische Ausgabe
  • K.R. Apt, E.-R. Olderog, Verification of Sequential and Concurrent Programs, 2nd Edition, Springer-Verlag, 1997
Links
Unterrichtssprache Deutsch
Dauer in Semestern 1 Semester
Angebotsrhythmus Modul unregelmäßig
Aufnahmekapazität Modul unbegrenzt
Modullevel / module level AS (Akzentsetzung / Accentuation)
Modulart / typ of module je nach Studiengang Pflicht oder Wahlpflicht
Lehr-/Lernform / Teaching/Learning method V+Ü
Vorkenntnisse / Previous knowledge Theoretische Informatik I und II
Lehrveranstaltungsform Kommentar SWS Angebotsrhythmus Workload Präsenz
Vorlesung
3 42
Übung
1 14
Präsenzzeit Modul insgesamt 56 h
Prüfung Prüfungszeiten Prüfungsform
Gesamtmodul
Am Ende des Semesters
Klausur oder mündliche Prüfung