Formale Spezifikation und Verifikation

Aktuelles

Inhalt

Die Veranstaltung führt in grundlegende Methoden und Konzepte ein, die bei der Spezifikation und Verifikation von Systemen von Bedeutung sind. Es werden Spezifikationsformalismen, Konzepte der System-Modellierung und Grundtechniken für die Automatisierung der Verifikation behandelt. Neben der Vorlesung werden die besprochenen Inhalte im Übungsteil anhand von praktischen Anwendungen eingeübt.

Termine

Personen

Materialien

Die folgenden Materialien unterliegen dem Copyright. Teilnehmern der Vorlesung ist die Verwendung für persönliche Studien gestattet. Alle anderen Rechte sind vorbehalten.

Vorlesungsskript, aktualisiert 2018-05-15 (bis VL 2018-05-14)
(Fehler im "schlechten" BDD auf Seite 13 korrigiert, hier hatten in der Skriptversion vom 13. Mai noch zwei Kanten zum 0-Terminalknoten gefehlt)
(Zugangsdaten erhalten Sie in der Übung)

Vorlesung

Datum Geplante Themen
23.4.Einführung, Modelle, Verifikation
30.4.Transitionssysteme, explizite Errreichbarkeitsanalyse
07.5.Symbolische Erreichbarkeitsanalyse
14.5.SROBDDs
21.5.keine Vorlesung
28.5.LTL und Automaten (Teil 1)
04.6.LTL und Automaten (Teil 2)
11.6.Timed Automata
18.6.Software-Verifikation und zugehörige Tools
25.6.Testing und zugehörige Tools
02.7.keine Vorlesung
09.7.SAT, DPLL, SMT

Übung

Die Übungsblätter und Folien zur Besprechung der Übungsblätter finden Sie im UniWorX!

Hörerkreis

Bachelor Informatik

Empfohlene Vorkenntnisse

Literatur

Nützliche Links