Model Checking

CS4138 TSJ14,

This course is concerned with model checking as a 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 emergence 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.

Page in Modulhandbuch:[modulid]=1060

Page on Moodle:


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

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