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 2016/2017
Schedule: Tuesdays 1:30pm-4am in T04 from 6.3.17 see calendar
First meeting: Tuesday, March 6 at 1:30pm in T04
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.
-
•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 HW 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 HW for corrections). It is not obligatory to hand in HW.
Exam dates: t.b.a..
Mini projects: t.b.a.
Useful links for the mini projects: SPIN course 1999, TU Eindhoven SPIN course 2009, TU Eindhoven
Schedule:
-
•Week 1, Tuesday 6.3.17, Introduction to verification methods and model checking in particular (Chapter 1 of all books), first meeting.
-
•Week 2, Tuesday 13.3.17, Modeling Systems (MC book, Chapter 2 with additional examples of modeling programs); LTS and Kripke structures; the algebraic structure of processes.
...
This webpage was not regularly updated because of a small number of students and hence informal communication was possible.
The course took place and was a pleasant experience for myself and the students.
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 is in collaboration with Igor Konnov, Georg Weissenbacher, and Josef Widder from TU Vienna. The course will be held in this shape at both universities.
Ana Sokolova
Dr. TU Eindhoven, The Netherlands, 2005
Associate Professor
Department of Computer Sciences
Austria
