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.

Application

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.

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		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		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		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		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		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:

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:
- Map of Tram 1
- For more information on public transportation in Nancy, visit http://www.reseau-stan.com (in French only)

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.

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.

Important Dates

Application Deadline: 30th August 2009
Notification until: 11th September 2009
Summer School: 2009/10/12 - 2009/10/16

Photos

Photos of the event can be found here.