inf407 - Programmverifikation (Vollständige Modulbeschreibung)
Modulbezeichnung | Programmverifikation |
Modulkürzel | inf407 |
Kreditpunkte | 6.0 KP |
Workload | 180 h |
Einrichtungsverzeichnis | Department für Informatik |
Verwendbarkeit des Moduls |
|
Zuständige Personen |
|
Teilnahmevoraussetzungen | Theoretische Informatik I und II |
Kompetenzziele | Einführung in Methoden zum Nachweis der Korrektheit von sequentiellen, parallelen und verteilten Programmen. Fachkompetenzen Die Studierenden:
Die Studierenden:
Die Studierenden:
|
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:
|
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 |