|
Course Part I
|
|
Tuesdays 13:15-15:00
EA |
Thursdays 13:15-15:00
EA |
Fridays 13:15-15:00
EA |
1. W 35
28/8 - 1/9 |
Lecture:
Course Introduction (WA)
|
Lecture:
Promela Introduction (WA)
|
Lecture:
Safe and Secure Programming Using SPARK (AW)
SPIN Introduction, Verifying Assertions (WA)
|
2. W 36
4/9 - 8/9 |
Lecture:
Modeling Concurrency (WA)
|
Exercise:
Promela (AL)
|
Lecture:
Modeling Distribution (WA)
|
3. W 37
11/9 - 15/9 |
Lecture:
Propositional and Temporal Logic (WA)
|
Exercise:
Channels, LTL and Model Checking (RP)
|
Lecture:
Temporal Model
Checking part 1 (WA)
|
4. W 38
18/9 - 22/9 |
Exercise:
Model Checking with SPIN (RP)
|
No lecture, no exercise
|
Lecture:
Temporal Model Checking part 2
+ First-Order Logic (WA)
|
| 29/9 |
Deadline Lab Assignment Promela/SPIN
|
|
Course Part II
|
|
Tuesdays 13:15-15:00
EA |
Thursdays 13:15-15:00
EA |
Fridays 13:15-15:00
EA |
5. W 39
25/9 - 29/9 |
Lab1 Questions Session (RP)
|
Lecture:
Sequent Calculus, KeY prover,
Java Modeling Language part 1 (WA)
|
Lecture:
Java Modeling Language part 2 (WA)
|
6. W 40
2/10 - 6/10 |
Exercise:
First-Order + JML (RP)
|
Lecture:
Dynamic Logic part 1 (RP)
|
No lecture, no exercise
|
7. W 41
9/10 - 13/10 |
Lecture:
Dynamic Logic part 2 (WA)
|
Exercise:
Dynamic Logic (RP)
|
Lecture:
Proof Obligations (WA)
|
8. W 42
16/10 - 20/10 |
Lecture:
Verification of Method Calls and Loops (WA)
|
Exercise:
Verification (MC)
|
Lab2 Questions Session (MC)
|
| 23/10 |
Deadline Lab Assignment KeY
|
9. W 43
23/10 - 27/10 |
Individual Oral Examination
|