Formal Methods for Software Development TDA294/DIT271, LP1, HT2018

Schedule

Places and Times

The titles of the lectures shown below are preliminary and subject to change.

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

Teacher: WA = Wolfgang Ahrendt Teaching Assistants: AL = Andreas Lööw OA = Oskar Abrahamsson

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



Home | Course | Schedule | Exam | Exercises | Labs | Eval | Tools W. Ahrendt, Oct 23, 2018