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 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.

 


Dates

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.


Instructor

Prof. Dr.-Ing. Holger Hermanns

Assistants

Yulyia Butkova, BSc
Alexander Graf-Brill, MSc
Arnd Hartmanns, MSc

Tutors

Felix Freiberger

Lecture Notes & Exercises

Lecture Notes and exercises will be made available in the dCMS.


Literature

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

  • 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:

www.infomath-bib.de/tmp/vorlesungen/info-core_verification.html