Model Checking, Summer semester 2008/2009

Department of Computer Sciences, University of Salzburg

Lecturer:      Dr. A. Sokolova, ana.sokolova"at"cs.uni-salzburg.at, office 2.17 (maybe sometimes Prof. C.M. Kirsch)

Schedule (NEW as of 23.3.09):      Thursdays 10am-12am in T06 and 1pm-2pm in T04

First meeting:    Tuesday, 3.3.2009, 3pm, room T02

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 should be available at the department library in March.
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. (mini project = 25 points, homeworks = 11 points, exam = 100 points)

Exam dates: First possibility: Thursday 2.7.2009, 10am, T06. Second possibility: Monday 13.7.2009, 2pm, T06. Third possibility: Tuesday 25.8.2009, 2pm, T06.

Mini projects:
(1) OBDDs, Bryant's work and extensions, implementation details (theoretical mini project) - Tobias Berka
(2) Model checking garbage collection with SPIN - Andreas Haas
(3) Model checking a security protocol with SPIN - Stefan Jenisch and Stefan Lukesch
(4) Model checking non-blocking data structures with SPIN - Andreas Schoenegger
(5) Logic(s) for probabilistic model checking (theoretical mini project) - Silviu Craciunas

The deadline for completing the mini projects is 15.7.2009. Each student should submit a concise description of the project and the results (up to 5 pages of text).
Schedule:
Results from the exam(s) and homeworks
Student ID Exam points (<= 100) HW points (*)(<= 11) Project points (<= 25) Mark (**) Exam date
****240 85 - 25 1 2.7.9
****949 88 9 25 1 2.7.9
****259 51 - 23 3 2.7.9
****929 44 5 20 3 2.7.9
****307 31 - 23 4 25.8.9
(*) There were 11 homework tasks. Each delivered homework task counts as one HW point.
(**) Total = Exam points + HW points + Project points. The final mark is determined as follows: 1 if Total >= 105, 2 if 85 <= Total <= 104, 3 if 65 <= Total <= 84, 4 if 50 <= Total <= 64, 5 otherwise.