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-07-10 (Mitschrift der VL vom 2018-06-25 hinzugefügt)
Vorlesungsevaluation
(Zugangsdaten finden Sie in den Folien zur ersten Übung im UniWorX)

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