Model Checking, Summer semester 2009/2010

Department of Computer Sciences, University of Salzburg

Lecturer:      Dr. A. Sokolova, ana.sokolova"at", office 2.17

Schedule:      Tuesdays 10am-12am and 4pm-5pm in T06

First meeting:    Tuesday, March 2 at 4pm 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 . 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. 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: First possibility: Tuesday 6.7.2010, 10am, T06. Second possibility: Thursday 22.7.2010, 10am, T06. Third possibility: Tuesday 10.8.2010, 10am, T06.

Mini projects have been assigned, deadline for submitting a mini project is 1.8.2010

Useful links for the mini projects:

Results from the exam(s) and homeworks
Student ID Exam points (<= 100) HW points (*)(<= 11) Project points (<= 25) Mark (**) Exam date
****057 94 11 25 1 6.7.2010
****642 86 11 25 1 6.7.2010
****270 76 9 25 2 22.7.2010
****614 74 3 22 2 22.7.2010
****594 73 11 22 2 22.7.2010
****203 73 2 22 2 10.8.2010
****112 72 11 25 2 6.7.2010
****510 50 - 20 4 22.7.2010

(*) There were 11 homeworks. Each delivered homework counts as one HW point.
(**) Total = Exam points + HW points + Project points.