WS 2011/12: Modellierung, Analyse, Verifikation

Dozentin / Übungsleitung

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

Übungsleitung:

Jan Stückrath (Email)
früher: Christoph Blume (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 Sommersemester 2009 sein.

 

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:

  • Mi, 12–14 Uhr, LC 137
  • Do, 08-10 Uhr, LC 137

Übungen:

  • Do, 10-12 Uhr, LC 140

Übungsbeginn: Donnerstag, den 27. Oktober

Am 2.2. findet im Rahmen der Vorlesung eine Wiederholungsstunde statt! Bitte schicken Sie Ihre Fragen an barbara_koenig(at)uni-due.de.

Prüfung

Bitte setzen Sie sich mit der Dozentin in Verbindung, um einen genauen Termin für die mündliche Prüfung am 10.7.12 zu erhalten.

Die Klausur zur Vorlesung findet am 09.02.2012 um 14 Uhr im Raum MC 351 statt.

Aktuelles

Keine Artikel in dieser Ansicht.

© Universität Duisburg-Essen, Lehrstuhl Theoretische InformatikLogin