|
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
|