In this course we will learn the principles of model checking, namely modeling with transition systems, the temporal logics LTL and CTL, their comparison, as well as algorithms for verifying these logics. In addition, on the practical side, we will get acquainted with the basics of the SPIN model checker, one of the most commonly used model checking tools for automatic verification.

- Textbook: Model Checking, by Edmund M. Clarke, Orna Grumberg, and Doron A. Peled, MIT Press, 1999.

- Textbook: Principles of Model Checking by Christel Baier and Joost-Pieter Katoen. MIT Press, 2008.
- The Spin Model Checker, Primer and Reference Manual, by Gerard J. Holzmann, Addison-Wesley, 2004.
- Principles of the Spin Model Checker, by Mordechai Ben-Ari, Springer, 2008.

(1) OBDDs, Bryant's work and extensions, implementation details (theoretical mini project) - Tobias Berka

(2) Model checking garbage collection with SPIN - Andreas Haas

(3) Model checking a security protocol with SPIN - Stefan Jenisch and Stefan Lukesch

(4) Model checking non-blocking data structures with SPIN - Andreas Schoenegger

(5) Logic(s) for probabilistic model checking (theoretical mini project) - Silviu Craciunas

The deadline for completing the mini projects is 15.7.2009. Each student should submit a concise description of the project and the results (up to 5 pages of text).

- Week 1, Tuesday 3.3.09: Introduction to Model Checking (Chapter 1 of all books), first meeting. Thursday, 5.3.09: Modelling, (MC book p.12-16, PMC book p.19-26)
- Week 2, Tuesday 10.3.09: Modelling (MC book p.16-25, PMC book p.26-88), Homework: Derive a formula and draw the Kripke structure for a simple concurrent program for mutual exclusion presented in class; read about modelling of mutual exclusion in Promela/SPIN in the SPIN book (Chapter 2) and try out one example in SPIN; Thursday 12.3.09: CTL* (MC book p. 27-30).
- Week 3, Tuesday 17.3.09: LTL and CTL (MC book p.30-32, PMC book browse through Chapter 5 and Chapter 6). Homework: given in class, 2 illustrative exercises. Thursday 19.3.09 no class.
- Week 4, Thursday 26.3.09 (3 hours): Fairness, Tarjan's algorithm for strongly connected components in a graph, and model checking CTL (MC book p. 32-37, SIAM Journal of Computing 1(2) 1972 for Tarjan's algorithm).
- Week 5, Thursday 2.4.09 (3 hours): Model checking CTL (continued), examples, model checking CTL with fairness, examples, towards symbolic model checking (fixed points). (MC book p.37-41 and p.60-63) Homework: given in class, one illustrative exercise.
- Week 6, Thursday 23.4.09 (3 hours): Symbolic model checking CTL (continued), examples, OBDDs. (MC book p.64-69 and p.51-57) Homework: given in class, (1) an illustrative exercise for symbolic model checking, and (2) prove the fixpoint characterisation of AFf.
- Week 7, Thursday 30.4.09 (3 hours): OBDDs (continued), fair symbolic model checking CTL, examples, counterexamples and witnesses. (MC book p.57-60 and p.69-75)
- Week 8, Thursday 7.5.09 (3 hours): Model checking LTL, automata-based approach. (MC book p.121-127) Homework: simple illustrative exercise on witnesses and counter examples given in class.
- Week 9, Thursday 14.5.09 (3 hours): Model checking LTL, properties of Buechi automata. (MC book p.127-132)
- Week 10, Thursday 28.5.09 (3 hours): Translating LTL formulas to Buechi automata. (MC book p.132-138) HW: Construct automata for [pUq] and [rU[pUq]], using the translation algorithm.
- Week 11, Thursday 4.6.09 (3 hours): Model checking mu-calculus. (MC book p.97-103) HW: Show the duality of least and greatest fixed points (with respect to negation).
- Week 12, Thursday 18.6.09 (3 hours): Model checking mu-calculus; State space reduction via equivalences and preorders. (MC book p.103-105, 107-108, 171-176, 178-180) HW: Apply the model checking algorithm (both the naive one and the Emerson-Lei's one) on a simple example, given in class.
- Week 13, Thursday 25.6.09 (3 hours): Discussion, Q&A, we go through an exemplaric set of exam problems/questions.

Student ID | Exam points (<= 100) | HW points (*)(<= 11) | Project points (<= 25) | Mark (**) | Exam date |

****240 | 85 | - | 25 | 1 | 2.7.9 |

****949 | 88 | 9 | 25 | 1 | 2.7.9 |

****259 | 51 | - | 23 | 3 | 2.7.9 |

****929 | 44 | 5 | 20 | 3 | 2.7.9 |

****307 | 31 | - | 23 | 4 | 25.8.9 |

(*) There were 11 homework tasks. Each delivered homework task counts as one HW point.

(**) Total = Exam points + HW points + Project points. The final mark is determined as follows: 1 if Total >= 105, 2 if 85 <= Total <= 104, 3 if 65 <= Total <= 84, 4 if 50 <= Total <= 64, 5 otherwise.