Summer School 2013: Verification Technology, Systems & Applications

VTSA08

The summer school on verification technology, systems & applications takes place at INRIA Center Nancy, France from September 02-06, 2013. 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 Swen Jacobs, Konstantin Korovin, Kim Larsen, Xavier Leroy, and Torsten Schaub 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 20th Juli 2013. Notifications on acceptance will be given by 27th Juli 2013.

Registration

The registration will be open to accepted applicants starting on 27th Juli 2013.

Program

All lectures will take place in room C005.

Schedule

September 02
Monday
September 03
Tuesday
September 04
Wednesday
September 05
Thursday
September 06
Friday
9.00-12.30 Xavier Leroy
Course Material | Slides
Torsten Schaub
Slides
Konstantin Korovin
Slides Part 2
Swen Jacobs
Slides Part 1
Kim Larsen
Slides Part 3 | Slides Part 4
12.30-14.00 Lunch break
14.00-17.20 Konstantin Korovin
Slides Part 1
Xavier Leroy
Course Material | Slides
Torsten Schaub
Slides
Kim Larsen
Slides Part 1 | Slides Part 2
Swen Jacobs
Slides Part 2
17.30-18.30 Presentations by participants Presentations by participants Presentations by participants
Evening School Dinner

Lecturer(s)

Swen Jacobs
Swen Jacobs

Reactive Synthesis
Reactive synthesis is the problem of turning a temporal logic specification into a reactive system. A major advantage of synthesis over verification is that manual programming is no longer required: synthesis automatically derives an implementation that is correct by construction. After synthesis was defined as an automated reasoning problem, it had long been considered infeasible for any interesting application. Recent years have brought advances both in reasoning methods that can be used as tools in the synthesis process, and in synthesis approaches themselves. As a result, case studies of substantial size can now be synthesized automatically.

In this lecture, we will formally define the synthesis problem and look at basic (game-based) approaches to solve it. As these approaches suffer from a state explosion problem that makes synthesis infeasible for all but very simple specifications, we will go on to review specialized techniques (GR(1)-synthesis, lazy synthesis, parameterized synthesis) that try to circumvent this problem in different ways.

Konstantin Korovin
Konstantin Korovin

Automated reasoning for first-order logic: theory, practice and challenges
Automated reasoning for first-order logic has a wide range of applications in verification, knowledge representation and proving mathematical theorems. First-order logic provides flexible expressive formalism for specifying problems in different domains. During the last 50 years there has been a large amount of research aimed at developing efficient reasoning methods for first-order logic. This lead to new logical calculi, frameworks for establishing completeness of such calculi, methods for redundancy elimination and advanced implementation techniques. In these lectures we take a journey from theoretical foundations of automated reasoning for first-order logic to practical implementation techniques, applications and discuss current challenges.

Kim Larsen
Kim Larsen

Model-Based Verification, Optimization, Synthesis and Performance Evaluation of Real-Time Systems
Model-driven development has been proposed as a way to deal with the increasing complexity of real-time and embedded systems, while reducing the time and cost to market. The use of models should permit early assessment of the functional correctness of a given design as well as requirements for resources (e.g. energy, memory, and bandwidth) and real-time and performance guarantees.

During these lectures we will offer a thorough account of the formalism of timed automata due Alur and Dill as well as several recent extensions. These extensions include priced timed automa- ta, (priced) timed games and most recently stochastic timed automata and we will introduce a number of associated decision problems related to model-checking, refinement checking and optimal scheduling and synthesis. The frontier of decidability will be drawn including pointing out a number of open problems.

The lectures will also emphasize the substantial research effort in the design of algorithms and datastructures for efficient analysis of timed automata and its extensions covering important datastructures such as DBMs (difference bounded matrices) and CDD (clock difference diagrams) as to be found in the verification tool UPPAAL and its various branches. Also, substantial focus will be on the application of statistical model checking where properties are settled up to user- specied level of confidence based on randomly generated simulation runs. A number of industrial applications will also be given.

Xavier Leroy
Xavier Leroy

Mechanized semantics with applications to program proof and compiler verification
The goal of this lecture is to show how modern theorem provers -- I use the Coq proof assistant -- can be used to mechanize the specification of programming languages and their semantics, and to reason over individual programs as well as over generic program transformations, as typically found in compilers.

The topics covered include:

  • Operational semantics: small-step, big-step, definitional interpreters.
  • Some forms of denotational semantics.
  • Axiomatic semantics and Hoare logic.
  • Generation of verification conditions; application to program proof.
  • Compilation to virtual machine code and its proof of correctness.
  • An example of an optimizing program transformation and its proof of correctness.
Torsten Schaub
Torsten Schaub

Answer Set Solving in Practice
Answer Set Programming (ASP) provides a declarative tool for modeling various problems typical to Knowledge Representation and Reasoning in particular and AI in general.
The unique pairing of declarativeness and performance allows for concentrating on an actual problem, rather than a smart way of implementing it. The ASP approach is not only highly suitable for the practitioner solving an AI problem at hand but also for disseminating many basic AI techniques through teaching their (executable) formalization in ASP.

The potential target audience for the tutorial is thus manifold, and comprises graduate students in AI, teachers of AI at universities, researchers addressing NP or NPNP hard problems, as well as Industrials addressing NP or NPNP hard problems.

What makes this tutorial different from others on ASP is its focus on putting ASP at work.
This comprises a good understanding of ASP solving technology and systems as well as basic skills in ASP's modeling capacities.

Contents:
The tutorial aims at acquainting the participant with ASP's modeling and solving methodology, enabling her/him to independent problem solving using ASP systems.
To this end, the tutorial starts with an introduction to the essential formal concepts of ASP, needed for understanding its semantics and solving technology. In fact, ASP solving rests on two major components: A grounder turning specifications in ASP's modeling language into propositional logic programs and a solver computing a requested number of answer sets of the given program.
Building on the aforementioned formal concepts, we provide a characterization of ASP's inference schemes that are in turn mapped into algorithms relying on advanced Boolean Constraint technology. We illustrate this technology through the ASP solver \texttt{clasp}, developed at the University of Potsdam, and winning first places at international ASP, CASC, MISC, PB, and SAT competitions. Similarly, ASP's grounding inferences are discussed in conjunction with (deductive) database techniques.
The remainder of the tutorial is dedicated to applying ASP, involving an introduction to ASP's modeling language, its solving methodology, and advanced techniques fostering scalability. The latter is illustrated via some real-world applications, taken from bio-informatics.
All involved ASP systems are freely available from http://potassco.sourceforge.net.

Accommodation

The participants are responsible for their room reservations.

We have negotiated special rates at Residhome Appart Hotel Nancy Lorraine: from 55€ per night and per room. Please specify "INRIA" when booking, before August 1st 2013.

Below is a selection of some hotels in Nancy, which are located close to the city center and the tram and bus lines to INRIA. For more information, see the Tourist Office of Nancy, or Booking.com.

There is a youth hostel located very close to INRIA (less than 10 minutes walking distance). Rooms have about 3 or 4 beds, and the rates are very cheap for members of a youth hostel association.

Château de Rémicourt
149 rue de Vandoeuvre
54600 Villers-lès-Nancy
Phone: +33 (0)3 83 27 73 67

Arrival / Directions

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

Nancy is reached in 1.5 hours by TGV from Paris (Gare de l'Est). There are also direct train connections to Strasbourg, Luxembourg, and Lyon.

Another option is the TGV Lorraine train station that is located close to the Metz-Nancy airport and is served by the same shuttle service to Nancy. It has direct TGV connections to Charles de Gaulle airport, Strasbourg, Lille, Rennes, and Bordeaux.

INRIA Nancy is located on the campus of the Faculty of Sciences of Nancy University (Université Henri Poincaré). Its physical address is

615 rue du Jardin Botanique
54602 Villers-lès-Nancy
tel. (+33) 383 59 30 00
Google Maps

The main entrance to INRIA Nancy is situated close to the southern tip of the building, from the parking located uphill. You will be asked to show an ID card at the front desk. INRIA provides wireless Internet access through eduroam or through a local visitor network.

From the train station and the city center, the INRIA research center is easily reached by public transportation.

From the train station:
Take the "tram" line 1 at the Nancy Gare stop in the direction of Vandoeuvre CHU and get off at the stop Callot. Then traverse the University campus: from the tram stop, turn right towards Lycée Jacques Callot, then follow the street uphill (turning left), finally enter the campus. INRIA is the white building on the top of the hill. The tram takes less than 15 minutes and runs every 5 minutes from 5:00am to 0:30am.

From the city center:
Take the line 8 for example at the Place Stanislas / Dom Calmet stop in the direction of Vandoeuvre CHU and get off at the stop Grande Corvée. INRIA is on your left, walk uphill about 30m. (The bus stop is in Rue du Jardin Botanique, facing the back side of INRIA, the main entrance to INRIA is on the other side.) The bus ride takes less than 15 minutes, buses run every 15-30 minutes from 5:00am to 10:00pm.

You can buy individual bus tickets from the driver. All tram stops have vending machines that accept coins and credit cards. Tickets for multiple trips can be bought at kiosks or at the vending machines.

Like many French cities, Nancy has a system of short-term bike rentals called Velostan. The bike ride from the city center to INRIA takes about 20 minutes.

Organization and Contact

General Organization

Local Organization

Website

For comments or questions send an email to Stephan Merz (stephan.merz (at) loria.fr).

The summer school is organized by the Montefiore Institute, University of Luxembourg, INRIA Nancy, and the Max Planck Insitute for Informatics Saarbrücken.

Important Dates

(Format is MM/DD/YYYY)

Sponsored by
INRIA MPII University of Lige Luxembourg
fnrs Moves SNT
Université de Lorraine Région Lorraine Communauté Urbaine du Grand Nancy