INRIA
max planck institut
informatik
mpii logo Minerva of the Max Planck Society

Summer School 2009: Verification Technology, Systems & Applications

VTSA08

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.

Application

Please apply electronically by sending an email to Manuel Lamotte-Schubert (lamotte (at) mpi-inf.mpg.de) including

until the 30th August 2009. Notifications on acceptance will be given by 11th September 2009.

Registration

The registration will be open to accepted applicants starting on 11th September 2009.

Program

All lectures will take place in room C005.

Schedule

October 12
Monday
October 13
Tuesday
October 14
Wednesday
October 15
Thursday
October 16
Friday
9.00-12.30 Daniel Le Berre
Slides Part 1
Leonardo de Moura
Slides Part 2
Extra Slides
Stephan Schulz
All Slides
Benjamin Werner Patricia Bouyer
Slides Part 1
12.30-14.00 Lunch break
14.00-17.20 Leonardo de Moura
Slides Part 1
Daniel Le Berre
Slides Part 2
Benjamin Werner Stephan Schulz
All Slides
Patricia Bouyer
Slides Part 2
17.30-18.30 Presentations by participants Presentations by participants Presentations by participants
Evening School Dinner

Lecturer(s)

Daniel Le Berre
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 and MAXSAT.
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 problems.
An analysis of recent SAT, MAXSAT and Pseudo Boolean competitive events will conclude the lecture.

Patricia Bouyer
Patricia Bouyer

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

Leonardo de Moura
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.

Stephan Schulz
Stephan Schulz

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.

Benjamin Werner
Benjamin Werner

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

Accommodation

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
54000 Nancy
(5 minutes by foot from the station)
Phone: +33 (0)3 83 40 31 24
Website: http://www.accorhotels.com/gb/hotel-6852-all-seasons-nancy-centre-gare/index.shtml

Hotel Akena Nancy

41 rue de Raymond Poincare
54000 Nancy
Phone: +33 (0)3 83 28 02 13
Website: http://www.hotel-akenanancy.com/

Hotel Le Guise

18 rue de Guise
54000 Nancy
Phone: +33 (0)3 83 32 24 68
Website: http://www.hoteldeguise.com

Hotel Ibis Nancy Centre Gare

3 rue Crampel
54000 Nancy
Phone: +33 (0)3 83 32 90 16
Website: http://www.ibishotel.com

Hotel Best Western

5, rue Chanzy
54 000 Nancy
Phone: +33 (0)3 83 17 54 00
Website: http://www.bestwestern.fr/hotelcrystal

Hotel des Prelats

56 place Mgr Ruch
54 000 Nancy
Phone: +33 (0)3 83 30 20 20
Website: http://www.hoteldesprelats.com

Youth Hostel

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
54600 Villers-lès-Nancy
Phone: +33 (0)3 83 27 73 67
Website: http://www.fuaj.org/

Arrival / Directions

The Summer School 2009 will take place at INRIA Center Nancy.

Travelling to Nancy

General instructions: 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 airports.

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

Nancy 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 by train.

There are two ways to reach the INRIA Center Nancy from the Train Station:

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 LORIA site.
[From the Callot Stop to the LORIA]

Here is a detailled plan of the location. Please note that the bus stops "UFR Staps" and "Grande Corvée" are identical.
In the LORIA building, you will be able to get an Internet connection, either in the room with machines, or using your own notebook with WiFi connection.

[Detailled map, click to enlarge]

Organization and Contact

General Organization

Local Organization

  • Anne-Lise Charbonnier
  • Nicolas Alcaraz

Website

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.

VTSA 09

Important Dates

Photos

Photos of the event can be found here.

Sponsored by
DFH INRIA MPII
Luxembourg SNT SNT SNT SNT SNT