Seminar Verifikation (WS 2013/14)
Organisatorisches
- Veranstalter: Prof. Dr. Markus Lohrey (Raum H-A 7109, Tel. 0271-740-2826)
- Termin: Montags, 12:00-14:00, im H-F 115
- Einführungstermin: Montag, 14. Oktober, 12:00, im H-F 115
Unter Verifikation oder Model-Checking versteht man den automatisierten Beweis, dass ein System das tut, was man von ihm erwartet. Systeme können verschiedenster Natur sein, etwa Hardware, Software, Echtzeitsysteme, stochastische Prozesse (z.B. Markov-Ketten), u.s.w. Eigenschaften solcher Systeme lassen sich mittels temporaler Logiken, wie etwa LTL (Linear Temporal Logic) oder CTL (Computation Tree Logic) adequat formalisieren. Model-Checking ist dann die Aufgabe, nachzuweisen, dass ein System eine temporallogische Formel erfüllt. Hierfür sollen in dem Seminar auf die verschiedenen Systemtypen zugeschnittene Algorithmen vorgestellt werden.
Programm
(alle Angaben beziehen sich auf das Lehrbuch von Baier und Kartoen)
Datum | Thema | Vortragender | Betreuer | |
1. | 02.12.2013 | Automaten auf unendlichen Wörtern I (Kap. 4.3) | Philip Reh |
|
2. | 09.12.2013 | Automaten auf unendlichen Wörtern II (Kap. 4.4) | Danny Hucke |
|
3. | 16.12.2013 | Linear Time Temporal Logic (LTL): Syntax und Semantik (Kap. 5.1) | Simon Heimes |
|
4. | 13.01.2014 | LTL Model-Checking (Kap. 5.2) | Felix Nöh |
|
5. | 20.01.2014 | Computation Tree Logik (CTL): Syntax und Semantik (Kap. 6.1-6.3) | Benjamin Elfers |
|
6. | 20.01.2014 | CTL Model-Checking (Kap. 6.4) | Benjamin Elfers |
|
7. | 27.01.2014 |
CTL Model-Checking mit OBDDs (Kap. 6.7) | Eric Nöth |
|
8. | Echtzeitautomaten (Kap. 9.1) | |||
9. | Timed CTL (Kap. 9.2) | |||
10. | Markov-Ketten (Kap. 10.1) | |||
11. | Probabilistisches CTL (Kap. 10.2) | |||
12. | ||||
13. | ||||
14. |
Lehrbücher
- Christel Baier, Joost-Pieter Katoen, Principles of Model Checking. MIT Press, 2008.
Impressum