Modellierung, Analyse, Verifikation (WS 2019/20)
Dozentin/Übungsleitung:
Prof. Dr. Barbara König
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)
Der Inhalt der Vorlesung wird im Wesentlichen ähnlich zur Vorlesung im Wintersemester 2018/19 sein.
Tools
Folgende Werkzeuge werden in der Vorlesung eingesetzt:
- PAG/WWW (Programmanalyse-Generator mit WWW-Interface)
- jasmin (Assembler für Java-Bytecode)
Termine
Vorlesung
- Dienstag, 8:30-10:00, LC 137
- Donnerstag, 8:30-10:00, LC 137 (jede zweite Woche)
Erste Vorlesung am 15.10.19
Am 28.1.20 findet im Rahmen der Vorlesung eine Fragestunde statt.
Übungen
- Donnerstag, 8:30-10:00, LC 137 (jede zweite Woche)
Übungstermine: 29.10., 14.11., 28.11., 12.12., 16.1., 30.1.
Die dazugehörigen Übungsblätter werden jeweils eine Woche vorher veröffentlicht.
Prüfung
Die mündlichen Prüfungen im Sommersemester finden am 23. und 24. Juli 2020 statt (Alternativtermin: 30. Juli 2020). Bitte melden Sie sich beim Prüfungsamt im Anmeldezeitraum (15.6.-26.6.) an. Bitte kontaktieren Sie mich, um einen genauen Termin zu erhalten. Dann kann ich Ihnen auch Einzelheiten zum Prüfungsablauf mitteilen.
Die mündlichen Prüfungen finden am 6. und 7. Februar 2020 im Raum LF 264 statt. Ab sofort liegen im Sekretariat LF 227 Terminlisten aus, in die Sie sich eintragen können.
Downloads
Skript
- Skript (Stand 17.10.2019)
Folien
Die Folien werden ähnlich zu den Folien im Wintersemester 2018/19 sein.
Hinweis: s/w = schwarz-weiß
- Alle Folien (Stand: 23.1.20): [1x1] [2x2] [1x1(s/w)] [2x2(s/w)]
Folien, unterteilt in Kapitel
- Organisation (Stand: 22.10.19) [1x1] [2x2] [1x1(s/w)] [2x2(s/w)]
- Einführung (Stand: 17.10.19) [1x1] [2x2] [1x1(s/w)] [2x2(s/w)]
- Datenflussanalyse (Stand: 19.11.19) [1x1] [2x2] [1x1(s/w)] [2x2(s/w)]
- Java Bytecode Verifier (Stand: 26.11.19) [1x1] [2x2] [1x1(s/w)] [2x2(s/w)]
- Abstrakte Interpretation (Stand: 23.1.20) [1x1] [2x2] [1x1(s/w)] [2x2(s/w)]
Übungsblätter
- Übungsblatt 1 (Besprechung am 29.10, kein Testatblatt)
- Übungsblatt 2 (Besprechung am 14.11, Testatblatt: Abgabe vor der Übung oder im LF 261)
- Übungsblatt 3 (Besprechung am 28.11, kein Testatblatt)
- Übungsblatt 4 (Besprechung am 12.12, Testatblatt: Abgabe vor der Übung oder im LF 261)
- Übungsblatt 5 (Besprechung am 16.01, Testatblatt: Abgabe vor der Übung oder im LF 261)
- Übungsblatt 6 (Besprechung am 30.01, kein Testatblatt)