The course is about the theory of model checking. Model checking is a static verification technique that allows one to check whether an abstraction of a system (for instance: hardware, software or protocol) has a specified property.
In this course we cover:
- Transition Systems
- Linear Temporal Logics (LTL), Computation Tree Logic (CTL) and Timed Computation Tree Logic (TCTL)
- Model checking techniques to verify whether a given transition system has a property specified in LTL, CTL or TCTL
- Partial-order reduction techniques to optimize model checking