Term 1, 2020
Course Schedule
This is a tentative course schedule, which will evolve during the semester.
| Week | Topic | Homeworks | Lecturer |
| 1 | Course Overview, Automata, Logic and Models, Temporal Logic | Liam | |
| 2 | Expressiveness, CTL Model Checking, Linear Behaviours, Safety and Liveness | Homework 0 Released | Liam |
| 3 | Büchi Automata, LTL Model Checking, Tool: Spin, Homework 0 Solutions | Homework 0 Due | Liam |
| 4 | Simulation and Bisimulation, Abstraction Refinement, Predicate Abstraction | Homework 1 Released | Liam |
| 5 | Static Analysis, Abstract Interpretation, Tool: Skink, Homework 1 Solutions | Homework 1 Due | Liam |
| 6 | Recap, Break (1 Lecture) | Homework 2 Released | Liam |
| 7 | Break (1 Lecture), Symbolic Model Checking | Homework 2 Due | Rob |
| 8 | Symbolic MC Continued, Binary Decision Diagrams | Homework 3 Released | Rob |
| 9 | Timed Automata, Region Automata, Timed Languages, Timed Logics | Homework 3 Due | Miki |
| 10 | Model Checking Timed Automata, Tool: Uppaal | Homework 4 Released | Miki |
| 11 | Wrap-up | Homework 4 Due | Miki and Rob |
\(\;\)
NOTE: I am putting up my lecture slides. However, these slides are not a complete representation of the material covered in the lectures, and they are no substitute for attending the lectures. I am supplying a lot of information during the lecture that is not on the slides (verbally, on the whiteboard, on the overhead projector, and by coding live). It is your duty to ensure that you are aware of and study that extra material by attending the lectures and making your own notes. The extra information that I supply in the lecture is examinable.