Course: Advanced Model Checking

Schedule

  • Course (Prof. Dr. Stefan Leue)
    Monday    10:00 - 11:30  Room PZ 801
    Thursday  10:00 - 11:30  Room PZ 901
  • Tutorial (Alina Bey) 
    Wednesday  11:45 - 13:15  Room: PZ 901

Description

Contents

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 11.

Participants

  • Bachelor and Master students
  • Offering suitable for participants from other programs and pubject areas

Subject Area

Informatik der Systeme / Angewandte Informatik

Prerequisites

  • 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.

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.

Credit Requirements

  1. Oral or written examination at the end of the semester
  2. Active participation in the excercises

Credits: 10

SWS: 4+2

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.