| N | Data | Time | Room | Kind | Topic |
| 1t | Tue 15/09 | 14:00-16:00 | L1 | theory | An introduction to model checking and a taste of transition systems |
| 2t | Thu 17/09 | 16:00-18:00 | L1 | theory | Transition systems for modelling parallel/communicating systems |
| 3t | Fri 18/09 | 11:00-13:00 | L1 | theory | Transition systems for modelling channel systems |
| 1e | Tue 22/09 | 14:00-16:00 | L1 | exe | First exercise sheet |
| 4t | Thu 24/09 | 16:00-18:00 | L1 | theory | On linear time properties |
| 5t | Fri 25/09 | 11:00-13:00 | L1 | theory | On safety |
| 6t | Tue 29/09 | 14:00-16:00 | L1 | theory | On liveness and fairness |
| 2e | Thu 01/10 | 16:00-18:00 | L1 | exe | Second exercise sheet |
| 7t | Fri 02/10 | 11:00-13:00 | L1 | theory | Regular safety properties |
| 8t | Tue 06/10 | 14:00-16:00 | L1 | theory | ω-regular properties [up to slide 137] |
| 9t | Thu 08/10 | 16:00-18:00 | L1 | theory | Closure results for ω-regular properties [from slide 138] |
| 10t | Fri 09/10 | 11:00-13:00 | L1 | theory | Model checking with Büchi automata |
| 4e | Tue 13/10 | 14:00-16:00 | L1 | exe | Third exercise sheet |
| 11t | Tue 20/10 | 14:00-16:00 | L1 | theory | Syntax and semantics of linear temporal logic [up to slide 216] |
| 12t | Thu 22/10 | 16:00-18:00 | L1 | theory | LTL formulas: normal forms and fairness [from slide 217] |
| 13t | Fri 23/10 | 11:00-13:00 | L1 | theory | Model checking with Büchi automata [skipping from slide 209 up to slide 310] |
| 6e | Tue 27/10 | 14:00-16:00 | L1 | exe | Fourth exercise sheet (and a cheating tool) |
| 14t | Thu 29/10 | 16:00-18:00 | L1 | theory | Syntax and semantics of computational tree logic |
| 7e | Fri 30/10 | 11:00-13:00 | L1 | exe | Fifth exercise sheet |