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.
The aim of this course is to introduce Model Checking and related automatic approaches to program verification. The techniques covered are 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.
The module is offered in winter term 2014/15. Lectures are scheduled for Thu 8:30-10:00 and Fri 10:00-12:00 in building E1 3, lecture hall 001.
We start on Oct 23, and end on Feb 13. We will have three exams, tentatively scheduled for Nov 20, Jan 8, and Feb 12 or 13. The course will also include practical programming assignements. Tutorials are scheduled to take place on Tue 12:00-14:00 and Wed 10:00-12:00. The lectures and tutorials will be given in English.
Further details are available at the dCMS.
Lecture Notes & Exercises
Lecture Notes and exercises will be made available in the dCMS.
We will mostly follow the book '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
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
Symbolic Model Checking, Kluwer Academic, 1993
Concepts, Algorithms and Tools for Model Checking,
Erlangen: Institut für Mathematische Maschinen und Datenverarbeitung, 1999
|Dependable Systems & Software Group
|Department of Computer Science
|Universität des Saarlandes