Formal Methods for Software Development

TDA294/DIT271, LP1, HT2017

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.

Welcome to the first lecture on Tuesday, August 29, at 13:15 in room EA.

Teacher:

Teaching Assistants:

Guest Lecturer:

Course Part I
	Tuesdays 13:15-15:00 EA	Thursdays 13:15-15:00 EA	Fridays 13:15-15: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 + First-Order Logic (WA)
29/9	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 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: First-Order + 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

W. Ahrendt, Oct 17, 2017