Model Checking

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:   https://www.uni-luebeck.de/index.php?id=6269&tx_webparser_pi1[modulid]=1060

Page on Moodle: https://moodle.uni-luebeck.de/course/view.php?id=3597

Prerequisites

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