| N | Data | Time | Room | Kind | Topic |
| 1t | Mon 16/09 | 14:00-16:00 | L1 | theory | An introduction to model checking |
| 2t | Tue 17/09 | 16:00-18:00 | M1 | theory | On transition systems and the modelling of parallel/communicating systems |
| 3t | Wed 18/09 | 14:00-16:00 | L1 | theory | Transition systems for modelling channel systems |
| 1e | Mon 23/09 | 14:00-16:00 | L1 | exe | First exercise sheet |
| 2e | Tue 24/09 | 16:00-118:00 | M1 | exe | Solutions of the first exercise sheet |
| 4t | Wed 25/09 | 14:00-16:00 | L1 | theory | On linear time properties |
| 5t | Mon 30/09 | 14:00-16:00 | L1 | theory | On safety |
| 6t | Tue 01/10 | 16:00-18:00 | online | theory | On liveness and fairness |
| 3e | Wed 02/10 | 14:00-16:00 | online | exe | Second exercise sheet |
| 7t | Mon 07/10 | 14:00-16:00 | L1 | theory | Regular safety properties |
| 8t | Tue 08/10 | 16:00-18:00 | M1 | theory | ω-regular properties [up to slide 137] |
| 9t | Wed 09/10 | 14:00-16:00 | online | theory | Closure results for ω-regular properties [from slide 138] |
| 10t | Mon 14/10 | 14:00-16:00 | L1 | theory | Model checking with Büchi automata |
| 4e | Tue 15/10 | 16:00-18:00 | M1 | exe | Third exercise sheet |
| 5e | Wed 16/10 | 14:00-16:00 | L1 | exe | Q&A session |
| 11t | Mon 21/10 | 14:00-16:00 | L1 | theory | Syntax and semantics of linear temporal logic [up to slide 216] |
| 12t | Tue 22/10 | 16:00-18:00 | M1 | theory | LTL formulas: normal forms and fairness [from slide 217] |
| 13t | Wed 23/10 | 14:00-16:00 | L1 | theory | Model checking with Büchi automata [skipping from slide 209 up to slide 310] |
| 6e | Thu 24/10 | 16:00-18:00 | C1 | exe | Fourth exercise sheet (and a cheating tool) |
| 14t | Mon 04/11 | 14:00-16:00 | L1 | theory | Syntax and semantics of computational tree logic |
| 7e | Tue 05/11 | 16:00-18:00 | M1 | exe | Fifth exercise sheet |
| 15t | Wed 06/11 | 14:00-16:00 | L1 | theory | CTL vs LTL |
| 16t | Mon 11/11 | 14:00-16:00 | L1 | theory | Some model checking [skipping from slide 99 up to slide 125] |
| 17t | Tue 12/11 | 16:00-18:00 | M1 | theory | On fair CTL |
| 8e | Thu 14/11 | 16:00-18:00 | A1 | exe | Sixth exercise sheet |
| 18t | Mon 18/11 | 14:00-16:00 | L1 | theory | On CTL* |
| 19t | Tue 19/11 | 16:00-18:00 | M1 | theory | Equivalences for transitions systems |
| 9e | Wed 20/11 | 14:00-16:00 | L1 | exe | Seventh exercise sheet |
| 10e | Tue 26/11 | 16:00-18:00 | M1 | exe | Q&A session |
| 11e | Wed 27/11 | 14:00-16:00 | L1 | exe | Mid-term |
| 20t | Mon 02/12 | 14:00-16:00 | L1 | theory | Statistical model checking: foundations (by Andrea Vandin) |
| 12e | Tue 03/12 | 16:00-18:00 | M1 | exe | Solving and marking mid-term |
| 21t | Wed 04/12 | 14:00-16:00 | L1 | theory | Statistical model checking: applications (by Andrea Vandin) |
| 22t | Mon 09/12 | 14:00-16:00 | L1 | theory | Spatial model checking: foundations (by Vincenzo Ciancia) |
| 23t | Tue 10/12 | 16:00-18:00 | C1 | theory | Spatial model checking: applications to medical imaging (by Vincenzo Ciancia) |
| 13e | Wed 11/12 | 14:00-16:00 | L1 | exe | Seminar planning |