# Course: Formal Methods 2022

Eindhoven University of Technology, Eindhoven

Monday June 13 – Friday June 17, 2022

IPA organises *Advanced Courses* on each of its major research fields: Algorithmics and Complexity, Formal Methods and Software Technology. Each of these Advanced Courses intends to give an overview of (part of) the research of IPA in this specific field.

This Advanced Course focusses on subject areas in formal methods where successful research is being conducted by groups in or affiliated with IPA. From several of these areas, topics are taken to which an entire course day is dedicated. Course days consist of lectures mixed with active training (exercises, assignments, etc.).

#### Dates, Locations and Programme

The lectures will take place in various rooms on the campus of Eindhoven University of Technology. See https://www.tue.nl/en/our-university/tue-campus/ for information on how to reach the campus, and where to find the respective buildings.

The overall schedule of the course is as follows: course days will start at 10.00 and last until approximately 16.30 hours. Short coffee breaks are planned mid-morning and mid-afternoon and an organised lunch break 12.15-13.30 with lunch.

*On Tuesday June 14th, the course day will be followed by drinks 16:30–17:30 and a buffet diner (Indonesian “rijsttafel”) 17:30—ca. 19:30.*

MONDAY 13 June | Joshua Moerman (OU) and Frits Vaandrager (RU) |

Auditorium, Senaatszaal | Introduction to Active Automata LearningIn this tutorial on active automata learning algorithms, we will start with the In the second part of the tutorial we will discuss various applications of active Next, we will introduce L # , a new and simple approach to active automata learning. Instead of focusing on equivalence of observations, like the L * algorithm and its descendants, L # takes a different perspective: it tries to establish apartness, a constructive form of inequality. The course will be accompanied by examples and exercises with the LearnLib tool and prepare participants to apply automata learning in practice. |

TUESDAY 14 June | Jorge Perez and Dan Frumin (RUG) |

De Zwarte Doos, Filmzaal |
This course day will offer participants an overview of the key concepts of session types, a type-based approach for communication correctness in message-passing concurrent programs. Session types have been intensively developed within different research communities (notably, concurrency theory, programming languages, and software engineering) in the last 20 years. The course day describes these developments in two parts. In the first part, participants will be exposed to basic concepts of session types, in binary and multiparty formulations. The second part analyzes these concepts from the perspective of “propositions as sessions”, the correspondence that elegantly connects session types and linear logic in the style of the Curry-Howard isomorphism. After the course day, participants will have a high-level understanding of how session types offer a rigorous, paradigm-independent verification methodology for message-passing programs. They will also have an essential understanding of the key literature and open research problems in this area. |

De Zwarte Doos, Grand Café |
Drinks 16:30–17:30 and a buffet diner (Indonesian “rijsttafel”) 17:30—ca. 19:30. |

WEDNESDAY 15 June | Joost-Pieter Katoen (RWTH Aachen) |

Auditorium, Senaatszaal |
Probabilistic programs describe recipes on how to infer statistical
conclusions about data from a complex mixture of uncertain data and
real-world observations. They are ubiquitous. They steer autonomous
robots and self-driving cars, are key to describe security mechanisms,
naturally code up randomised algorithms, and are rapidly encroaching AI.
Probabilistic programming aims to make probabilistic modeling and
machine learning accessible to the programmer.
Probabilistic programs are hard to grasp, let alone automatically
checkable. Are they doing the right thing? What’s their precision? These
questions are notoriously hard — even the most elementary question “does
a program halt with probability one?” is “more undecidable” than the
halting problem. Bugs thus easily occur. Hard guarantees are called for.
The objective of this one-day course is to give insight into what
probabilistic programming is (using webPPL) and will present a formal
verification framework using weakest preconditions a la Dijkstra. |

THURSDAY 16 June | Arend Rensink (UT) |

Gemini-zuid 3A13 |
Theoretically, directed graphs can be understood as generalisations of Practically, directed graphs are a very intuitive way of understanding During this workshop, we briefly explore some of the foundations of |

FRIDAY 17 June | Henning Basold (UL) |

Gemini-zuid 3A13 |
At the very heart of formal logic sits the notion of proof verification
and proof search, which form an intriguing connection between logic
and computation. The part of this connection that we will focus on in
this course is the proofs-as-programs interpretation. This
interpretation states that proving a proposition is the same as writing
a program, and thus devising a logic with a proof system is the same as
developing a corresponding programming language!
We will discuss the simply-typed λ-calculus, which provides a proof
system for propositional logic, and show how computations relate to
proof tree manipulations. After this warm-up, we will discuss why
dependent type systems are required in mathematical and computer
science practice and how they can account for first order logic.
This course will be accompanied by examples and exercises in the system
Agda. We will use this system to demonstrate how the computer can assist
in larger proofs, and to show more advanced reasoning techniques.
In particular, we will reason about primitive recursion with induction
and general recursion with coinduction.
The course and the exercises in Agda will prepare participants to
implement and verify properties of fairly complex mathematical theories
and computer programs in proof-assistants that are based on dependent
type theory. |

#### Registration

Please register via this form. Registration is available until Monday June 6th at 10:00.

As always, IPA PhD candidates can attend for free. For others, details on pricing will be made available upon request.

#### Accommodation

Overnight accommodation is ** not** included by default for this course. The schedule is set up in such a way that it is feasible for many students to commute. In the event this is not feasible (mainly: PhD candidates based at RUG or UT), let us know and we will arrange basic overnight accommodation. You can specify your accommodation needs on the registration form.