Modellierung, Analyse, Verifikation (WS 2020/21)
Vergangene VeranstaltungDiese Seite bezieht sich auf eine Vorlesung aus vorherigen Jahren. Aktuelle Termine und Arbeitsmaterialien sind hier zu finden. |
Vorlesungsablauf
Die Vorlesung wird dieses Wintersemester aufgrund der Covid-19-Situation nicht als Präsenzveranstaltung stattfinden, sondern online. Bitte melden Sie sich im Moodle-Kurs an (Zugangsschlüssel notwendig, wenden Sie sich bitte an Frau Prof. König oder Frau Mika-Michalski). Alle Materialien und weitere Informationen werden im Moodle regelmäßig aktualisiert.
Wir werden wöchentlich Videos von der Vorlesung bereitstellen. Übungsaufgaben werden online abgegeben und bewertet. Auch die Besprechung der Übungen erfolgt online durch Videos. Ihre Fragen zum Stoff können im Moodle-Forum oder per Mail gestellt werden und werden von uns beantwortet. Außerdem werden wir online Fragestunden in einem BBB-Meetingraum anbieten (dazu mehr demnächst im Moodle).
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 2019/20 sein.
Tools
Folgende Werkzeuge werden in der Vorlesung eingesetzt:
- PAG/WWW (Programmanalyse-Generator mit WWW-Interface)
- jasmin (Assembler für Java-Bytecode)
Termine
Vorlesung
Ab der Woche vom 2. November online als Aufzeichnung zum Download, Links werden im Moodle bereitgestellt.
Übungen
Online als Aufzeichnung zum Download (siehe Moodle). Alle Fragen bitte im Diskussionsforum stellen oder via email.
Prüfung
TBA
Downloads
Die Vorlesungsfolien, das Skript und die Übungsblätter werden über das Moodle der Vorlesung zur Verfügung gestellt.