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