### Algorithms for Model Checking (2IW55)

In these lectures, we study the model checking problem from an algorithmic
viewpoint. In particular, algorithms for various temporal logics
(CTL, LTL, mu-calculus, etc) are studied and presented.

#### Update

- Nov 13:
Some typos have been fixed. Notable changes occurred in week 6
(fixed scoping of an
*if* statement in the Emerson-Lei algorithm
and corrected embedding of CTL into mu-calculus).
- Jan 3-4:
Changed font settings as the previous font somehow did not print
some characters such as
*[*. Most changes in week 6 and week 15.
- Jan 5:
Added exercises to weeks 11 and 12.
- Jan 21: For those of you that did not attend the lectures:
the exam is
**open book**, i.e. the book, handouts and slides may
be used for consulting during the examination. Laptops and grannies are not
allowed.

#### Course material

- Required reading:
Model Checking. Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled.
MIT Press, ISBN 0-262-03270-8
- Handouts:
- week 2: Depth-First Search and Linear Graph Algorithms by R. Tarjan
- week 5: Bounded Model Checking by A. Biere, A. Cimatti, E. Clarke, O. Strichman, Y. Zhu
- week 7: Verification of
Modal Properties Using Boolean Equation Systems by A. Mader
- week 11--13: Optional reading:
Timed
Automata by R. Alur
- week 14--15: Optional reading:
- Parameterised
Boolean Equation Systems by J.F. Groote and T.A.C. Willemse
- Model-checking Processes with Data by J.F. Groote and T.A.C. Willemse

#### Course notes

- week 1: The temporal logics CTL*, CTL and LTL: syntax and semantics
(slides)
- week 2: Fairness and Basic Model Checking Algorithms for CTL and fair CTL
(slides)
- week 3: Symbolic Model Checking for CTL
(slides)
- week 4: Symbolic Model checking: fairness and counterexamples
(slides)
- week 5: Bounded Model Checking (slides)
- week 6: Mu-calculus (slides)
- week 7: Boolean Equation Systems (slides)
- week 8: Equivalences and Pre-orders: State Space Reduction and Preservation
of Properties (slides)
- week 9: Data Abstraction (see slides for week 8 of
previous year)
- week 10: Repetition of week 1-9, no new material
- week 11: Timed Verification: Timed Automata (slides)
- week 12: Timed Verification: Timed Automata (slides)
- week 13: Timed Verification: Timed Automata (slides)
- week 14: Parameterised Boolean Equation Systems (slides)
- week 15: Parameterised Boolean Equation Systems (slides)

For slides of previous years, see

here.
First day's announcements can be downloaded

here.