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:            Tuesdays 9am-12am in T05 from 10.3.15 see calendar


First meeting:       Tuesday, March 3 at 1pm 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: Monday, July 13, 5pm.


Mini projects: Discussed in class. Deadline for the miniprojects Tuesday, September 15.


Homework feedback and discussion: Thursday, June 18, 1pm (in my office).


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

Schedule:


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

  2. •Week 2, Tuesday 10.3.15, Modeling Systems (MC book, Chapter 2 except Section 2.2.1 which we will cover next week). 

  3. •Week 3, Tuesday 17.3.15, (Modeling continued, and) Temporal logics, CTL*, LTL and CTL. (MC book, Section 2.2.1, and Chapter 3 -- we looked at examples and proved some interesting properties, PMC book browse through Chapter 5 and 6)

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

  4. •Week 4, Tuesday 14.4.15, Still a bit on CTL (alternative definition, interesting proofs), ACTL, ACTL*, a detailed example. Strongly connected components. (Most of what we did today is not to be found in the MC book, we looked in-depth into things of Chapter 3; SIAM Journal on Computing 1 (2) 1971 for Tarjan’s algorithm).

  5. •Week 5, Tuesday 21.4.15, Model checking CTL, fairness (MC book, Section 3.3. and Section 4.1)

  6. •Week 6, Tuesday 28.4.15, Model checking fair CTL continued, towards symbolic MC of CTL: fixpoints -- most of what we did today is not exactly in the book (still, please read MC book, Section 4.1.1, Chapter 5, and Section 6.1. until page 63)

  7. •Week 7, Tuesday 5.5.15, Unusual class -- instead the regular lecture, everyone attended the morning session of AVM 2015 (which happened to be mainly on Model Checking :-)).

  8. •Week 8, Tuesday 12.5.15, Towards symbolic model checking CTL, fixpoint representations, properties, OBDDs. (MC book Section 6.1 and 6.2, pages 60-68 and Chapter 5, pages 51-59).

  9. •Week 9, Tuesday 19.5.15, Fairness in symbolic model checking; counter examples and witnesses; model checking LTL - the big picture. (MC book Section 6.3 and 6.4 -- please also read Section 6.5 and 6.6 -- pages 68-87 and a bit of Chapter 9, next time more).

  10. •Week 10, Tuesday 2.6.15, Model checking LTL, automata on finite and infinite words (MC book Chapter 9 until Section 9.2.2 -- pages 121-128).

  11. •Week 11, Tuesday 9.6.15, Still some constructions on Buechi automata, translating LTL formulas to Buechi automata (started). (MC book pages 128-134 with additional things covered in class -- please also read all of Section 9.4. to be discussed next time).

  12. •Week 12, Tuesday 16.6.15, LTL formulas to Buechi automata (detailed comprehensive lecture with proofs of correctness and examples). (MC book Section 9.4., and a Wikipedia article -- handouts given in class).

  13. •Week 13, Tuesday 30.6.15, Model Checking Fault-tolerant Distributed Algorithms, guest lecture by Josef Widder (TU Vienna). Download slides class 1, class 2, class 3 .

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