Formale Spezifikation und Verifikation

Aktuelles

Aktualisiertes Skript
Klausur: Mi 31.7.2019, 16-18 Uhr s.t., Geschwister-Scholl-Platz 1, B101 und B201.
Bitte anmelden bis 28.7.2019, 23:55 Uhr: UniWorX
Raumzuteilung: A-M: B101; N-Z: B201
Nachholklausur: Mo, 7.10.2019, 12-14 Uhr s.t., Geschwister-Scholl-Platz 1, M 018
Bitte anmelden bis 3.10.2019, 23:55 Uhr: UniWorX
Raumzuteilung: A-Z: M 018

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.

Modulhandbuch, 2.18 P 18: Formale Spezifikation und Verifikation (INF-FSV), Seite 48.

Personen

Dozent: Prof. Dr. Gidon Ernst
Übungsleitung: Martin Spießl

Termine

Vorlesung: Mo 11-14 Uhr c.t., Schellingstr. 3, S 004 (erste Vorlesung am 29.04.2019)
Übung: (erste Übungen am 02.05.2019)
- Do 16-18 Uhr c.t., Schellingstr. 3, S005
- Do 18-20 Uhr c.t., Hauptgebäude, A 017
Klausur: Mi 31.7.2019, 16-18 Uhr s.t., Geschwister-Scholl-Platz 1, B101 und B201, Raumzuteilung: A-M: B101; N-Z: B201
Nachholklausur: Mo 7.10.2019, 12-14 Uhr s.t., Geschwister-Scholl-Platz 1, M 018, Raumzuteilung: A-Z: M 018

Materialien

Skript

Vorlesung

Themen

29.4. Einführung, Modelle, Verifikation
06.5. Transitionssysteme, explizite Errreichbarkeitsanalyse
13.5. Testing
20.5. Symbolische Erreichbarkeitsanalyse
27.5. SROBDDs
03.6. LTL und Automaten
10.6. entfällt
17.6. LTL und Automaten
24.6. Software-Verifikation und Tools
01.7. entfällt
08.7. SAT, DPLL, SMT
15.7. entfällt
22.7. Deduktive Verifikation

Übung

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