Jakob-Haringer-Str. 2

5020 Salzburg, Austria

Room 2.17


+43 (0)662 8044 6417

+43 (0)662 8044 611 (fax)

Skype ana_sokolova

Many thanks to Silviu Craciunas for the photo (RTAS 2010 in Stockholm) and his help with iWeb!

Computer Aided verification (CAV), Summer semester 2020/2021

Schedule:            Thursdays 9:30am-12noon see calendar

First meeting:       Friday, March 5 at 10am (only this meeting on Friday)

Language:           English

The course may also be taken by PhD students


  1. Textbook: Model Checking, by Edmund M. Clarke, Orna Grumberg, and Doron A. Peled, MIT Press, 1999. [MC]

        (new 2018 edition available, co-authored also by Daniel Kroening and Helmut Veith)

  1. Textbook: Principles of Model Checking by Christel Baier and Joost-Pieter Katoen. MIT Press, 2008.

  1. The Spin Model Checker, Primer and Reference Manual, by Gerard J. Holzmann, Addison-Wesley, 2004.

  1. Principles of the Spin Model Checker, by Mordechai Ben-Ari, Springer, 2008.

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 2VO+1PS course. For the lectures part (VO), 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. For the practical part (PS), there will be mini projects to complete during the summer.

In addition, I give homework in class from time to time. This is to help you estimate your progress, and possibly provide you with feedback (if you hand in the homework for corrections). It is not obligatory to hand in homework.

Exam dates: t.b.a. (all announceents via Blackboard and Slack)

Mini projects: t.b.a. (all announceents via Blackboard and Slack)

Useful links for the mini projects:  SPIN course 1999, TU Eindhoven   SPIN course 2009, TU Eindhoven

Course description: This is a course on the foundations and state-of-the-art techniques and tools for automated verification. The most successful such technique is model checking of finite-state concurrent systems such as sequential circuit designs and communication protocols. Model checking 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, temporal logics, as well as algorithms for verifying these logics. In addition, on the practical side, we will get acquainted with tools that implement particular model checking algorithms.

This is a remake of my model checking course, re-designed to incorporate up-to-date techniques and tools. The reconstruction was done in collaboration with Igor Konnov, Georg Weissenbacher, and Josef Widder from TU Vienna. The course was held in this shape at both universities.

Ana Sokolova

Dr. TU Eindhoven, The Netherlands, 2005

Associate Professor

Computational Systems Group

Department of Computer Sciences

University of Salzburg


All information about the course will be given via Blackboard and Slack, channel #cav21 (see Plusonline, Blackboard)