Model Checking, Summer semester 2012/2013
Lecturer: Dr. A. Sokolova, ana.sokolova"at"cs.uni-salzburg.at, office 2.17
Schedule: Thursdays 10am-12am and 1pm-2pm in T06
First meeting: Thursday, March 7 at 10am in T06
The course may also be taken by PhD students
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.
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 homeworks and the
mini project will also contribute to the final grade.
Exam dates: t.b.a.
Mini projects: t.b.a.
Useful links for the mini projects:
- Week 1, Thursday 7.3.13: Introduction to Model Checking (Chapter 1 of
all books), first meeting.