max planck institut
mpii logo Minerva of the Max Planck Society

Summer School 2008: Verification Technology, Systems & Applications


The summer school on verification technology, systems & applications takes place at the Max Planck Institute for Informatics at Saarbrücken, Germany from September 15th-19th. We believe that all three aspects verification technology, systems & applications strongly depend on each other and that progress in the area of formal analysis and verifiation can only be made if all three aspects are considered as a whole. Our five speakers Gilles Barthe, Clark Barrett, Martin Fraenzle, Radu Mateescu, and Grégoire Sutre stand for this view in that they represent and will present a particular verification technology and its implementation in a system in order to successfully apply the approach to real world verification problems.

The number of participants in the school is limited to 40. We expect participants to hold a bachelor (or higher) degree in computer science (or equivalent) and to have basic knowledge in propositional and first-order logic.

The summer school is free of charge. It includes the lectures, daily coffee breaks and lunches and the special summer school dinner on Wednesday. Participants take travel, accomodation and daily living costs on their own. Recommendations on hotels can be found below.


Please apply electronically by sending an email to Manuel Lamotte (lamotte (at) including

until the 20th of July, 2008. Notifications on acceptance will be given by July, 31st.


The registration will be open to accepted applicants starting on August, 1st, 2008.


All lectures will take place in room 024 at the ground floor of the Max Planck Institute for Informatics (MPII, building E1 4) located on the university campus of Saarbrücken.


September 15
September 16
September 17
September 18
September 19
9.00-12.30 Radu Mateescu
Gilles Barthe
Martin Fränzle
Grégoire Sutre
Static Analysis
Clark Barrett
SMT: Theory and Practice
12.30-14.30 Lunch break
14.30-18.30 Gilles Barthe
Radu Mateescu
Clark Barrett
SAT: Theory and Practice
Martin Fränzle
Grégoire Sutre
Abstraction Refinement
Evening School Dinner


Clark Barrett
Clark Barrett

SAT and SMT: Theory and Practice
In the past decade, there has been a steady increase in the use of formal methods to verify systems. This success is largely due to advances in algorithms for Boolean logic. In particular, fast algorithms for Boolean satisfiability (SAT) have increased the capability of core Boolean verification engines by several orders of magnitude.

While Boolean methods are capable of modeling most verification tasks, systems are usually designed and modeled at a higher level, and the translation to Boolean logic can be both expensive and obfuscating. Satisfiability Modulo Theories (SMT) is the natural next step in the evolution of fast and automatic verification engines. Built on top of fast SAT solvers, SMT solvers can match the speed and automation of today's Boolean engines while at the same time providing high-level reasoning capabilities that give them a significant advantage in both ease of use and performance.

In these lectures, I will present a theoretical framework for SAT and SMT, discuss the history and content of the main innovations that have led to important performance improvements, and give some perspective on how to build and use SAT and SMT solvers.

Gilles Barthe
Gilles Barthe

Formal Methods for Software Correctness and Security
Reliability and security of executable code is an important concern in many application domains, and in particular mobile code where code consumers run code that originate from untrusted and potentially malicious producers. The purpose of this course is to introduce some static mechanisms to ensure properties of source programs, and to demonstrate how the evidence they provide may be transferred to their executable counterparts, in the form of a certificate that can be used in the context of Proof Carrying Code. The primary focus shall be on type-based mechanisms for enforcing type safety and information flow policies, but I shall also discuss using logical methods to verify program correctness, and describe algorithms that transform proofs of source prgorams into proofs of executable code.

Martin Fränzle
Martin Fränzle

Automatic Analysis of Hybrid Systems
Embedded digital systems have become ubiquitous in everyday life. Many such systems, including many of the safety-critical ones, operate within or comprise tightly coupled networks of both discrete-state and continuous-state components. The behavior of such hybrid discrete-continuous systems cannot be fully understood without explicitly modeling and analyzing the tight interaction of their discrete switching behavior and their continuous dynamics, as mutual feedback confines fully separate analysis to limited cases. Tools for building such integrated models and for simulating their approximate dynamics are commercially available, e.g. Simulink with the Stateflow extension. Simulation is, however, inherently incomplete and has to be complemented by verification, which amounts to showing that the coupled dynamics of the embedded system and its environment is well-behaved, regardless of the actual disturbance and the influences of the application context, as entering through the open inputs of the system under investigation. Basic notions of being well-behaved demand that the system under investigation may never reach an undesirable state (safety), that it will converge to a certain set of states (stabilization), or that it can be guaranteed to eventually reach a desirable state (progress).

Within this school, we concentrate on automatic verification and analysis of hybrid systems, with a focus on fully symbolic methods manipulating both the discrete and the continuous state components symbolically by means of predicates. We provide an introduction to hybrid discrete-continuous systems, demonstrate the use of predicative encodings for compactly encoding operational high-level models, and continue to a number of methods for automatically analyzing safety, stability, and progress.

Radu Mateescu
Radu Mateescu

Model Checking of Action-Based Concurrent Systems
Asynchronous systems are present in a variety of domains, such as telecommunication protocols, embedded software, or multiprocessor architectures. These systems typically consist of a set of computing entities (processes or agents) executing in parallel and communicating by message-passing. Their behaviour is therefore complex and must be analyzed formally in order to detect and correct design errors as early as possible. Several formalisms have been defined for specifying the behaviour of asynchronous systems, among which networks of communicating automata, process algebras, and mu-calculi. The semantic models underlying these formalisms are the so-called labeled transition systems (LTSs), which are state/transition graphs describing the behaviour of asynchronous systems in terms of the actions.

We give an overview of these formalisms and show how they can be used to specify the behaviour of various asynchronous systems. We also present the main verification methods operating on LTSs, namely equivalence checking and model checking, and we illustrate their practical implementation and usage by means of CADP, a state-of-the-art verification toolbox for asynchronous systems.

Grégoire Sutre
Gregoire Sutre

Software Model Checking
Ensuring correctness of software systems is an increasingly challenging task due to the rapidly growing size and complexity of software. Moreover, software systems play an increasing role in safety-critical embedded systems, where dedicated hardware parts are gradually being replaced with generic architectures with dedicated software running on top of them. There is therefore an increasing need for automatic tools to formally verify software systems. However, such systems have in general very large or even infinite state spaces, and hence they are not directly amenable to classical finite-state verification methods.

Approximate verification techniques can be used to verify large systems that are beyond the reach of classical model checking. These techniques are based on property-preserving abstractions of the semantics of the system. Abstractions were first designed manually, but automatic techniques such as predicate abstraction and CEGAR (counter-example guided abstraction refinement) have recently led to fully automatic and successful tools for the verification of large software systems.

In these lectures, I will present the two main theoretical frameworks for software verification by abstraction: abstract interpretation and abstract model refinement. Algorithms to automatically construct abstract models from program sources will be presented, as well as an overview of several refinement methods. Several variants of the CEGAR approach will be compared. I will also discuss symbolic verification of some classes of infinite-state abstract models that arise from software constructs such as recursion or thread creation.


The participants are responsible for their room reservations. In Saarbrücken per-night prices including taxes and breakfast typically range from EURO 20 (youth hostel, double room) to about EUR 70 (hotel, single room).

Here is a list of hotels as provided by the Kongress and Touristik GmbH, Saarbrücken.

We have also reserved rooms at a special rate in the following hotels. Please book the rooms yourself using the keyword "Summer School".

Arrival / Directions

The Summer School 2008 will take place at the campus of Saarland University, in the building of the Max Planck Institute for Informatics (MPII, building E1 4) located on the university campus. For more information on Saarbrücken, you can also check here.

Travelling to Saarbrücken

General instructions: Directions

With Public Transportation from the City to the MPII

Please use the connection planning tool offered by the public transportation in Saarland:

By Car

Please use the multi-storey car park "Uni-Ost". Pull a parking ticket. On departure you will get a free ticket for leaving the car park.

Organization and Contact

General Organization

Local Organization

For comments or questions send an email to Roxane Wetzel (wetzel (at)


Important Dates


Photos of the event can be found here.

Useful Links

Sponsored by DFH INRIA MPII Trustworthy Software Systems