Université du Luxembourg

Université du Luxembourg

Université de Liège

Université de Liège

Inria

Inria

Max-Planck-Institut für Informatik

Max-Planck-Institut für Informatik

UniGR Summer School on Verification Technology, Systems & Applications 2019

The summer school on verification technology, systems & applications takes place at the University of Luxembourg, Belval Campus, Maison du Savoir from July 1 - July 5, 2019. 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 Alexey Gotsman, Jochen Hoenicke, Catalin Hritcu, Marieke Huisman and Cezary Kaliszyk 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.

Application

Please apply electronically by sending an email to Soumya Paul including

by May 17, 2019. (Deadline extended) Notifications on acceptance/rejection will be given by May 20, 2019.

Registration

Registration will be open to accepted applicants starting on May 20, 2019.

Program

Schedule

All lectures take place in room MSA 4.520.

July 1
Monday
July 2
Tuesday
July 3
Wednesday
July 4
Thursday
July 5
Friday
8.00 Registration
8.45 Welcome
9.00-12.30 Catalin Hritcu Alexey Gotsman Marieke Huisman Cezary Kaliszyk Joechen Hoenicke
12.30-14.00 Lunch break
14.00-17.30 Alexey Gotsman Catalin Hritcu Jochen Hoenicke Marieke Huisman Cezary Kaliszyk
17.30-18.30 Reception 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.

Lecturer(s)

Alexey Gotsman
Alexey Gotsman

Reasoning About Data Consistency in Distributed Systems

Modern distributed systems often partition and replicate the data they manage across a large number of nodes and a wide geographical span. A key challenge that such systems have to address is maintaining data consistency in the presence of concurrent modifications at different nodes and despite inevitable failures. There is a spectrum of consistency models that a system can provide, and navigating it is far from trivial. Strong consistency models give the programmer the illusion that all nodes are always in sync, but hinder system scalability. In contrast, weak consistency models expose the programmer to the effects of replication in exchange for more scalable implementations. We will present modern methods for formally specifying consistency models of distributed systems and reasoning about how their choice affects system correctness. We will also present techniques for proving the correctness of consistency model implementations, including Paxos-based replication and replicated data types.

[Slides]

Jochen Hoenicke
Jochen Hoenicke

Software Model Checking with Ultimate

The Ultimate goal of software model checking is push button verification of existing code. In an ideal world one would use model checkers to find generic errors in code, e.g., undefined behaviour or crashes, similar to the way compilers today can be used to find syntactical errors. While this goal cannot be perfectly achieved the problem in general is undecidable the problem can be decided in common cases.

In this lecture we will take a closer look into a particular software model checker, Ultimate Automizer. This tool aims to be a sound verification tool that either finds a concrete error, proves the absence of errors, or runs out of resources. We will explain how the problem of finding generic errors on C programs can be reduced to a reachability problem in a simpler language. We will look under the hood and investigate techniques like trace abstraction and interpolation based model checking. This will be illustrated with examples where this method succeeds to prove the program correct and we show the limitations of this method.

[Slides]

Catalin Hritcu
Catalin Hritcu

Program Verification with F*

F* is a general-purpose functional programming language with effects aimed at program verification. It puts together the automation of an SMT-backed deductive verification tool with the expressive power of a proof assistant based on dependent types. After verification, F* programs can be extracted to efficient OCaml, F#, or C code. This enables verifying the functional correctness and security of realistic applications, such as a verified HTTPS stack.

This course will give an introduction to program verification in F* using simple examples and a few, even simpler exercises along the way. We will start with specifying and verifying purely-functional programs and then move to programs with side-effects such as divergence and mutable state. We will also cover F*’s support for reasoning about monotonically evolving state and for adding extra monadic side-effects, which is for instance used to implement F*’s tactic system in F* itself. Finally, we will look a bit under the hood at how F* encodes verification conditions to the SMT and how it computes them in the first place using monads indexed by predicate transformer monads, aka Dijkstra monads.

[Course Material]

Marieke Huisman
Marieke Huisman

Verification of Concurrent and Distributed Software

Concurrent and distributed software is inherently error-prone, due to the possible interactions and subtle interplays between the parallel computations. As a result, error prediction and tracing the sources of errors often is difficult. In particular, rerunning an execution with exactly the same input might not lead to the same error. To improve this situation, we need techniques that can provide static guarantees about the behaviour of a concurrent or distributed program.

In this lecture, I present an approach based on program annotations. I will first describe the fundamental of annotation-based verification, and then I discuss what is needed to use this approach for concurrent and distributed software. In particular, for concurrent and distributed software the program annotations have to take care of what part of the memory is affected by a thread or process. To take care of this, the program annotations will be based on concurrent separation logic. I will describe how this is done, and how we support reasoning about concurrent and distributed programs using the VerCors tool set.

In the second part of the lecture, I will describe a further extension, which allows one to reason about behavioural properties of a concurrent or distributed program. We will show how we can define an abstract model that captures the behaviour of the program. We use program logic to show that the program behaves as described by the abstract model, while we use model checking to reason about properties of the abstract model.

Throughout the lecture, various exercises will be given, so that the audience gets hand-on experience with verification of concurrent and distributed software.

[Course Material]

Cezary Kaliszyk
Cezary Kaliszyk

Artificial Intelligence in Theorem Proving

The course will discuss the learning problems in theorem proving. We will start with the design of automated and interactive theorem proving systems as well as proof certifiers and discus the various machine learning problems that correspond to the built in heuristics. First, the course will focus on the high-level learning problems in proof assistants and techniques for the selection of relevant lemmas in large libraries. Next the focus of the course will be on strategy selection and strategy tuning using learning. Finally internal guidance of automated reasoning systems, including prediction of useful inference steps and tactics, as well as the evaluation of intermediate proof states will be discussed.

[Part1], [Part2]

Accommodation

Participants are responsible for their own accommodation arrangements.

We have negotiated special rates at:

Ibis Esch Belval
12 Avenue du Rock’n Roll
L-4361 Esch/Alzette

Please fill in this form in capital letters and fax or email it back to the hotel no later than 30/05/2019.

Arrival / Directions

The Summer School 2019 will take place at University of Luxembourg, Campus Belval, Esch-sur-Alzette.

The summer school will take place in the lecture room MSA 4.520 (building Maison du Savoir) at the Belval Campus of University of Luxembourg. Please check this link for information on how to access the summer school.

Organization and Contact

General Organization

Local Organization

Website

For comments or questions send an email to Jun Pang

The summer school is organized by the University of Luxembourg, Inria Nancy - Grand Est, the University of Liège, and the Max Planck Institute for Informatics, Saarbrücken.

Important Dates

Application Deadline: 2019/05/17
Notification until: 2019/05/20
Summer School: 2019/07/01 - 2019/07/05
(Format is YYYY/MM/DD)

Sponsored by
UniGR

UniGR

Université du Luxembourg

Université du Luxembourg

Computer Science and Communications Research Unit

Computer Science and Communications Research Unit

CSCE

Doctoral Programme in Computer Science and Computer Engineering

Interdisciplinary Centre for Security, Reliability and Trust

Interdisciplinary Centre for Security, Reliability and Trust

Inria

Inria

Université de Liège

Université de Liège

Max-Planck-Institut für Informatik

Max-Planck-Institut für Informatik

Supported by CPEC TRR 248 (see perspicuous-computing.science)