..
Suche
Hinweise zum Einsatz der Google Suche
Personensuchezur unisono Personensuche
Veranstaltungssuchezur unisono Veranstaltungssuche
Katalog plus
 

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