Course: Advanced Model Checking
Schedule:
- Course (Prof. Dr. Stefan Leue)
Tuesday 10:00 - 11:30 Room: PZ 901 Start: 21 Apr 2020
Thursday 10:00 - 11:30 Room: PZ 901 Start: 23 Apr 2020
- Tutorial (Fabian Marquart)
Monday 15:15 - 16:45 Room: PZ 901 Start: 27 Apr 2020
Description:
Teaching methods
During the summer term 2020 this course will be offered as an online course!
The currently pursued approach is as follows. For every 90 minute lecture, a recording of this lecture in English language from a previous term will be made available to participants. During the final 30 minutes of the regular lecture slot (i.e., Tuesdays and Thursdays 11:00 - 11:30) there will be an online Question and Answer-Session conducted through an electronic conference tool. It is essential that all participants have watched the respective lecture recording and have prepared questions before the Q&A session starts.
The first lecture, which will be devoted to the organization of the course, will be held on Thursday, April 23, 10:00-11:30 via a video conferencing tool. The lecture on Tuesday, April 21 is cancelled!
We will make further information (in particular, the access information for the first lecture) available by email. To send email to participants we will use the email functionality of ILIAS. It is therefore essential that all participants register for this course not only in ZEuS, but also in Ilias.
I am aware that this course format is a new experience for most of us. I ask everyone to be flexible in dealing with potential imperfections. However, I am convinced that this hybrid asynchronous and synchronous approach to teaching this course will lead to excellent learning experiences and results. I am looking forward to delivering this course to you!
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.
Course material
The course material, for instance, lecture slides and exercises will be published on Ilias.
Workload
270 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: 9