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

Summer School on Verification Technology, Systems & Applications 2021

The summer school on verification technology, systems & applications takes place at the University of Liège, Sart-Tilman Campus from October 11 - October 15, 2021. 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 Gilles Audemard, Cezara Drăgoi, Christoph Haase, Leslie Lamport, and Josef Widder 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 a school dinner. Participants take travel, accommodation and daily living costs on their own. Recommendations on hotels can be found below.

More photos can be found here

Application

Please apply electronically by sending an email to vtsa2021@montefiore.ulg.ac.be including

by September 15, 2021. Notifications on acceptance/rejection will be given by September 20, 2021.

We are very happy that Leslie Lamport, Turing Award 2013, will be present for a discussion at VTSA 2021. We ask every applicant to watch his talk "If you're Not Writing a Program Don't Use a Programming Language" and think about one question that he/she would like to ask during this discussion with Leslie Lamport. Please provide this question in your application letter.

Registration

Registration will be open to accepted applicants starting on September 20, 2021.

Program

Schedule

All lectures take place in room R7 at the Montefiore Institute (B28), Sart-Tilman, University of Liège, except on Monday afternoon (I.21, same building).

11/10
Monday
12/10
Tuesday
13/10
Wednesday
14/10
Thursday
15/10
Friday
8.00 Registration
8.45 Welcome
9.00-12.30 Josef Widder
Cezara Drăgoi
Cezara Drăgoi
Christoph Haase
Christoph Haase
12.30-14.00 Lunch break
14.00-17.30 Gilles Audemard
Josef Widder
Discussion with
Leslie Lamport (16:30 - 18:00)
Gilles Audemard
17:30-18:30 Student Sessions Student Sessions
Evening Get-Together (19:30) School Dinner (19:00) Student Session (17:30)

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)

Gilles Audemard
Gilles Audemard

SAT solver essentials, SAT modeling and algorithms

In this course, we will focus on sequential and parallel SAT solving techniques. We will first describe the main components of Conflict Driven Clause Learning (CDCL) architecture used in most SAT solvers (conflict analysis, restarts, heuristics...). After that, we will present different approaches used to solve SAT in a parallel environment with a special attention to shared clauses. Finally, we will focus on SAT encoding and on incremental SAT solving where the SAT solver is used as an oracle to solve computationally more challenging problems. This course will also contain practical sessions.

Slides: [Part 1] [Part 2] [Part 3] [Part 4] [Part 5]

Cezara Drăgoi
Cezara Dragoi

Towards automated verification of fault-tolerantdistributed systems

Fault-tolerant distributed systems have been widely used and studied for the past 25 years. Solutions for agreement like problems, e.g., consensus, state machine replication, are developed and deployed over large networks by commercial products, e.g., Apache Zookeeper, Cassandra. However, the automated verification techniques have received much less attention in the academic or industrial community.

In this lecture we will identify the new challenges posed by fault-tolerance to automated techniques and we will discuss some of the existing solutions. The lecture will mainly focus on verification techniques designed for distributed protocols, with few pointers to extensions of these techniques to large scale implementations of these protocols.

The lecture focuses of verification techniques for consensus and replicated state machine. The lecture presents a formalization of communication-closure, a property of distributed systems that facilitates formal reasoning. We define a semantic reduction of the execution space, based on communication-closure, that preserves an important class of properties, including consensus. Concretely, the reduction shows that an asynchronous set of executions is equivalent to a synchronous set of executions. Verification techniques based on SMT-solvers are applied only to synchronous executions, which have much simple proof arguments.

Christoph Haase
Christoph Haase

Linear arithmetic theories: theory andapplications

Theories of linear arithmetic over R, Q, Z, and N are at the core of computational logic. Arising as generalizations of their existential conjunctive fragments, linear programming and integer programming, they occur in many contexts in computer science both in theory and practice. Reducing domain-specific constraints to a linear arithmetic theory is a standard and powerful problem-solving technique. Arithmetic theories are a fascinating object to study, as they lie at the interface of geometry, algorithmics, and logic.

This course gives an introduction to logical theories of linear arithmetic and their applications, such as the first-order linear theory of the reals and Presburger arithmetic, its analogue over the natural numbers. In the first part of the course, we will explore the theory behind linear arithmetic theories and mainly focus on paradigms for deciding such theories based on quantifier elimination, finite-state automata, generating sets and generating functions. In the second part of the course we will look at concrete applications of linear arithmetic theories in software verification, e.g., for finding bugs in concurrent programs and other infinite-state systems.

Slides: [PDF]

Leslie Lamport
Leslie Lamport

Discussion

We are very happy that Leslie Lamport, Turing Award 2013, will be present for a discussion at VTSA 2021. We ask every applicant to watch his talk "If you're Not Writing a Program Don't Use a Programming Language" and think about one question that he/she would like to ask during this discussion with Leslie Lamport. Please provide this question in your application letter.

Josef Widder
Josef Widder

Consensus in distributed systems

Fault-tolerant distributed consensus has been a central problem in the study of the principles of distributed computing for over forty years: each component in an unreliable distributed system has an input value and the component should eventually agree to output the same value, selected from the inputs. As individual components may fail, devising correct solutions is hard, error-prone, and for many systems impossible.

Due to the considerable cost of consensus solutions, the classic application domains were typically limited to safety critical systems, where for instance, out of four components at most one is assumed to fail and the others should maintain operational and in agreement. Recently we observed a renaissance of consensus in the scope of blockchains: For instance, Tendermint/Cosmos is a modern implementation that uses consensus for state machine replication, and scales to hundreds of components in adversarial environments.

I will discuss how distributed systems are modeled, I will show classical definitions of consensus and related problems, and describe solutions to the problems, and how one proves them correct by hand.

Understanding the intricacies of these issues is crucial for computer-aided verification of consensus algorithms and implementations, which is a flourishing research line these days. I will present some methods for the verification of abstract algorithms based on the threshold automata framework.

Slides: [PDF]

Accommodation

Participants are responsible for their own accommodation arrangements.

Arrival / Directions

The Summer School 2021 will take place at University of Liège, Sart-Tilman Campus.

There is still some uncertainty with the current sanitary crisis. Please check the traveling rules for Belgium that apply to you here: https://www.info-coronavirus.be/en/travels/
As for now, fully vaccinated people from EU are allowed to travel to Belgium without quarantine, but filling a Passenger Locator Form (PLF) is required.

If the school cannot happen in person, it will be canceled (and rescheduled when the situation gets clear).

Organization and Contact

General Organization

Local Organization

Special thanks to Prof. Pascal Gribomont for his generous support

Website

For comments or questions send an email to vtsa2021@montefiore.ulg.ac.be.

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.

Important Dates

Application Deadline: 2021/09/15
Notification until: 2021/09/20
Summer School: 2021/10/11 - 2021/10/15
(Format is YYYY/MM/DD)

Photos

click to enlarge

Sponsored by

UniGR

Université du Luxembourg

Computer Science and Communications Research Unit

Doctoral Programme in Computer Science and Computer Engineering

Interdisciplinary Centre for Security, Reliability and Trust

Inria

Université de Liège

Max-Planck-Institut für Informatik

Supported by the Faculty of Applied Sciences

Supported by the Montefiore Institute