Informatik an der TU Clausthal > Abteilungen > Computational Intelligence > Computational Intelligence > Teaching > Winter 2012/13 > Verification of Concurrent Systems (Verifikation von Parallelen Systemen) (MSc)

**Lecturer**:

Dr. Nils Bulling**About this course: **

The course is a master course. It is a 6 ECTS course with 3+1 hours a week (3 lectures/labs, 1 exercise/lab class). Exercises/labs are mandatory.**Times:**

-Monday 13:00-15:00 o’clock, Seminarraum 210, Am Regenbogen 15

-Wednesday 13:00-15:00 o’clock, Seminarraum 210, Am Regenbogen 15

-The first lecture takes place October, 15th.**Prerequisites**:

- All students have to register in the StudIP-System.

- Oral exams will be offered at the end of the lecture.

- In order to be permitted to the exam, in average 60% of all exercise sheet have to be solved successfully.

- Informatics 1-3

- more details are coming soon...

**Contents of the course**:

Model checking is a technique for verifying whether a model of a system (e.g. of a hardware or software system) meets a given specification. The aim of this course is to give an introduction to various aspects of model checking concurrent systems. This course teaches how concurrent systems can be modeled by transitions systems, how linear-time properties (e.g. safety, liveness, and fairness properties) can serve as system specifications, and how this connects to automata on infinite objects. The linear-time temporal logic LTL and the computation tree logics CTL and CTL* are discussed as specification languages. The course also covers symbolic model checking and equivalence/abstraction techniques. These techniques are used with models of (real world) problems which are too large to consider them explicitly. In the course we also make use of model checking tools.**Literature**:

- Christel Baier and Joost-Pieter Katoen. Prinicples of Model Checking, MIT Press

- tba