|
Course Part I
|
|
Tuesdays 13:15-15:00
EA |
Thursdays 13:15-15:00
EA |
Fridays 13:15-15:00
EA |
1. W 35
29/8 - 2/9 |
Lecture:
Course Introduction
(WA)
|
Lecture:
Promela Introduction (WA)
|
Lecture:
SPIN Introduction, Verifying Assertions (WA)
|
2. W 36
5/9 - 9/9 |
Lecture:
Modeling Concurrency (WA)
|
Exercise:
Promela
(MC)
|
Lecture:
Modeling Distribution (WA)
|
3. W 37
12/9 - 16/9 |
Lecture:
Propositional and Temporal Logic (WA)
|
Exercise:
Channels,
LTL and Model Checking (RP)
|
Lab FAQ Session (MC, RP)
|
4. W 38
19/9 - 23/9 |
Lecture:
Temporal Model Checking (WA)
|
Exercise:
Model
Checking with SPIN (RP)
|
(no Lecture, no Exercise)
|
| 30/9 |
Deadline Lab Assignment Promela/SPIN
|
|
Course Part II
|
|
Tuesdays 13:15-15:00
EA W 39,40,41; EC W 42 |
Thursdays 13:15-15:00
EA W 39,40,41; EC W 42 |
Fridays 13:15-15:00
EA |
5. W 39
26/9 - 30/9 |
Lecture:
First-Order Logic (WA)
|
Lecture:
Java Modeling Language part 1 (WA)
|
Lecture:
Java Modeling Language part 2 (WA)
|
6. W 40
3/10 - 7/10 |
Exercise:
First-Order + JML (MC)
|
Lecture:
Dynamic Logic part 1 (WA)
|
(no Lecture, no Exercise)
|
7. W 41
10/10 - 14/10 |
Lecture:
Dynamic Logic part 2 (MC)
|
Exercise:
Dynamic Logic (MC)
|
Lecture:
Proof Obligations (MC)
|
8. W 42
17/10 - 21/10 |
Lecture in EC:
Verification with KeY (WA)
|
Exercise in EC:
Verification (RP)
|
Lab FAQ Session (MC, RP)
|
| 24/10 |
Deadline Lab Assignment KeY
|
| 28 October 2016 |
Exam - 2.00 pm in TBA
|