N 
Data

Time

Room

Kind

Topic

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

2t 
Tue 18/09 
1113 
X1 
theory 
Dataintensive transition systems [from slide 80]
and the modelling parallel systems [up to slide 72]

3t 
Thu 20/09 
1618 
N1 
theory 
Transition systems
for modelling communicating [from slide 77]
and channel systems

4t 
Fri 21/09 
1113 
N1 
theory 
On linear time properties

1e 
Mon 24/09 
1416 
X1 
exe 
First
exercise sheet

5t 
Thu 27/09 
1618 
X1 
theory 
On safety

6t 
Tue 02/10 
1113 
X1 
theory 
On liveness and fairness
[up to slide 100]

7t 
Wed 03/10 
1113 
X2 
theory 
Fairness assumptions [from slide 101]
and regular safety properties [up to slide 48]

8t 
Thu 04/10 
1618 
X1 
theory 
Verifying regular safety [from slide 49]

2e 
Fri 05/10 
1113 
N1 
exe 
Second
exercise sheet

9t 
Mon 08/10 
1416 
X1 
theory 
ωregular properties

3e 
Thu 11/10 
1618 
X1 
exe 
Checking exercises

10t 
Mon 15/10 
1416 
X1 
theory 
Model checking with Büchi automata
[up to slide 133]

11t 
Tue 16/10 
1113 
X1 
theory 
Syntax and semantics of linear temporal logic
[up to slide 216]

4e 
Fri 19/10 
1113 
X1 
exe 
Third
exercise sheet

12t 
Mon 22/10 
1416 
X1 
theory 
LTL formulas: normal forms and fairness
and some exercise checking

13t 
Thu 25/10 
1618 
X1 
theory 
Model checking with Büchi automata
[skipping from slide 209 up to slide 310]

5e 
Fri 26/10 
1416 
X3 
exe 
Fourth
exercise sheet + checking exercises

 
Fri 02/12 
1618 
L1 
exe 
Midterm

6e 
Fri 09/11 
1416 
X3 
exe 
Correction of midterm

14t 
Tue 13/11 
1113 
X1 
theory 
A survey on formal methods for validation and verification (by Roberto Bagnara)

15t 
Wed 14/11 
1113 
X2 
theory 
A gentle introduction to abstract interpretation (by Roberto Bagnara)

16t 
Thu 15/11 
1618 
X1 
theory 
Syntax and semantics of computational tree logic

17t 
Fri 16/11 
1416 
X3 
theory 
CTL vs LTL
and some model checking [up to slide 98]

18t 
Mon 19/11 
1416 
X1 
theory 
On the MISRA C coding standard (by Roberto Bagnara)

7e 
Fri 23/11 
1416 
X3 
exe 
Fifth exercise sheet

19t 
Mon 26/11 
1416 
X1 
theory 
Probabilistic model checking (by Mieke Massink)

20t 
Tue 27/11 
1113 
X1 
theory 
Model checking PCTL (by Mieke Massink)

21t 
Wed 28/11 
1113 
X2 
theory 
Mean field model checking population models (by Mieke Massink)

22t 
Thu 29/11 
1618 
X1 
theory 
Fair CTL [up to slide 64] and on CTL*

23t 
Mon 03/12 
1416 
X1 
theory 
Equivalences for transitions systems

24t 
Fri 07/12 
1416 
X3 
theory 
On quantified modal logics

8e 
Mon 10/12 
1416 
X1 
exe 
Recollecting thoughts
(and
sixth
exercise sheet)

25t 
Tue 11/12 
1113 
X1 
theory 
Topologics (by Vincenzo Ciancia)

26t 
Wed 12/12 
1113 
X2 
theory 
A tour on VoxLogica, and some experiments (by Vincenzo Ciancia)

27t 
Thu 13/12 
1618 
X1 
theory 
(by Vincenzo Ciancia)

9e 
Fri 14/12 
1416 
X3 
exe 
Scheduling the seminars and so on
