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
|