- Theory of model checking
- various approaches
- links to other courses
- automata
- temporal logic
- overview of literature
- Promela (the description language)
- syntax
- semantics (informally)
- practical use
- Protocols
- what are they?
- modelling them efficiently
- Using the Spin tool
- spin vs. xspin
- finding documentation
- Simulation
- Analysis and Validation
- principles
- unreachable code
- deadlock
- ``simple'' assertions
- assertions in combination with monitors: system invariants
- never claims and Linear Temporal Logic
- various cycle checks, fairness
- Tackling the state explosion
- partial order reduction
- compression techniques
- atomic and d_step
- other optimisations
- bit-state hashing
- Exercises
- theoretical (``think questions'')
- practical (``think & do'')
- Assignment
- Evaluation
- weak and strong points of model checking
- weak and strong points of Spin
- examples where model checking/Spin is less applicable