Model Checking

Course Content

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