The summer school on verification technology, systems & applications takes place at INRIA Nancy, France from August 28 - September 1, 2023. 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 Sandrine Blazy, Simon Bliudze, Igor Konnov, Martin Leucker, and Peter Müller 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 as well as a school dinner. Participants take travel, accommodation and daily living costs on their own. EuroProofNet can refund the travel and accommodation of a number of participants (the daily allowance for accommodation and meals is 120 euros). The criteria according to which EuroProofNet will decide to reimburse travel costs are in order: inclusiveness target countries, age, gender, and team with low resources. Useful information concerning eligibility and reimbursement rules can be found under the following links: Eligibility Reimbursement Rules
Please apply electronically by sending an email to Jennifer Müller including
by July 9, 2023. Notifications on acceptance/rejection will be given by July 12, 2023.
Accepted participants are automatically registered for the summer school. If you are not able to attend the summer school, please follow the instructions in your acceptance notification email.
All lectures take place in room A008, LORIA building.
| August 28 Monday |
August 29 Tuesday |
August 30 Wednesday |
August 31 Thursday |
September 1 Friday |
|
|---|---|---|---|---|---|
| 08.00 - 08.45 | Registration | ||||
| 08.45 - 09.00 | Welcome | ||||
| 09.00 - 12.30 | Sandrine Blazy | Igor Konnov | Martin Leucker | Peter Müller | Peter Müller |
| 12.30 - 14.00 | Lunch break | ||||
| 14.00 - 17.30 | Martin Leucker | Sandrine Blazy | Igor Konnov | Simon Bliudze | Simon Bliudze |
| 17:30 - 18:30 | Student Sessions | Student Sessions | Student Sessions | ||
| Evening | Get-Together (19:30) | School Dinner (20: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.
Sandrine Blazy
|
Verified Compilation Deductive verification provides very strong guarantees that software is bug-free. Since the verification is usually done at the source level, the compiler becomes a weak link in the production of software. Verifying the compiler itself provides guarantees that no errors are introduced during compilation. This course will first introduce the basics of verified compilation, using the Coq theorem prover. Then, it will present CompCert, a fully verified compiler for C that is actually usable on real source code and that produces decent target code on real-world architectures. More generally, this approach opens the way to the verification of software tools involved in the production and verification of software. |
Simon Bliudze
|
Rigorous System Design using BIP: Correctness by All Means This course is about the Rigorous System Design (RSD) approach for concurrent component-based systems. The aim of the approach is to manage the complexity of showing the system correctness by decomposing it into small, focused tasks, such as verification of individual components and of concurrent design patterns, on one hand, and proof of model transformation techniques, on the other hand. We will focus on the BIP framework supporting such an RSD approach. In the first part, we overview the RSD approach and the BIP language. In the second part, we discuss some theoretical results supporting the various components of the correctness argument. |
Igor Konnov
|
Specifying blockchain protocols with TLA+ and Quint and checking them with Apalache TLA+ is a language and logic for formal specification of all kinds of computer systems. System designers use this language to specify concurrent, distributed, and fault-tolerant protocols, which are traditionally presented in pseudo-code. At Informal Systems, we have been using TLA+ to specify and reason about the protocols and distributed applications that are running in Cosmos blockchains. Our main tool of choice for TLA+ is the symbolic model checker called Apalache. In 2023, we introduced a new specification language called Quint. This language is an alternative syntax for TLA+ that should look more familiar to engineers. In this lecture, we demonstrate the main principles of writing specifications and checking them with Apalache. We are using examples from the blockchain industry. We also show the practical applications of the tooling provided by Apalache and Quint. |
Martin Leucker
|
Theory and Practice of Runtime Verification In this course we give an introduction to the field of Runtime Verification. More specifically, we give a comprehensive and coherent assessment to Linear Temporal Logic-based monitor synthesis approaches. We cover both rewriting and automata-based techniques based on both finite and infinite trace semantics. Moreover, we give an introduction to stream-runtime verification and discuss the commonalities as well as differences. Beyond a formal account we present applications in different settings. |
Peter Müller
|
Building Deductive Program Verifiers Deductive program verifiers attempt to construct a proof that a given program satisfies a given specification. Their implementations reflect the semantics of the programming language and the specification language, and often include elaborate proof search strategies to automate verification. Each of these components is intricate, which makes building a verifier from scratch complex and costly. In this lecture series, we will present an approach to build program verifiers as a sequence of translations from the source language and specification via intermediate languages down to a logic for which automatic solvers exist. This architecture reduces the overall complexity by dividing the verification process into simpler, well-defined tasks, and enables the reuse of essential elements of a program verifier such as parts of the proof search, specification inference, and counterexample generation. We will introduce intermediate verification languages and demonstrate how they can encode interesting verification problems. |
Participants are responsible for their own accommodation arrangements.
The Summer School 2023 will take place at INRIA Nancy, France. You will be asked to show an ID card at the front desk and you may be subject to a bag search.
Nancy is located roughly 300km east of Paris, 130km west of Strasbourg, and 100km south of Luxembourg. 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. From the train station, take the bus line A in the direction of Vandœuvre CHU and get off at the Vélodrome stop. Continue on foot across the Vélodrome intersection and traverse the university campus, following the street uphill. Inria is the white building on the top of the hill. The trip takes about 20 minutes. Alternatively, take the bus line 3 and get off at the stop Grande Corvée at the back side of the Inria building, then continue uphill and around the building to reach the front entrance. The Web site https://www.reseau-stan.com has more information on public transportation in Nancy. Tickets are available at vending machines, kiosks or from the bus driver (single tickets only).
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.
The summer school will take place in the lecture room A008.
For comments or questions, please send an email to Stephan Merz.
The summer school is organized by the University of Liège, the University of Luxembourg, Inria Nancy - Grand Est, and the Max Planck Institute for Informatics, Saarbrücken.
| Application Deadline: | 2023/07/09 | |
|---|---|---|
| Notification until: | 2023/07/12 | |
| Summer School: | 2023/08/28 - 2023/09/01 |
click to enlarge
