The summer school on verification technology, systems & applications takes place at Inria Center Nancy, France from August 27 - August 31, 2018. 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 verification can only be made if all three aspects are considered as a whole. Our five speakers David Basin, Jean-Christophe Filliâtre, Peter Lammich, Anca Muscholl and Carsten Sinz 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, accommodation and daily living costs on their own. Recommendations on hotels can be found below.
Please apply electronically by sending an email to stephan.merz@loria.fr including
by July 8, 2018. Notifications on acceptance/rejection will be given by July 11, 2018.
Registration will be open to accepted applicants starting on July 11, 2018.
All lectures take place in room A008, near the main entrance.
| August 27 Monday |
August 28 Tuesday |
August 29 Wednesday |
August 30 Thursday |
August 31 Friday |
|
|---|---|---|---|---|---|
| 8.00 | Registration | ||||
| 8.45 | Welcome | ||||
| 9.00-12.30 | David Basin | Anca Muscholl | Carsten Sinz | Peter Lammich | Jean-Christophe Filliâtre |
| 12.30-14.00 | Lunch break | ||||
| 14.00-17.30 | Anca Muscholl | David Basin | Jean-Christophe Filliâtre | Carsten Sinz | Peter Lammich |
| 17.30-18.30 | Student session | Student session | Student session | ||
| Evening | Get-Together (19:30) | School dinner (19:00) | |||
Note: The Student sessions give all participants the opportunity to discuss their PhD/Master topics with the speakers, the organizers and further senior researchers. The topic can be introduced by a short talk (10-15 minutes) and/or a poster. We encourage the participants to contribute to the student sessions. They are a great opportunity to discuss interesting topics with world leading experts in a relaxed atmosphere.
David Basin
|
Formal Methods for Security Protocols Security protocols are essential for securing distributed applications in today's Internet, e.g., by authenticating parties or setting up cryptographic keys. Although they are often small distributed algorithms, in practice they are exceedingly difficult to get right. Hence formal methods and associated tools play a crucial role in ensuring their correctness. We provide an overview to security protocol verification and focus, in particular, on the Tamarin Prover. Tamarin is a security protocol verification tool that supports both falsification and unbounded verification of security protocols specified as multiset rewriting systems with respect to (temporal) first-order properties and a message theory that models Diffie-Hellman exponentiation combined with a user-defined subterm-convergent rewriting theory. We will explain the ideas behind the tool and its application. |
Jean-Christophe Filliâtre
|
An Introduction to Deductive Program Verification This lecture introduces elementary concepts and techniques related to deductive program verification, such as loop invariants, function contracts, termination proofs, ghost code, modeling of data structures, weakest preconditions, etc. A particular focus is made on the use of automated theorem provers in the verification process and the tension that may exist between an elegant specification and a fully automated proof. The lecture includes many examples using the Why3 tool and participants are invited to verify small yet challenging programs using an on-line version of Why3. |
Peter Lammich
|
Algorithm Verification with the Isabelle Refinement Framework Isabelle/HOL is an interactive theorem prover for higher-order logic, that is, a tool that assists the user in conducting mathematically rigorous proofs that are verified by the computer. Isabelle/HOL comes with a large library of formalized mathematics and computer science, which can readily be used for new formalizations. One interesting application of theorem provers is to verify algorithms and their implementations. Stepwise refinement allows to structure such a proof along natural concepts known to most programmers: First, the mathematical idea of the algorithm is verified using adequate mathematical concepts like sets and functions. This results in a pseudo-code like algorithm as one may find in algorithm textbooks. Then, the mathematical concepts are implemented using appropriate data structures (e.g. Hash-table) and sub-algorithms (e.g. quicksort), which can be verified independently. Also, implementation specific optimizations can be added. The Isabelle Refinement Framework supports stepwise refinement in Isabelle/HOL. It comes with a large library of verified data structures and algorithms, and supports both functional and imperative features, as well as the generation of actual source code in various target languages (Haskell, Scala, OCaML, SML). In this lecture, we present stepwise refinement using network flow algorithms as running example. We will use the Isabelle Refinement Framework, but the presented formal tools and techniques are generally applicable, and prior knowledge of Isabelle is not required. |
Anca Muscholl
|
Distributed Synthesis Formal methods in computer science rely on a clear mathematical understanding of programs and their interactions. In synthesis, the goal is to construct a program that complies with some given logical specification. Synthesis of reactive programs addresses this question in the setting where programs interact with their environment. The problem was proposed in the sixties by A. Church as the solvability problem, and it can be stated in terms of a game between program and environment. An alternative formulation is the theory of supervisory control, that asks to build a controller guaranteeing that a given program satisfies some requirements. The course will start with an introduction to the areas of logic, automata and game theory that play a prominent role in synthesis. Then we will present different frameworks for distributed synthesis. The goal in distributed synthesis is to construct programs and controllers that consist of local entities that evolve by exchanging information. Distributed synthesis is a truly challenging area, where in some of the frameworks the decidability of the problem remains open. We will discuss the state-of-the-art and the challenges raised by the distributed setting. |
Carsten Sinz
|
Bounded Model Checking of Software for Real-World Applications Bounded model checking (BMC), a technique that originated form hardware verification, is increasingly used to check properties of software. It allows encoding program properties as SAT problems (or in certain SMT logics) by restricting programs to decidable fragments of first-order logic. BMC is especially suitable for low-level system software, where it has been applied to find bugs, e.g., in the Linux kernel or in embedded software. In the first part of this lecture, we will cover the basics of encoding programs and their properties as bounded model checking problems in SMT logic. We will also present some techniques, how program memory can efficiently be encoded in the logic of bit-vectors plus arrays, and which algorithms are used within SMT solvers to solve these problems. We will demonstrate this for the programming language C and run-time properties such as integer overflows, illegal memory accesses, etc., making use of the compiler framework LLVM’s intermediate representation. In the second part of the lecture, we will focus on techniques to increase scalability of BMC by adding light-weight program analysis methods, such as data-flow and control-flow analysis, slicing, or alias-analysis to the basic approach. |
Participants are responsible for their own accommodation arrangements.
Below is a selection of some hotels in Nancy, which are located close to the city center and the tram and bus lines to Iria. For more information, see the Tourist Office of Nancy, or Booking.com.
The Summer School 2018 will take place at Inria Nancy, France.
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 connected to Nancy by a shuttle service. 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. Take the tram line 1, for example at the Nancy Gare stop, in the direction of Vandoeuvre CHU and get off at the stop Callot. 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. 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.
For comments or questions send an email to stephan.merz@loria.fr
The summer school is organized by Inria Nancy - Grand Est, the University of Liège, the University of Luxembourg and the Max Planck Institute for Informatics, Saarbrücken.
| Application Deadline: | 2018/07/08 | |
|---|---|---|
| Notification until: | 2018/07/11 | |
| Summer School: | 2018/08/27 - 201/08/31 |
