Course Part I


Tuesdays 13:1515:00 EA 
Thursdays 13:1515:00 EA 
Fridays 13:1515:00 EA 
1. W 36 2/9  6/9 
Lecture:
Course Introduction (WA)

Lecture:
Promela Introduction (WA)

Lecture:
SPIN Introduction, Verifying Assertions (WA)

2. W 37 9/9  13/9 
Lecture:
Modeling Concurrency (WA)

Exercise:
Promela (AL)

Lecture:
Modeling Distribution (WA)

3. W 38 16/9  20/9 
Lecture:
Propositional and Temporal Logic (WA)

Exercise:
Channels, LTL and Model Checking (OA)

Lecture:
Temporal Model Checking part 1 (WA)

4. W 39 23/9  27/9 
Exercise:
Model Checking with SPIN (OA)

No lecture, no exercise

Lecture:
Temporal Model Checking part 2 + FirstOrder Logic (WA)

4/10 
Deadline Lab Assignment Promela/SPIN

Course Part II


Tuesdays 13:1515:00 EA 
Thursdays 13:1515:00 EA 
Fridays 13:1515:00 EA 
5. W 40 30/9  4/10 
Lab1 Questions Session (AL, OA)

Lecture:
Sequent Calculus, KeY prover, Java Modeling Language part 1 (WA)

Lecture:
Java Modeling Language part 2 (WA)

6. W 41 7/10  11/10 
Exercise:
FirstOrder + JML (OA)

Lecture:
Dynamic Logic part 1 (AL)

No lecture, no exercise

7. W 42 14/10  18/10 
Lecture:
Dynamic Logic part 2 (WA)

Exercise:
Dynamic Logic (AL)

Lecture:
Proof Obligations (WA)

8. W 43 21/10  25/10 
Lecture:
Verification of Method Calls and Loops (WA)

Exercise:
Verification (AL)

Lab2 Questions Session (AL, OA)

28/10 
Deadline Lab Assignment KeY

9. W 44 28/10  1/11 
Individual Oral Examination
