Summer School 2009: Verification Technology, Systems & Applications
The second summer school on verification technology, systems & applications takes place at
the INRIA Center Nancy, France from
October, 12th-16th. 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 Daniel Le Berre, Patricia Bouyer,
Leonardo de Moura, Stephan Schulz, and Benjamin Werner 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-Schubert (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 30th August 2009. Notifications on acceptance will be given by 11th September 2009.
The registration will be open to accepted applicants starting on 11th September 2009.
All lectures will take place in room C005.
Daniel Le Berre
SAT and related technologies from a practitioner perspective
Within a decade, the use of SAT related technology moved from a
confidential interest among specialists to a popular tool for solving
some discrete combinatorial problems.
Improvements in the practical resolution of SAT is driven by
applications: Bounded Model Checking in Electronic Design Automation
has been a major component for the success of SAT engines for solving
"real" combinatorial problems at the end of the 90s, Bioinformatic and
Software engineering are currently two areas where SAT engines receive
a lot of interest.
In this lecture, we will focus on the theory behind modern SAT solvers
tailored to solve "real" combinatorial problems, and discuss their
extension to optimization problems such as pseudo boolean optimization
The lecture will introduce the generic SAT engine architecture used in
SAT4J (www.sat4j.org) inherited from
the original Minisat (www.minisat.se)
allowing to handle user defined constraints.
The specific case of pseudo boolean constraints will be detailed.
Then, we will see how to solve optimization problems with a SAT engine
able to handle pseudo boolean constraints.
The lecture will not be limited to the features found in SAT4J: it will
also include e.g. UNSAT core computation and their use to solve MAXSAT
problems since it is currently an efficient way to solve "real" MAXSAT
An analysis of recent SAT, MAXSAT and Pseudo Boolean competitive events
will conclude the lecture.
On the verification and control of timed systems
The modelling of complex systems like embedded systems or
communication protocols often requires being able to express
quantitative constraints on delays between events (such as "the
propagation delay is no more than 5 ms"), because the correctness of
these systems heavily depends on these quantitative aspects. Timed
automata have been proposed in the early nineties as a model for real-
time systems with rather good theoretical properties. Since then, they
have been much studied, and tools have been developed, which
automatically analyse this model.
In this tutorial, we will present the basics of the verification of
timed automata, from theoretical and decidability issues to algorithms
and tools. We will then discuss recent challenges that are being
investigated, like the modelling of resources (e.g. energy) in timed
Leonardo de Moura
On Designing and Implementing Satisfiability Modulo Theory Solvers
Satisfiability is one of the most fundamental problems in computer
science, namely the problem of determining whether a formula
expressing a constraint has a solution. The most well-known
constraint satisfaction problem is propositional satisfiability SAT,
where the goal is to decide whether a formula over Boolean variables,
formed using logical connectives, can be made true by choosing 0/1
values for its variables. Some problems require or are more naturally
described in more expressive logics such as first-order logic. Of
particular recent interest is satisfiability modulo theories (SMT),
where the interpretation of some symbols is constrained by a
background theory. For example, the theory of arithmetic constraints the
interpretation of symbols such as: +, < , 0, and 1.
In recent years, there has been an enormous progress in the scale of
problems that can be solved, thanks to innovations in core algorithms,
data structures, heuristics, and paying attention to implementation
details. In these lectures, we provide a brief overview of SMT, the
main technical ideas, and implementation techniques.
Implementation of First-Order Theorem Provers
First-order logic is in the Goldilocks Zone of deduction - expressive
enough to easily specify even complex properties, but simple enough to
support effective automatization. In this lecture, we will discuss the
implementation of efficient theorem proving systems for first-order
logic with equality.
After a short discussion of the logic and the calculus, the lecture
will cover the basic structure of a modern first-order theorem prover
based on clausification and saturation with redundancy elimination.
We will discuss the representation of the search state, the basic
saturation algorithm, search heuristics, and efficient algorithms and
data structures for implementing the most important operations. A
particular focus will be on proof search and on the implementation of
practically important simplification techniques.
Practical exercises for the "Implementation of First-Order Theorem Provers" will
require a laptop with a UNIX/Posix tool set, in particular "make", "gcc", and
basic UNIX utilities.
MacOS-X 10.4 and later will work. Linux, FreeBSD and Solaris will also work.
Cygwin with gcc installed will probably work.
It is no problem if you cannot bring a laptop, we have computers with Linux installed.
Coq proofs: the case of prime numbers
The fact that a number n is prime is an archetype of mathematical statements. However, the way
one proves this proposition will vary greatly with various factors: the size of n, the computing
power available, and the mathematical knowledge one can rely on.
Exactly the same situation can be observed when formalizing primality
proofs in a system like Coq. We will thus use this as a guideline for exploring
various proof-styles supported by Coq, and particularly proofs involving
The participants are responsible for their room reservations. Here is a list of recommended hotels. It is convenient to choose a hotel in the center, and to use the tram to reach the INRIA Center Nancy. You may also visit the Nancy Tourism Office website for other hotels (online booking is available).
Hotel All Seasons Nancy Centre Gare
3 rue de l'Armee Patton
(5 minutes by foot from the station)
Phone: +33 (0)3 83 40 31 24
Hotel Akena Nancy
41 rue de Raymond Poincare
Phone: +33 (0)3 83 28 02 13
Hotel Le Guise
18 rue de Guise
Phone: +33 (0)3 83 32 24 68
Hotel Ibis Nancy Centre Gare
3 rue Crampel
Phone: +33 (0)3 83 32 90 16
Hotel Best Western
5, rue Chanzy
54 000 Nancy
Phone: +33 (0)3 83 17 54 00
Hotel des Prelats
56 place Mgr Ruch
54 000 Nancy
Phone: +33 (0)3 83 30 20 20
There is a youth hostel located at a castle very close to the LORIA (5 minutes walk). Rooms have about 3 or 4 beds. The price per person per night is 13,90 Euros and includes sheets and breakfast.
Château de Rémicourt
149 rue de Vandoeuvre
Phone: +33 (0)3 83 27 73 67
Arrival / Directions
The Summer School 2009 will take place at INRIA Center Nancy.
Travelling to Nancy
Nancy is located roughly 300km east of Paris, 130km west of
Strasbourg, and 100km south of Luxembourg.
The Metz-Nancy Lorraine
regional airport is mainly served by domestic flights, but it may
be an option if your incoming flight goes to Lyon. There is a
regular shuttle service
to Nancy train station.
The closest international airports are Paris (Charles de Gaulle
and Orly), Luxembourg, and Frankfurt (Germany).
More adventurous spirits may try Frankfurt-Hahn or Bâle-Mulhouse
Nancy is reached in 1.5 hours by TGV from Paris, with some
direct trains from Charles de Gaulle airport. There are regular
train connections from Luxembourg and Germany (Frankfurt via Metz,
direct trains from Munich and Stuttgart).
TGV trains from Paris (Gare de l'Est) to Nancy arrive at Nancy
train station. TGV trains from other destinations (such as
Charles de Gaulle airport), or those that continue to Strasbourg
and Stuttgart stop at TGV Gare Lorraine, which is close to the
Metz-Nancy airport and served by the same
is well known for its 18th-century city center around
Place Stanislas, for its Art Nouveau buildings, and as a
center of research and higher education.
The Nancy Jazz Pulsations take place from 6th - 17th October. If you
are interested, please see the website of
Nancy Jazz Pulsations.
Travelling to INRIA Center Nancy
Most problably, people will be
arriving by train. Nancy only has a regional airport, so
also people arriving to the nearest international airports (Paris,
Luxemburg, Frankfurt, etc.) will probably complete their journey
There are two ways to reach the INRIA Center Nancy from the Train Station:
There is a new bus connection "Stan Campus"
from the train station (Nancy Gare) to the campus. The station for the INRIA Center
is "UFR STAPS".
Maps and timetable for this bus can be found here.
During the rush hour, the bus goes every 8 minutes, travel time is around 15 minutes.
The second way from the train station to the INRIA center is to take Tram 1
(this is the only tram line in Nancy).
In the map you can see the situation of the Train
Station and the nearest stop of Tram 1. Take the tram
towards Vandoeuvre, Chu Brabois until Callot stop (it is a 20 minutes ride).
There are ticket machines (you'll need
coins though, bills or cards are not accepted) at the stop of the
tram. Please note, that you cannot buy the ticket on the tram, so remember to buy
the ticket before boarding the tram.
The following pdf file might be useful:
The Summer School 2009 will take place at the building of
LORIA. The building is highlighted in the map below. We have also marked the path from the nearest tram station (stop Callot, of Tram
1). It takes about 5 minutes to walk from the tram station to the
Here is a detailled plan of the location. Please note that the bus stops "UFR Staps" and "Grande Corvée" are identical.
LORIA building, you will be able to get an Internet connection, either
in the room with machines, or using your own notebook with WiFi
Organization and Contact
- Anne-Lise Charbonnier
- Nicolas Alcaraz
For comments or questions send an email to Stephan Merz (stephan.merz (at) loria.fr).
The summer school is organized by INRIA Nancy and the Max Planck Insitute for Informatics Saarbrücken and also sponsored
by the University of Luxembourg, represented by Jun Pang. In 2010 the summer school on verification technology, systems & applications
will take place at the University of Luxembourg and will be organized by Jun Pang.
- Application Deadline: 30th August 2009
- Notification until: 11th September 2009
- Summer School: 2009/10/12 - 2009/10/16
Photos of the event can be found here.