Formal Methods for Software Development TDA294/DIT272, LP1, HT2023

Lectures and Exercises

Times, Place, Content, Slides

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.

Course Part I
Tuesdays 13:15-15:00 in EA Thursdays 13:15-15:00 in EA Fridays 13:15-15:00 in EA
1. W 35
28/8 - 1/9
Lecture:
Course Introduction
Lecture:
Promela Introduction
Lecture:
SPIN Introduction
2. W 36
4/9 - 8/9
Lecture:
Modeling Concurrency
Exercise:
Promela (David)
Lecture:
Modeling Distribution
3. W 37
11/9 - 15/9
Lecture:
Propositional and Temporal Logic
Lecture:
Temporal Model Checking with SPIN
Exercise:
Channels, LTL and Model Checking (David)
4. W 38
18/9 - 22/9
Exercise:
Model Checking with SPIN (David)
Lecture:
Temporal Model Checking: Theory
Lecture:
First-Order Logic, Sequent Calculus
29/9 Deadline Lab Assignment Promela/SPIN
Course Part II
Tuesdays 13:15-15:00 in EA Thursdays 13:15-15:00 in EA Fridays 13:15-15:00 in EA
5. W 39
25/9 - 29/9
Lecture:
Java Modeling Language part 1
Lecture:
Java Modeling Language part 2
Dynamic Logic part 1

Exercise:
First-Order + JML (Guilherme)
6. W 40
2/10 - 6/10
Lecture:
Dynamic Logic part 2
Lecture:
Proof Obligations
No lecture, no exercise
(Blocked, Re-exam period)
7. W 41
9/10 - 13/10
Exercise:
Dynamic Logic (Guilherme)
Lecture:
Verification of Method Calls and Loops
No lecture, no exercise
8. W 42
16/10 - 20/10
Exercise:
Verification (Guilherme)
No lecture, no exercise
Lab2 Questions Session (online)
23/10 Deadline Lab Assignment KeY
W 43+44
22/10 - 03/11

Individual Oral Examination



W. Ahrendt