WS 2015/16: Modellierung, Analyse, Verifikation

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)

Der Inhalt der Vorlesung wird im wesentlichen ähnlich zur Vorlesung im Wintersemester 2014/15 sein.

Bonusregelung

Es wird insgesamt sieben Übungsblätter geben, von denen drei Testatblätter sein werden. Man kann einen Bonus für die Prüfung erhalten, d.h. eine Notenaufwertung um eine Stufe (z.B. 2,3 auf 2,0), wenn man:

  • alle Testatblätter bearbeitet und abgibt,
  • insgesamt mindestens die Hälfte der Punkte in den Aufgaben erhält, und
  • eine Übungsaufgabe in den Übungen vorrechnet.

Tools

Folgende Werkzeuge werden in der Vorlesung eingesetzt:

  • PAG/WWW (Programmanalyse-Generator mit WWW-Interface)
  • jasmin (Assembler für Java-Bytecode) 

Termine

Vorlesung:

  • Di, 8:30–10 Uhr, LC 137
  • Do, 8:30-10 Uhr, LC 137

Übungen:

  • Do, 8:30-10 Uhr, LC 137

Die Übungen finden (nur) an den folgenden Terminen, anstelle der Vorlesung, statt:

05.11. / 19.11. / 03.12. / 17.12. / 14.01. / 28.01. / 11.02.

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

Die mündlichen Prüfungen im Sommersemester 16 finden vom 15.-18.8.2016 statt, bevorzugt am 16.8.2016. Bitte schreiben Sie mir eine Mail (barbara_koenig(at)uni-due.de), um einen Termin zu vereinbaren.

Aktuelles

no news in this list.

© Universität Duisburg-Essen, Lehrstuhl Theoretische InformatikLogin