Advanced Topics in Verification

Advanced Topics in Verification

News

05. Mai - Im zweiten Dokument zu Persistent Sets wurde die zweite Bedingung des Algorithmus genauer spezifiziert.
29. April - Es gab eine kleine Änderung auf Blatt 02, durch die genauer spezifiziert wird, was bei 2.1b) angegeben werden muss.
07. April - Die Veranstaltung beginnt am 13.04.2026.
16. Februar - Die Informationen auf dieser Webseite sind noch vorläufig.

Organisation

Der Modulverantwortliche ist Prof. Dr. Roland Meyer. Die Veranstaltung wird zudem von Thomas Haas betreut. Der Übungsbetrieb wird von Natalia Gacek geleitet.

  • Zielgruppe der Vorlesung sind Studierende der Informatik im Master.
  • Das Modul kann nur von Studierenden in der neuen Masterprüfungsordnung 6 belegt werden. Bei Fragen diesbezüglich wenden Sie sich bitte an das Prüfungsamt.
  • Falls Sie die Vorlesung in den Bachelor einbringen möchten, klären Sie dies bitte mit dem Prüfungsamt ab.
  • Vorlesungstermin: Montag, 15:00 - 16:30 in IZ 358
  • Übungstermin: Dienstag, 16:45 - 18:15 in IZ 358
  • Die Veranstaltung beginnt am 13.04.2026.

Modul

Es handelt sich um eine Veranstaltung mit 4 (2 VL + 2 Ü) Semesterwochenstunden.
Um das Modul erfolgreich mit 5 ECTS abzuschließen, sind zwei Leistungen zu erbringen:

  • Studienleistung: Sie erreichen mindestens 50% der Punkte in den Übungsaufgaben.
  • Prüfungsleistung: Sie bestehen eine (voraussichtlich) mündliche Prüfung in der vorlesungsfreien Zeit.

Übungsblätter

Materialien

Woche 1: Concurrent Systems

Woche 2: First Algorithms

Woche 3: Persistent Sets

Woche 4: Persistent Sets (continued), Sleep Sets (updated)

Woche 5: Remarks on Sleep Sets (see updated notes), Dynamic Partial-Order Reduction

Inhalte

In der Vorlesung werden aktuelle Themen in der Forschung im Bereich der Verifikation behandelt.

Literatur

Die Liste der Literatur, auf der die Vorlesung aufbaut, wird im Laufe des Semesters vervollständigt.

  • Patrice Godefroid. 1996. Partial-Order Methods for the Verification of Concurrent Systems. Springer Berlin, Heidelberg. ISBN 978-3-540-60761-8
  • Patrice Godefroid. 1997. Model checking for programming languages using VeriSoft. In POPL. ACM. DOI 10.1145/263699.263717
  • Cormac Flanagan and Patrice Godefroid. 2005. Dynamic Partial-Order Reduction for Model Checking Software. In POPL. ACM. DOI 10.1145/1040305.1040315