Model Checking
Prof. Dr. Christel Baier and Dr. Sascha Klüppelholz
SWS: (4/4/0), in English
Description
Model Checking is a fully automatic verification method for reactive systems. This course provides an introduction to the main principles of model checking:
- modeling reactive systems by transition systems
- linear time properties and Büchi automata
- linear temporal logic and automata-based model checking
- computation tree logic
and selected topics of:
- bisimulation and simulation relations
- probabilistic and timed automata
- partial order reduction, symbolic model checking
Registration
Enrolling via OPAL is required until October 11th 2021.
Dates
Thu | 2. and 3. time slot | [09:20 am – 12:40 pm] |
Fri | 2. and 3. time slot | [09:20 am – 12:40 pm] |
There will be no fixed assignment of the lectures and exercises to time slots. The schedule for the lectures and tutorials will be announced every week.
The course consists of a (4/2/0) lecture with exercises for the theoretical foundations (October – December) and an introduction to model checkers with practical exercises (0/2/0) (January).
Prerequisites
For the course, basic knowledge on algorithms, complexity theory, automata theory and logic is presumed.
Creditability
Bachelor Informatik
Master Informatik
Diplom Informatik
Master Computational Logic
- MCL-TCSL: Theoretical Computer Science and Logic
Master Computational Modeling and Simulation
- CMS-LM-MOC: Foundations of Logical Modeling
- CMS-LM-ADV: Foundations of Logical Modeling
Literature
The course follows the book “Principles of Model Checking” (C. Baier, J.P. Katoen, Principles of Model Checking, MIT Press) closely. This book is available at the SLUB (Lehrbuchsammlung).
Contact
Dr. Sascha Klüppelholz
Send encrypted email via the SecureMail portal (for TUD external users only).