VERIFICATION

Audience

This core lecture (Stammvorlesung) addresses Bachelor and Master students in Computer Science, Bioinformatics, CuK or Computerlinguistics. Bachelor students must have passed the base lecture Programming 1. The lectures Math 1 and 2, Programming 2, and Theoretical Computer Science are recommended.


Contents

The aim of this course is to introduce Model Checking as an automatic approach to program verification. As a technique, it is especially suited for verifying properties of concurrent systems which often

comprise many nonterminating and communicating processes.

 


Given a mathematical model of the system under consideration and a property specification, Model Checking examines all possible system states and checks if the specification is satisfied.


The complexity of concurrent systems is due to the interleaving of the execution of the participating processes as well as to their interaction, for example by inter-process communication.


State-of-the-art model checking tools can handle state-spaces of about one billion distinguished states. Nevertheless, real-life systems may still exceed this limit by orders of magnitude. Therefore, techniques are needed which reduce this growth - known as the state-space explosion problem - without changing the (in-)validity of the specification's properties with respect to the original system-model.

 

 

 

In the first part of this course, we study transition systems as a means of modelling reactive systems and classify some of their important properties.


The second part introduces the automata theory and the temporal logics that Model Checking relies on.


In the third part, we address model checking timed systems.


The last part of the lecture is dedicated to other techniques for verification.


Dates

The module is offered in the winter 2006/07. Lectures are scheduled for Tue 14:00-16:00 and Thu 14:00-16:00.

 

We start on Oct, 17, and end on Feb 15 with a final exam. We have a midterm exam on Dec 21 and a practical exercise between 15.01.07 and 21.01.07 which takes about 20 hours. Excersises take place on Wed either 14:00-16:00 or 16:00-18:00. The lectures will be given in English; exercises are in English and German.

 

 

Further details are available at the CMS.


Grading

The grade will be based on the midterm exam (35%), the practical exercise (30%) and the final exam (35%).

 

There will be a minitest prior to the exercise in the individual groups. You need 30% of points of the overall minitest for the final exam. If you answer more questions correctly, you may earn a small bonus on the grade.


Venue

The lectures will be held in E 1 3 Hörsaal 001. The exercise classes will be in E 1 3 SR 013, SR 014 and SR 016 (please check the CMS for details).


The grade will be based on the accumulated raw points you earned in your successful examinations. High performance in the quizzes entitles you some bonus points.


Please login into the CMS to get more information!


Instructor

Prof. Dr.-Ing. Holger Hermanns

Assistants

Dipl.-Inf. Lijun Zhang
Dipl.-Inf. Sven Johr

Tutors

Wasilli Anastasatos
Christian Eisentraut
Patrick Wischnewski

Lecture Notes & Exercises

Lecture Notes and exercises are available in the CMS.


Literature

We will mostly follow the draft book 'Principles of Model Checking' by C. Baier and J.-P. Katoen. The latest versions of the book is not available electronically, but we have chapters (currently chapter 1-6) of the latest draft available for copying. Another version for copying will be available at the CIAM.

If you find some typos or errors, please enter it on this page.

 

Additional literature can be found in:

  • M. Huth and M.D. Ryan:

    Logic in Computer Science -- Modelling and Reasoning about Systems, Cambridge University Press, 2nd edition, 2004

  • K. Schneider:

    Verification of Reactive Systems, Springer-Verlag, Texts in Theoretical Computer Science. An EATCS Series, 2004

  • E.M. Clarke, O. Grumberg, D.A. Peled:

    Model Checking, MIT Press, 1999

  • K.L. McMillan:

    Symbolic Model Checking, Kluwer Academic, 1993

  • J.-P. Katoen:

    Concepts, Algorithms and Tools for Model Checking,

    Erlangen: Institut für Mathematische Maschinen und Datenverarbeitung, 1999

See also:

infobib.cs.uni-sb.de/frames/vorlesungen/verifikation.html