Vorlesung Model Checking (WS 2015/2016)

Aktuelles

Organisatorisches

• Veranstalter: Prof. Dr. Markus Lohrey (Raum H-A 7109, Tel. 0271-740-2826)
• Vorlesungstermine:
  • Dienstag, 12:00-14:00, im H-F 001
  • Donnerstag, 10:00-12:00, im H-F 001
• Übungen :
  • Freitag, 10:00-12:00, im H-F 104/105

---

Einige Themen

• Transitionssysteme
• LTL (Linear temporal logic)
• Büchiautomaten
• CTL (Computation tree logic)
• Ordered Binary Decision Diagrams und symbolisches Model-Checking
• Pushdownsysteme und Model-Checking rekursiver Programme

---

Folien (Version 26.01.2016)

---

Übungsblätter

• Übung 1
• Übung 2
• Übung 3
• Übung 4
• Übung 5
• Übung 6
• Übung 7
• Übung 8
• Übung 9
• Übung 10
• Übung 11
• Übung 12
• Übung 13

---

Lehrbücher

• Baier, Katoen. Principles of Model Checking, MIT Press 2008.
• Clarke, Grumberg, Peled. Model-Checking, MIT-Press 1999.

---