Software Engineering using
Formal Methods
TDA293/DIT270, LP1, HT2015

Schedule

Places and Times

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, September 1, at 13:15 in room EA.

Teacher: WA = Wolfgang Ahrendt Teaching Assistants: MC =Mauricio Chimento RP =Raúl Pardo
Additional Lecturer: GS = Gerardo Schneider

Course Part I
Tuesdays 13:15-15:00
EA
Thursdays 13:15-15:00
EA
Fridays 13:15-15:00
EA
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 (MC)
Lecture:
Modeling Distribution (WA)
3. W 38
14/9 - 18/9
Lecture:
Propositional and Temporal Logic (GS)
Exercise:
Channels, LTL and Model Checking (RP)

Lab FAQ Session (MC, RP)
4. W 39
21/9 - 25/9
Lecture:
Temporal Model Checking (WA)
Exercise:
Model Checking with SPIN (RP)
(see Part II)
2/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
4. W 39
21/9 - 25/9
(see Part I) (see Part I) Lecture:
First-Order Logic (WA)
5. W 40
28/9 - 2/10
Lecture:
Java Modeling Language part 1 (WA)
Lecture:
Java Modeling Language part 2 (WA)
Exercise:
First-Order + JML (MC)
6. W 41
5/10 - 9/10
Lecture:
Dynamic Logic part 1 (WA)
Lecture:
Dynamic Logic part 2 (WA)
Exercise:
Dynamic Logic (RP)
7. W 42
12/10 - 16/10
Lecture:
Proof Obligations (WA)
Lecture:
Verification with KeY (WA)
Exercise:
Verification (MC)
Wrap Up
Monday 19/10 12:00-13:00
EA
Lab FAQ Session (MC, RP)
Monday 26/10 10:00-12:00
EB
Open Session (MC, RP)
26/10 Deadline Lab Assignment KeY
30 October 2015 Exam - 2.00 pm in Hörsalsvägen



Home | Course | Schedule | Exam | Exercises | Labs | Eval | Tools W. Ahrendt , Oct 22, 2015