Model Checking, Summer semester 2012/2013

Department of Computer Sciences, University of Salzburg

Lecturer:      Dr. A. Sokolova, ana.sokolova"at"cs.uni-salzburg.at, office 2.17

Schedule:      Thursdays 10am-12am and 1pm-2pm in T06

First meeting:    Thursday, March 7 at 10am in T06

Language:      English
The course may also be taken by PhD students
Course description: Model checking is a technique for automatic verification of finite state concurrent systems such as sequential circuit designs and communication protocols. This method has advanced verification from a purely theoretical to an also practically applicable discipline. Its inventors Edmund M. Clarke, E. Allen Emerson, and Joseph Sifakis have been awarded the significant Turing award in 2007.

In this course we will learn the principles of model checking, namely modeling with transition systems, the temporal logics LTL and CTL, their comparison, as well as algorithms for verifying these logics. In addition, on the practical side, we will get acquainted with the basics of the SPIN model checker, one of the most commonly used model checking tools for automatic verification.
Literature: The books can be ordered via Amazon.de . Some copies are available at the department library.
Prerequisites: None, the course material is self-contained, as is the textbook. Knowledge of basics of theoretical computer science like logic for computer science or automata theory is an asset.
Exam: This is a VP course. There will be three exam possibilities in June/July/August. The exam is written consisting of several excersises from the material covered during the course. Additionally, the homeworks and the mini project will also contribute to the final grade.

Exam dates: t.b.a.

Mini projects: t.b.a.

Useful links for the mini projects:
Schedule: