Verification

Verification

Audience

This core lecture (Stammvorlesung) addresses Bachelor and Master students in Computer Science, Bioinformatics, Embedded Systems, CuK or Computerlinguistics. Bachelor students must have passed the base lecture Programmmierung 1. Decent knowledge in Concurrent Programming and Theoretical Computer Science is recommended.

 

Contents

The aim of this course is to introduce Model Checking and related automatic approaches to program verification. These techniques are 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.

The course is tentatively structured as follows:

• In the first part of this course, we study transition systems as a means of modelling reactive systems, discuss temporal logics, and look into computation tree logic (CTL) model checking.
• The second part introduces automata theory on infinite words, linear time temporal logic (LTL), and LTL model checking.
• In the third part, we address abstraction techniques and discuss model checking for timed systems, as well as other techniques for verification.