Course Part I


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

Lecture:
Promela Introduction (WA)

Lecture:
SPIN Introduction, Verifying Assertions (WA)

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

Exercise:
Promela (AL)

Lecture:
Modeling Distribution (WA)

3. W 38 17/9  21/9 
Lecture:
Propositional and Temporal Logic (WA)

Exercise:
Channels, LTL and Model Checking (OA)

Lecture:
Temporal Model Checking part 1 (WA)

4. W 39 24/9  28/9 
Exercise:
Model Checking with SPIN (OA)

No lecture, no exercise

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

5/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 1/10  5/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 8/10  12/10 
Exercise:
FirstOrder + JML (OA)

Lecture:
Dynamic Logic part 1 (WA)

No lecture, no exercise

7. W 42 15/10  19/10 
Lecture:
Dynamic Logic part 2 (WA)

Exercise:
Dynamic Logic (AL)

Lecture:
Proof Obligations (WA)

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

Exercise:
Verification (AL)

Lab2 Questions Session (AL)

29/10 
Deadline Lab Assignment KeY

9. W 44 29/10  2/11 
Individual Oral Examination
