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