Course: Advanced Model Checking
Schedule
- Course (Prof. Dr. Stefan Leue)
Monday 10:00 - 11:30 Room: PZ 801 Start: 15 Apr
Thursday 10:00 - 11:30 Room: PZ 901 Start: 18 Apr
- Tutorial (Martin Kölbl)
Wednesday 11:45 - 13:15 Room: PZ 901 Start: 24 Apr
Prerequesites
No special model checking knowledge is needed, all foundations will be taught in the course
Basic programming skills
Contents
The course will cover advanced topics in Model Checking. The course will introduce into CTL model checking and into the foundations of BDD based symbolic model checking. The course will further cover model checking of real-time and probabilistic systems.
The course Model Checking of Software and Systems is not a prerequisite for the successful completion of this course.
In the excercise, different model checking tools (CTL, symbolic, timed, probabilistic) will be used to solve different kinds of model checking problems. In order to be able to write code in the different model checking languages basic programming skills are necessary
Learning objectives
It is the objective of this course to enable students to assess and use the particular model checking technologies that will be presented in this course. The participants of this course will be enabled to use model checking technologies in practical problems and to estimate and anticipate the possibilities as well as the limitations of using this technology in practical systems engineering projects. The will also be enabled to chose adequate tool support for the solution of practical model checking problems.
Course literature
E. Clarke, O. Grumberg and D. Peled, Model Checking, MIT Press, 1999
C. Baier and J.-P. Katoen, Principles of Model Checking, MIT Press, 2008
Additional literature will be announced during the course.
Workload
70 hours, of which 84 hours are spent in class and 186 hours of self study.
Records of academic assessments
Oral (30 min) or written examination (90 min) at the end of the semester
Active participation in the excercises
Participants
Master-level course. Open to Bachelor-level students.
Remark
The course will be taught in English. All course materials will be in English.
Credits
SWS: 4+2
ECTS-points: 10