Model Checking

CS4138 TSJ14,

This course is concerned with model checking as formal verification technique. It touches on theoretical foundations, algorithms and different optimisation and application techniques.

Classically, model checking is the problem from formal logic of deciding whether a given structure is a model of, i.e., satisfies, a given formula from some logical language. Since the emerge of automated verification techniques based on logical specification languages, the term model checking is used in a broader sense for a set of frameworks and techniques that aim at automatic evaluation of a formalised correctness property on a system or an abstract model of it.


The course builds on theoretical foundations typically taught in undergraduate courses in computer science. Attendees are expected to be familiar with basics in

  • propositional and first-order (predicate) logic
  • formal languages and automata theory (regular languages, finite automata, computability and complexity)
  • computer programming, algorithms and data structures