Université du Luxembourg

Université du Luxembourg

Université de Liège

Université de Liège

Inria

Inria

Max Planck Institute for Informatic

Max Planck Institute for Informatics

Summer School on Verification Technology, Systems & Applications 2024

The summer school on verification technology, systems & applications takes place at the University of Luxembourg, Belval Campus, Maison du Savoir from July 8 - July 12, 2024. 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 Wolfgang Ahrendt, Étienne André, Joao Marques-Silva, Caterina Urban and Anton Wijs 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 Jennifer Müller including

by May 24, 2024. Notifications on acceptance/rejection will be given by May 30, 2024.

Registration

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.

Program

Schedule

All lectures take place in room MSA 4.530.

July 8
Monday
July 9
Tuesday
July 10
Wednesday
July 11
Thursday
July 12
Friday
8.00 Registration
8.45 Welcome
9.00-12.30 Wolfgang Ahrendt
Anton Wijs
Joao Marques-Silva
Caterina Urban
Étienne André
12.30-14.00 Lunch break
14.00-17.30 Anton Wijs
Wolfgang Ahrendt
Étienne André
Joao Marques-Silva
Caterina Urban
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)

Wolfgang Ahrendt
Wolfgang Ahrendt

Dynamic Logic for Practical Program Verification

Dynamic logics (DL) are mutli-modal logics, where modalities are parameterised over actions from some action language. The action language may be a programming language, or consist of system (or component) level steps, or of environment moves. In this talk, I introduce principles of DL, and show how DL based verification can be practically used to verify programs. In particular, I will show how the KeY system supports dynamic logic based verification of some mainstream programming languages.

[Part 1], [Part 2], [Part 3], [Part 4], [Part 5]

Étienne André
Etienne Andre

(Parametric) Timed Verification

The correctness of real-time systems, that mix concurrency with hard timing constraints, is important, yet challenging to achieve. Formal verification techniques such as model checking provide guarantees of correctness. This course will focus on timed automata, an extension of finite-state automata with clocks measuring the elapsing of time, and on (timed) temporal logics; it will provide an overview of the concepts in this area. The course will also mention parametric timed formalisms, turning very useful when the system is not known with full precision, or at early design stages. Depending on the time, practical sessions may be organized.

Joao Marques-Silva
Joao Marques-Silva

An Overview of Symbolic Explainability

Motivated by the remarkable advances in machine learning (ML), there exists a pressing need to build trust in the operation of ML models, especially for those that target high-risk uses. One main goal of explainable artificial intelligence (XAI) is to deliver trustworthy AI, by enabling human decision makers to fathom the operation of ML models. Unfortunately, the most visible XAI solutions are riddled with misconceptions, and so computed explanations offer no guarantees of rigor. Formal (or symbolic) XAI represents a solution to the pitfalls of informal XAI that has been under active development in recent years. This lecture offers an overview of the emerging field of symbolic XAI, covering its main achievements, but also the challenges that it still faces.

Caterina Urban
Caterina Urban

Formal Methods for Machine Learning Pipelines

Formal methods offer rigorous assurances of correctness for both hardware and software systems. Their use is well established in industry, notably to certify safety of critical applications subjected to stringent certification processes. With the rising prominence of machine learning, the integration of machine-learned components into critical systems presents novel challenges for the soundness, precision, and scalability of formal methods.

This lecture serves as an introduction to formal methods tailored for machine learning pipelines, highlighting their strengths and limitations. We will present several approaches through the lens of different software properties and targeting software across all phases of a machine learning pipeline, with a focus on abstract interpretation-based techniques. We will then conclude by offering perspectives for future research directions in this evolving context.

[Slides]

Anton Wijs
Anton Wijs

Accelerated Verification

The formal verification of hard- and software, with techniques such as model checking and deductive verification, is computationally very demanding. Graphics Processing Units (GPUs) have been increasingly successful in pushing the boundaries of the state-of-the-art in many research fields, with their application to AI being the latest prominent success. This course will address how GPUs can be used to accelerate formal verification.

The focus will first be on the basics of GPU programming. You will get hands-on experience with the Single Instruction Multiple Threads execution model, and iteratively optimise an initial CUDA program to use the various features of NVIDIA’s GPUs. Next, you will apply this knowledge to accelerate computations relevant for formal verification, including graph analysis and SAT solving. How these computations fit in the bigger picture of formal verification tools will be discussed, including a comparison of relevant algorithms.

[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 June 8th, 2024.

Arrival / Directions

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

The summer school will take place in the lecture room MSA 4.530 (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: 2024/05/24
Notification until: 2024/05/30
Summer School: 2024/07/08 - 2024/07/12
(Format is YYYY/MM/DD)

Photos

click to enlarge

Université de Liège

Université du Luxembourg

University of Luxembourg - Department of Computer Science

Interdisciplinary Centre for Security, Reliability and Trust

Inria

Max Planck Institute for Informatics