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


Copyright 2015—2019