Formal Methods for Software Development TDA294/DIT271, LP1, HT2020
Lectures and Exercises

Times, Place, Content, Slides

The titles of the lectures and exercises are subject to change.

Copies of the lecture slides will be provided shortly after each lecture.

Exercises will be published before the first lecture on the topic of the exercise. After the exercise class we publish sketches of the solutions.

Teacher: WA = Wolfgang Ahrendt Teaching Assistant: AL = Andreas Lööw

Course Part I
Tuesdays 13:15-15:00 Thursdays 13:15-15:00 Fridays 13:15-15: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
+ First-Order Logic (WA) 		No lecture, no exercise
2/10 Deadline Lab Assignment Promela/SPIN
Course Part II
Tuesdays 13:15-15:00 Thursdays 13:15-15:00 Fridays 13:15-15: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:
First-Order + 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


W. Ahrendt, Oct 20, 2020