This time table is tentative, and may be subject to change. If possible slides will be uploaded a day in advance; however, due to time constraints this may not always be possible.
Week | Contents (tentative) | Slides/Notes | References | ||
---|---|---|---|---|---|
1 |
Introduction, Predicate Logic, LTL CTL*, CTL, Expressiveness |
||||
2 |
Expressiveness of Logics Finite Automata Model Checking: Reachability and Safety CTL Model Checking Abstraction & Refinement |
||||
3 |
Abstraction & Refinement Assignment 0 Symbolic CTL Model Checking (1) |
||||
4 |
Binary Decision Diagrams Symbolic CTL Model Checking (2) Summary Tool: nuXmv |
||||
5 |
LTL Model Checking Tool: SPIN |
||||
6 |
Bounded Model Checking Tool: CBMC Predicate Abstraction Refinement Assignment 1 |
||||
7 |
Static Analysis Tool: Skink |
||||
8 |
Timed and Region Automata Timed Languages Assignement 2 |
||||
9 |
Timed Logics and Model Checking Tool: Uppaal Assignment 3 Closing Remarks |
||||
10 | no lectures | ||||
11 | Q/A, Assignment 4 | ||||
12 | Exam |