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