Modellierung, Analyse, Verifikation (WS 2025/26)
Dozentin:
Prof. Dr. Barbara König
Übungsleitung:
Karla Messing
Inhalt und Lernziele
Zur automatischen Verifikation und Validierung von Programmen und Systemen benötigt man Verfahren, die bei Eingabe eines Programms und einer zugehörigen Spezifikation entscheiden, ob das Programm diese Spezifikation erfüllt.
Im Allgemeinen ist dieses Problem unentscheidbar, es gibt jedoch viele sicherheitskritische Programme, die man dennoch gerne maschinell analysieren und verifizieren möchte. Auch sie können analysiert werden, wenn man nicht-vollständige Verfahren zulässt. Man verlangt, dass diese Analyseverfahren niemals ein fehlerhaftes Programm als korrekt ansehen, es ist aber zulässig, korrekte Programme abzulehnen (einseitiger Irrtum). Auf diese Weise kann immer noch eine große Menge von Programmen analysisert und ihre Korrektheit verifiziert werden. Ein anderer wichtiger Anwendungsbereich ist die Programmoptimierung im Compilerbau.
In der Vorlesung werden insbesondere folgende Themen behandelt:
- Datenflussanalyse (Fixpunkttheorie, Monotone Frameworks, Worklist-Algorithmus, Anwendungsbeispiele: Compilerbau, Java Bytecode Verifier)
- Grundlagen der abstrakten Interpretation (Galois-Verbindungen, Sichere Approximation von Funktionen, Abstraktionsverfeinerung)
Tools
Folgende Werkzeuge werden in der Vorlesung eingesetzt:
- PAG/WWW (Programmanalyse-Generator mit WWW-Interface)
- jasmin (Assembler für Java-Bytecode)
Termine
Die Vorlesung und Übung werden in der Regel in Präsenz stattfinden.
Vorlesung
Die Vorlesung findet wöchentlich am Dienstag & Donnerstag, um 8:30-10:00, im LC 137 statt.
Die erste Vorlesung findet am 14.10.2025 statt.
Übungen
Die Übung wird jede zweite Woche statt einer der beiden Vorlesungen stattfinden. Die genauen Termine werden rechtzeitig vorher in der Vorlesung und im Moodle bekannt gegeben.
Die Übungsblätter werden über den Moodle-Kurs bereit gestellt.
Prüfung
Die Prüfung wird als mündliche Prüfung stattfinden. Die Termine werden im Laufe des Semesters bekannt gegeben.
(Anmeldung über das Prüfungsamt im Anmeldezeitraum)
Downloads
Die Vorlesungsfolien, das Skript und die Übungsblätter werden über das Moodle der Vorlesung zur Verfügung gestellt. Bitte melden Sie sich in diesem Moodle-Kurs an (der Zugangsschlüssel wird in der Vorlesung verteilt).