Software Engineering using
Formal Methods		 TDA293/DIT270, LP1, HT2011
Schedule

Places and Times

We have lectures every week on Tuesdays between 13:15 and 15:00 and on Wednesdays between 10:00 and 11:45.

There are exercise classes on Fridays between 10:00 and 11:45. The exercises won't necessarily last two hours, but we reserved a larger slot, just in case.

The schedule shown below is subject to change. Copies of the slides will be provided shortly after each lecture.

If you have any general questions regarding the course, please send them to our Google group (instructions for accessing the group are here).

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

Teachers: WA = Wolfgang Ahrendt RB = Richard Bubel WM = Wojciech Mostowski RE = Ramona Enache GP =Gabriele Paganelli

Lecture
Tuesdays 13:15-15:00
EA		 Lecture
Wednesdays 10:00-11:45
EA		 Exercises
Fridays 10:00-11:45
EB
1. W 35
29/8 - 2/9		 Course Introduction (WA) Promela
Introduction (RB) 		No Exercises
2. W 36
5/9 - 9/9		 SPIN Introduction
Verifying Assertions (WM) 		Modeling
Concurrency (WM) 		Promela (RE)
3. W 37
12/9 - 16/9		 Modeling
Distribution (RB) 		Propositional and Temporal Logic (RB) Channels, LTL and Model Checking (GP)
4. W 38
19/9 - 23/9		 Temporal Model Checking (RB) First-Order Logic (RB) Model Checking with SPIN (GP)
26/9 Deadline Lab Assignment Promela/SPIN
5. W 39
26/9 - 30/9		 Java Modeling
Language part 1 (WM) 		Java Modeling
Language part 2 (WM) 		First-Order + JML (RE)
6. W 40
3/10 - 7/10		 Dynamic Logic part 1 (WA) Dynamic Logic part 2 (WA) Dynamic Logic (GP)
7. W 41
10/10 - 14/10		 Proof Obligations (WM)
Advanced Verification with KeY (WM) Verification (RE)
17/10 Deadline Lab Assignment KeY
21/10 Exam


Home | Course | Schedule | Exam | Exercises | Labs | Eval | Tools W. Ahrendt R. Bubel W. Mostowski , Sep 15, 2011