EuroProofNet

EuroProofNet
COST action CA20111

Université de Liège

Université de Liège

Université du Luxembourg

Université du Luxembourg

Inria

Inria

Max-Planck-Institut für Informatik

Max-Planck-Institut für Informatik

EuroProofNet Summer School on Verification Technology, Systems & Applications 2022

The summer school on verification technology, systems & applications takes place at the Max Planck Institute for Informatics, Saarbrücken, Germany from September 5 - September 9, 2022. 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 Frédéric Blanqui, Carsten Fuhs, André Platzer, Philipp Rümmer, and Martina Seidl 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. Recommendations on hotels can be found below. EuroProofNet can refund the travel and accommodation of a number of participants (the daily allowance for accommodation and meals is 100 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 follwing links: Eligibility Reimbursement Rules

Application

Please apply electronically by sending an email to Jennifer Müller including

by July 20, 2022. Notifications on acceptance/rejection will be given by July 22, 2022.

Registration

Registration will be open to accepted applicants starting on July 22, 2022. Registration links have been send via eMail.

Program

Schedule

All lectures take place in room 002, building E1 5.

September 5
Monday
September 6
Tuesday
September 7
Wednesday
September 8
Thursday
September 9
Friday
08.00 - 08.45 Registration
08.45 - 09.00 Welcome
09.00 - 12.30 Martina Seidl Philipp Rümmer Carsten Fuhs André Platzer André Platzer
12.30 - 14.00 Lunch break
14.00 - 17.30 Carsten Fuhs Martina Seidl Frédéric Blanqui Philipp Rümmer Frédéric Blanqui
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.

Lecturer(s)

Frédéric Blanqui
Frédéric Blanqui

Interoperability of proof systems

In contrast with other technological areas, it is very difficult to make proof systems interoperate because proof systems are generally based on different and sometimes incompatible axioms or deduction rules. One promising way to enable interoperability whenever it is possible is by representing the axioms, deduction rules and proofs of the various systems in a logical framework so that a feature that is common to several systems is encoded in the same way.

In this lecture, I will present the logical framework called the λΠ-calculus modulo rewriting and its implementation in the tool Dedukti, and the tool Lambdapi which extends Dedukti with implicit arguments and tactics. I will show how to encode various logical or type systems in Dedukti, from first-order logic used in automated theorem provers, to higher-order logic used in proof assistants HOL, Isabelle or PVS, and to advanced type systems like the calculus of constructions with a linear infinite hierarchy of type universes used in the proof assistants Coq, Agda or Lean. For automated theorem provers, I will show how one can reconstruct proofs in Dedukti from TSTP files.

Slides: [Part 1] [Part 2]

Carsten Fuhs
Carsten Fuhs

Automated Termination and Complexity Analysis of Programs

Termination of a program means that regardless of the input to the program, its computations will always come to a halt. Although this property is undecidable, fully automated techniques and tools have flourished in recent years. This is witnessed also by the International Termination and Complexity Competition (termCOMP) as well as the Termination Category of the Competition on Software Verification (SV-COMP).

In the first part of this course, we will discuss approaches to automated termination analysis in several settings. On the one hand, we consider Term Rewrite Systems (TRSs) and Integer Transition Systems (ITSs), which have concise formal definitions and capture the core of many programming languages. On the other hand, we consider program analysis techniques for practically used programming languages such as Java or Haskell. These language-specific techniques extract TRSs or ITSs (or combinations thereof) whose termination (analysed separately) implies termination of the original program.

However, termination alone is not always enough. Complexity analysis is a refinement of termination analysis that has received a lot of attention in recent years. Here questions like "given a program P, how many steps does it take in the worst case to execute P on an input of size at most n?" are addressed. Corresponding program analysis tools have been developed and deployed for a variety of settings, including TRSs, ITSs, and real-world programming languages. To the above question, tools may provide answers such as "running P on an input of size at most n needs O(n^2) many steps". In the second part of the course, we will discuss a selection of techniques that are used by such tools for automated complexity analysis. As we shall see, a number of techniques from termination analysis can be revisited to yield powerful complexity analysis techniques.

[Course Materials]

André Platzer
André Platzer

Logic of Autonomous Dynamical Systems

This talk highlights some of the most fascinating aspects of the logic of dynamical systems which constitute the foundation for developing cyber-physical systems (CPS) such as robots, cars and aircraft with the mathematical rigor that their safety-critical nature demands. Differential dynamic logic (dL) provides an integrated specification and verification language for dynamical systems, such as hybrid systems that combine discrete transitions and continuous evolution along differential equations. In dL, properties of the global behavior of a dynamical system can be analyzed solely from the logic of their local change without having to solve the dynamics.

In addition to providing a strong theoretical foundation for CPS, differential dynamic logics as implemented in the KeYmaera X prover have been instrumental in verifying many applications, including the Airborne Collision Avoidance System ACAS X, the European Train Control System ETCS, automotive systems, mobile robot navigation, and a surgical robotic system for skull-base surgery. dL is the foundation to provable safety transfer from models to CPS implementations and is also the key ingredient behind autonomous dynamical systems for Safe AI in CPS.

References:
André Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018. DOI:10.1007/978-3-319-63588-0
André Platzer. Logics of dynamical systems LICS, 2012: 13-24. DOI:10.1109/LICS.2012.13

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

Philipp Rümmer
Philipp Rümmer

Solving Constraints with Complex String Operations

Over the last couple of years, a number of new SMT and constraint solvers have been proposed that can check satisfiability of quantifier-free formulas over a background theory of strings and string operations. String solvers can be applied in different verification algorithms, for instance in symbolic execution to check path feasibility, in software model checking to take care of implication checks; a prime application area is security analysis for languages like JavaScript and PHP, for instance to discover vulnerability to injection attacks.

After a general introduction to the field, this lecture will focus on methods for handling constraints with complex string operations. It will present decidability results and concrete algorithms for constraints including "real-world" regular expressions; matching, extraction, concatenation; different forms of replace and replace-all operations; encoders/decoders; string length, counting, and sub-string extraction. Along the way, the lecture will cover various flavours of finite-state automata that are useful to construct solvers.

[Course Materials]

Martina Seidl
Martina Seidl

Reasoning with Quantified Boolean Formulas

Many application problems from artificial intelligence, verification, and formal synthesis can be efficiently encoded as quantified Boolean formulas (QBFs), the extension of propositional logic with quantifiers. This extension makes the QBF decision problem PSPACE-complete (in contrast to SAT which is NP-complete).

Over the last years much progress has been made concerning the theory and practice of QBF research. In this lecture, we review the state of the art of QBF technology and show how to perform automated reasoning with QBFs. This lecture will include practical exercises.

[Course Materials]

Accommodation

Participants are responsible for their own accommodation arrangements.

We have reserved rooms at a special rate in the following hotels. Please book the rooms yourself by sending an email to the hotel using the keyword "VTSA22".

Please note that different cancellation policies apply.

Arrival / Directions

The Summer School 2022 will take place at the Max Planck Institute for Informatics (MPI-INF), on the Saarland Informatics Campus of Saarland University in Saarbrücken. Please note that all lectures will take place in building E1 5 (Building of MPI-SWS). For more information on Saarbrücken, you can also check here.

Travelling to MPI-INF

General instructions to the MPI-INF

Public Transportation between the City and the MPI-INF

Use the Online Travel Information System. The nearest bus station on Campus is "Universität Mensa".


General Locations and Tips

There are lots of cozy little pubs and cafés in Saarbrücken, especially near St. Johanner Markt. A few examples:

  • Pizza Gotti
    Mainzer Straße 8
    66111 Saarbrücken
  • Kulturcafé
    Sankt Johanner Markt 24
    66111 Saarbrücken
  • Sausalitos
    St. Johanner Markt 7-9
    66111 Saarbrücken
  • Iguana
    Mainzer Strasse 2
    66111 Saarbrücken
  • Alex
    Saarstraße 15
    66111 Saarbrücken

Organization and Contact

General Organization

Local Organization

Website

For comments or questions, please send an email to Jennifer Müller and Anna Rossien.

This time, the summer school is organized under the umbrella of the COST Action EuroProofNet (CA20111) 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: 2022/07/20
Notification until: 2022/07/22
Summer School: 2022/09/05 - 2022/09/09
(Format is YYYY/MM/DD)

Photos

click to enlarge

EuroProofNet
COST action CA20111

Université de Liège

Université du Luxembourg

Inria

Max-Planck-Institut für Informatik

Interdisciplinary Centre for Security, Reliability and Trust

COST (European Cooperation in Science and Technology) is a funding agency for research and innovation networks. Our Actions help connect research initiatives across Europe and enable scientists to grow their ideas by sharing them with their peers. This boosts their research, career and innovation.

COST Acknowledgement