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, systems which often comprise many nonterminating and communicating processes. We also review other verification techniques and domains.

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 winter 2008/09. Lectures are scheduled for Tue 14:15-15:55 and Thu 14:15-15:55 and are being held in HS 1 in E1 3.

We start on Thu, 23-10-2008 (not on Tue, 21-10-2008) and expect to finish on 12-02-2009

with a final exam. A midterm exam will be held on 18-12-008, and in the period 10-01-2009 to 19-01-2009 there will be a practical homework, that is expected to take about 15 hrs of time to get worked out.

Further details are available at the CMS.

Grading

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

Participating students have to hand in their solutions to the tutorial exercises prior to the individual exercise groups. They will be corrected. You need to secure 50% of the overall exercise points to qualify for the final exam. If you secure more than 80 %, you qualify for a bonus on the final grade.

Please login into the CMS to get more information!

Instructor

Prof. Dr.-Ing. Holger Hermanns

Assistant

Reza Pulungan, Msc

Lecture Notes & Exercises

Lecture Notes and exercises are available in the CMS.

Literature

We will mostly follow the great textbook 'Principles of Model Checking' by C. Baier and J.-P. Katoen.

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