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
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
Literature:
-
•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)
-
•Textbook: Principles of Model Checking by Christel Baier and Joost-Pieter Katoen. MIT Press, 2008.
-
•The Spin Model Checker, Primer and Reference Manual, by Gerard J. Holzmann, Addison-Wesley, 2004.
-
•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: 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
Department of Computer Sciences
Austria
All information about the course will be given via Blackboard and Slack, channel #cav21 (see Plusonline, Blackboard)
