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) mpi-inf.mpg.de) including
- a one page CV
- an application letter explaining your interest in the school and your experience in the area
- a copy of your bachelor certificate (or equivalent or a more significant certificate)
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.
SMT: Theory and Practice
SAT: Theory and Practice
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.
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.
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
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.
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".
- Hotel Continental
51 €, single room, breakfast included (reservation valid until the 1st of September 2008)
- Hotel Madeleine
65 €, single room, breakfast included, (reservation valid until the 1st of September 2008)
- Youth Hostel
33 €, single room, breakfast included, (reservation valid until the 1st of September 2008)
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:
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
- Application Deadline: 2008/07/20
- Notification until: 2008/07/31
- Summer School: 2008/09/15 - 2008/09/19
Photos of the event can be found here.