WS 2012/13: Modellierung, Analyse, Verifikation (Programmanalyse)

Dozentin / Übungsleitung

Dozentin:
Prof. Dr. Barbara König (Email)

Übungsleitung:

Jan Stückrath (Email)

Lernziele / Inhalt

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äßt. 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)
  • Model-Checking und/oder Typsysteme

Der Inhalt der Vorlesung wird im wesentlichen ähnlich zur Vorlesung im Wintersemester 2011/12 sein. Allerdings beträgt der Umfang der Vorlesung in diesem Semester nur 4 SWS, weswegen der Stoffumfang gekürzt sein wird.

Bonuspunkteregelung

Drei der Übungsblätter werden Testatblätter sein, die abgegeben werden können und bewertet werden. Man kann einen Bonus für die Vorlesung bekommen, wenn man alle drei Blätter bearbeitet, darauf mindestens 50% der Punkte erhält und eine Aufgabe in der Übung vorrechnet. Der Bonus verbessert die Note um eine Stufe (z.B. 2,3 auf 2,0).

Tools

Folgende Werkzeuge werden in der Vorlesung eingesetzt:

  • wAnalyzer (Datenflussanalyse-Tool: Softwarepraktikum an der Universität Stuttgart)
  • PAG/WWW (Programmanalyse-Generator mit WWW-Interface)
  • jasmin (Assembler für Java-Bytecode) 

Termine

Vorlesung:

  • Di, 8:15-9:45 Uhr, LC 137
  • Do, 8:30-10:30 Uhr, LC 137

Achtung: Am Dienstag beginnt die Vorlesung bereits um 8:15 Uhr!

Vorlesungsbeginn: 16.10.2012

Übungen:

In der Regel wird jeden zweiten Donnerstag statt der Vorlesung eine Übung stattfinden. Die genauen Termine sind:

30.10. / 15.11. / 29.11. / 13.12. / 10.01 / 29.01. / 07.02.

Prüfung

Die mündlichen Prüfungen im Sommersemester 2013 finden am 1. und 2. August 2013 statt. Ab sofort liegen im Sekretariat (LF 227) Terminlisten aus, in die man sich eintragen kann.

Aktuelles

no news in this list.

© Universität Duisburg-Essen, Lehrstuhl Theoretische InformatikLogin