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 2017/18 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 9.10. Am 15. und 17. Januar fällt die Vorlesung aus.

Übungen

• Donnerstag, 8:30-10:00, LC 137 (jede zweite Woche)

Übungstermine: TBA

Die dazugehörigen Übungsblätter werden jeweils eine Woche vorher veröffentlicht.

Prüfung

Die mündlichen Prüfungen finden am 18. und 19. Juli 2019 statt. Im Sekretariat LF 227 liegen ab sofort Terminlisten aus, in die Sie sich eintragen können.

Downloads

Skript

• Skript (Stand 30.10.2018)

Folien

Die Folien werden ähnlich zu den Folien im Wintersemester 2017/18 sein.

Hinweis: s/w = schwarz-weiß

• Alle Folien (Stand: 29.1.19): [1x1] [2x2] [1x1(s/w)] [2x2(s/w)]

Folien, unterteilt in Kapitel

• Organisation (Stand: 11.10.18) [1x1] [2x2] [1x1(s/w)] [2x2(s/w)]
• Einführung (Stand: 11.10.18) [1x1] [2x2] [1x1(s/w)] [2x2(s/w)]
• Datenflussanalyse (Stand: 15.11.18) [1x1] [2x2] [1x1(s/w)] [2x2(s/w)]
• Java Bytecode Verifier (Stand: 29.11.18) [1x1] [2x2] [1x1(s/w)] [2x2(s/w)]
• Abstrakte Interpretation (Stand: 29.1.19) [1x1] [2x2] [1x1(s/w)] [2x2(s/w)]

Übungsblätter

• Übungsblatt 1 (Besprechung am 25.10.2018)
• Übungsblatt 2 (Besprechung am 8.11.2018)
• Übungsblatt 3 (Besprechung am 22.11.2018)
• Übungsblatt 4 (Besprechung am 6.12.2018)
• Übungsblatt 5 (Besprechung am 13.12.2018)
• Übungsblatt 6 (Besprechung am 10.1.2019)
• Übungsblatt 7 (Besprechung am 31.1.2019)