Course: Advanced Model Checking

Schedule

Course (Prof. Dr. Stefan Leue)

Monday 11:45 - 13:15h Room: PZ901
Thursday 10:00 - 11:30h Room: PZ901

Tutorial (Alina Bey<link>)

Thursday 11:45h - 13:15h Room: Z1003

Description

All materials are available through the Ilias-Website.

Registration is done using your university e-mail account.
The password will be presented in the first session on April 13th.

Participants

Bachelor and Master students.

Subject Area

Informatik der Systeme / Angewandte Informatik

Offering Suitable for Participants from Other Programs and Subject Areas

All

Prerequisites

A good undergraduate level knowledge of automata theory, algorithmics and logic.
No special model checking knowledge is needed, all foundations will be taught in the course
Basic programming skills

Contents / Syllabus

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 CTL model checking. The course will further cover model checking of real-time and probabilistic systems. 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.

The course will be taught in English. All course materials will be in English.

Credits

SWS: 6
ECTS-points: 10

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: Advanced Model Checking