Modulbezeichnung | Programmverifikation |
Modulkürzel | inf407 |
Kreditpunkte | 6.0 KP |
Workload | 180 h |
Einrichtungsverzeichnis | Department für Informatik |
Verwendbarkeit des Moduls |
|
Zuständige Personen |
Olderog, Ernst-Rüdiger (Modulverantwortung)
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:
Methodenkompetenzen Die Studierenden:
Sozialkompetenzen Die Studierenden:
Selbstkompetenzen 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 |
|
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 |