Course Part I


Tuesdays 13:1515:00 EA 
Thursdays 13:1515:00 EA 
Fridays 13:1515: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
+ FirstOrder Logic (WA)

29/9 
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 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:
FirstOrder + 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
