N 
Data

Time

Room

Kind

Topic

1t 
Mon 16/09 
1416 
X1 
theory 
Introduction to model checking
and to controlintensive transition systems [up to slide 79]

2t 
Tue 17/09 
1113 
X1 
theory 
Dataintensive transition systems [from slide 80]
and the modelling of parallel/communicating systems

3t 
Thu 19/09 
1618 
X1 
theory 
Transition systems
for modelling channel systems

1e 
Fri 20/09 
1416 
X1 
exe 
First
exercise sheet

4t 
Mon 23/09 
1416 
X1 
theory 
On linear time properties

5t 
Fri 27/09 
1416 
X1 
theory 
On safety

6t 
Mon 30/09 
1416 
X1 
theory 
On liveness and fairness

7t 
Tue 01/10 
1113 
X1 
theory 
Regular safety properties

2e 
Thu 03/10 
1618 
X1 
exe 
Second
exercise sheet

8t 
Fri 04/10 
1416 
X1 
theory 
ωregular properties [up to slide 137]

9t 
Mon 07/10 
1416 
X1 
theory 
Closure results for ωregular properties [from slide 138]

10t 
Thu 17/10 
1416 
X2 
theory 
Model checking with Büchi automata

3e 
Fri 18/10 
1416 
X1 
exe 
Third
exercise sheet

11t 
Mon 21/10 
1416 
X1 
theory 
Syntax and semantics of linear temporal logic

12t 
Thu 24/10 
1416 
X2 
theory 
Model checking with Büchi automata
[skipping from slide 209 up to slide 310]

4e 
Fri 25/10 
1416 
X1 
exe 
Fourth
exercise sheet

5e 
Mon 28/10 
1416 
X1 
exe 
Checking (all) exercises

6e 
Thu 07/11 
1416 
X2 
exe 
Summing up theory and exercises

7e 
Fri 08/11 
1416 
X1 
exe 
Midterm

13t 
Mon 11/11 
1416 
X1 
theory 
Syntax and semantics of computational tree logic

14t 
Fri 15/11 
1416 
X1 
theory 
Probabilistic model checking (by Mieke Massink)

15t 
Tue 19/11 
1113 
X1 
theory 
Model checking PCTL (by Mieke Massink)

16t 
Thu 21/11 
1416 
X2 
theory 
Mean field model checking population models (by Mieke Massink)

8e 
Fri 22/11 
1416 
X1 
exe 
Checking midterm

17t 
Mon 25/11 
1416 
X1 
theory 
CTL vs LTL
and some model checking [up to slide 98]

9e 
Tue 26/11 
1113 
X2 
exe 
Fifth exercise sheet

18t 
Thu 28/11 
1416 
X2 
theory 
Topologics (by Vincenzo Ciancia)

19t 
Fri 29/11 
1416 
X1 
theory 
A tour on VoxLogicA
(by Vincenzo Ciancia)

20t 
Mon 02/11 
1416 
X1 
theory 
Medical image analysis via model checking (by Vincenzo Ciancia)

21t 
Fri 06/12 
1416 
X1 
theory 
Fair CTL [up to slide 64] and on CTL*
(including equivalences) 
22t 
Mon 09/12 
1415 
X1 
theory 
On quantified modal logics

10e 
Mon 09/12 
1516 
X1 
exe 
Sixth exercise sheet

23t 
Tue 10/12 
1113 
X1 
theory 
A survey on formal methods for validation and verification (by Roberto Bagnara)

24t 
Thu 12/12 
1416 
X2 
theory 
A gentle introduction to abstract interpretation (by Roberto Bagnara)

25t 
Fri 13/12 
1416 
X1 
theory 
On the MISRA C coding standard (by Roberto Bagnara)

11e 
Mon 16/12 
1416 
X1 
exe 
Scheduling the seminars and so on
