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!

Computer Aided verification (CAV), Summer semester 2018/2019

Schedule:            Thursdays 10am-1pm in T06 from 7.3.19 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. [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 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 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: July 12, 2019, 10am in T04.


Mini projects: The mini projects have been assigned, the deadline is August 25, 2019.


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

Schedule:


  1. •Week 1, Thursday 7.3.19, Introduction to verification methods and model checking in particular, first meeting. We also started with models and modeling techniques. Please read Chapter 1 of all books.

  2. •Week 2, Thursday 14.3.19, Some more material on modeling programs, and we started with temporal logics: CTL* and just a brief intro to LTL using these slides or the version with all stages of built. Please read Chapter 2 and Section 3.1 of [MC].

  3. •Week 3, Thursday 21.3.19, We continued with detailed introduction of LTL and CTL, and discussed the comparison/expressivity of different temporal logics. We also learned about fairness, and strongly connected components (Tarjan’s algorithm) as preparation to CTL model checking. Please read Sections 3.2 and 3.3 of [MC].

  4. •Week 4, Thursday 28.3.19, CTL model checking: the explicit-state algorithm; CTL model checking with fairness; we started discussing fixed points towards symbolic model checking of CTL. Please read Section 4.1 of [MC].

  5. •Week 5, Thursday 4.4.19, We discussed fixed points in detail (and proved all necessary results), as well as fixed-point characterisation of CTL, and the symbolic algorithm. We started discussing OBDDs, but will need to still continue next time. Please read Section 6.1, 6.2, and parts of Section 5.1 from [MC].

  6. •Week 6, Thursday 11.4.19, OBDDs, Bryant’s reduction procedure, examples, fair symbolic model checking CTL, counter-examples and witnesses. Please read Section 5.1, 5.2, as well as Section 6.3 and 6.4 from [MC].

  7. •Week 7, Thursday 9.5.19, We started with the automata-based algorthm for model checking LTL, in particular we: recalled LTL, described the very high-level algorithm steps, learned Büchi automata, turning a Kripke structure into a Büchi automaton, discussed intersection and complementing Büchi automata (some bits on complementation we will still discuss next time too). Please read Section 9.1 and 9.2 from [MC].

  8. •Week 8, Thursday 16.5.19. We continued with the discussion of complementing Büchi automata, generalized Büchi automata, the algorithm for checking emptiness based on double DFS, and started discussing the translation of LTL formulas into Büchi automata (the needed data structures and part of the algorithm). Please read Section 9.3 and (parts of ) 9.4 from [MC].

  9. •Week 9, Thursday 23.5.19. We clarified the algorithm for translating LTL to generalized Büchi automata in detail and looked at multiple examples. The presentation of the algorithm and everything around it is much better in the new edition of the MC book.
    Please read the rest of Section 9.4 from [MC] as well as Chapter 7 from the new edition of the book.

  10. •Week 10, Thursday 13.6.19. We learned the mu-calculus: syntax, semantics, examples, naive algorithm, and the Emerson-Lei algorithm. Please read Chapter 7 from [MC].

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

Austria


anas@cs.uni-salzburg.at

Timing:   We aim at 10 meetings of 3 full hours each, as some of the Thursdays in this semestar we will not meet due to my traveling.  Therefore, we start at 10:00 sharp, and end either at 1pm sharp or at 1:15pm with a break of 15 minutes in between.