Address

Jakob-Haringer-Str. 2

5020 Salzburg, Austria


Room 2.17


Phone

+43 (0)662 8044 6417

+43 (0)662 8044 611 (fax)


Skype ana_sokolova

Home

Papers

Talks

Teaching

Personal

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

Model Checking, Summer semester 2012/2013

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

from 11.4.2013 on, Thursdays 9am - 12am (sharp) in T06 see calendar


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


Language:           English

The course may also be taken by PhD students

Literature:


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


  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 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 homework and the mini project will also contribute to the final grade.


Exam dates: discussed in class/via email


Mini projects: discussed in class/via email


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

Schedule:


  1. •Week 1, Thursday 7.3.13, Introduction to Model Checking (Chapter 1 of all books), first meeting.

  2. •Week 2, Thursday 14.3.13, More introduction, some modeling, CTL* (MC book Chapter 2 and Section 3.1, p. 13-30, PMC book 26-88, browse)


        (no classes for a while -- traveling and Easter break, see calendar)

  1. •Week 3, Thursday 11.4.13, LTL and CTL, fairness (MC book Section 3.2 and 3.3, p. 30-35, browse through Chapter 5 and 6 of the PMC book)

  2. •Week 4, Thursday 18.4.13, Strongly connected components, CTL model checking algorithm (with fairness) (MC book 35-41, SIAM Journal of Computing 1(2) 1972 for Tarjan’s algorithm)

  3. •Week 5, Thursday 25.4.13, Towards symbolic model checking of CTL formulas: Fixed points, predicate transformers, monotonicity, symbolic model checking algorithm (MC book 60-68)

  4. •Week 6, Thursday 2.5.13, OBDDs, fair symbolic model checking CTL, counterexamples and witnesses (MC book 50-59 and 68-75, look also at the ALU example MC book 75-87)


        (no class on 9.5.13 -- holiday)

  1. •Week 7, Thursday 16.5.13, Model checking LTL, automata based approach, properties of Buechi automata, checking emptiness (MC book 121-132)

  2. •Week 8, Thursday 23.5.13, Translating LTL into automata, examples (MC book 132-138)

  3. •Week 9, Wednesday 29.5.13 (as Thursday 30.5. was a holiday), Model checking mu-calculus (MC book 97-105 and 107-108)

  4. •Week 10, Tuesday 4.6.13 (due to traveling on Thursday 5.6.), State space reduction via equivalences and preorders (MC book 171-180)


Due to the very small number of students this semester and our traveling/timing constraints, the schedule deteriorated. We had full 3 hours per session (180 min), scheduled additional sessions out of the scheduled hours, and finished the planned material in 10 sessions.

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.

Ana Sokolova

Dr. TU Eindhoven, The Netherlands, 2005


Associate Professor


Computational Systems Group

Department of Computer Sciences

University of Salzburg

Austria


anas@cs.uni-salzburg.at