Course Part I


Tuesdays 13:1515:00 
Thursdays 13:1515:00 
Fridays 13:1515:00 
1. W 36 31/8  4/9 
Lecture:
Course Introduction (WA)

Lecture:
Promela Introduction (WA)

Lecture:
SPIN Introduction, Verifying Assertions (WA)

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

Exercise:
Promela (AL)

Lecture:
Modeling Distribution (WA)

3. W 38 14/9  18/9 
Lecture:
Propositional and Temporal Logic (WA)

Exercise:
Channels, LTL and Model Checking (AL)

Lecture:
Temporal Model Checking part 1 (WA)

4. W 39 21/9  25/9 
Exercise:
Model Checking with SPIN (AL)

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

No lecture, no exercise

2/10 
Deadline Lab Assignment Promela/SPIN

Course Part II


Tuesdays 13:1515:00 
Thursdays 13:1515:00 
Fridays 13:1515:00 
5. W 40 28/9  2/10 
Lab1 Questions Session (AL, WA)

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

Lecture:
Java Modeling Language part 2 (WA)

6. W 41 5/10  9/10 
Exercise:
FirstOrder + JML (AL)

Lecture:
Dynamic Logic part 1 (WA)

No lecture, no exercise

7. W 42 12/10  16/10 
Lecture:
Dynamic Logic part 2 (WA)

Exercise:
Dynamic Logic (AL)

Lecture:
Proof Obligations (WA)

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

Exercise:
Verification (AL)

Lab2 Questions Session (AL, WA)

26/10 
Deadline Lab Assignment KeY 
9. W 44 26/10  30/10 
Individual Oral Examination
