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 Learning

In this tutorial on active automata learning algorithms, we will start with the
famous L * algorithm proposed by Dana Angluin in 1987, and explain how this
algorithm approximates the Nerode congruence by means of refinement. We will present a brief overview of the various improvements of the L * algorithm that have been proposed over the years, and show how these algorithms can be combined with conformance testing algorithms to obtain automata models of black-box reactive systems.

In the second part of the tutorial we will discuss various applications of active
automata learning, such as finding bugs in network protocol implementations, obtaining models of embedded software and hardware components, and refactoring of legacy software. We will also discuss extensions of L* to richer settings in which data and timing information is present.

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

Session Types for Message-Passing Concurrency

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

Reasoning about probabilistic programs

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

Graph transformation: theory (a little) and practice (a lot)

Theoretically, directed graphs can be understood as generalisations of
multisets, strings or trees. Like those simpler structures, graphs can
be rewritten on the basis of transformation rules. Sets of such rules,
called graph transformation systems or sometimes graph grammars, can be
understood as a mechanism to specify graph languages, relations between
graphs or state spaces. The theoretical underpinnings have been studied
in some depth, with roots in category theory.

Practically, directed graphs are a very intuitive way of understanding
many kinds of visual domain models, and can therefore be used as a
foundation for the syntax and semantics of diagrammatic modelling
languages, as well as for model transformation. For such more practical
uses, it is needful to enrich the simple notion of directed graphs and
simple rules with typing, attributes, rule control and quantification.

During this workshop, we briefly explore some of the foundations of
graph transformation, and more extensively go into their use in
practice. For the latter, we use the graph transformation tool GROOVE.
Workshop participants are expected to use this tool for small exercises
and case studies. You can prepare youself by installing the tool from
sf.nt/projects/groove. (It runs under Java 8, not yet under more recent versions of Java. Please make sure to have Java 8 installed by start of the course day. You can e.g. obtain it from https://adoptium.net/temurin/releases)
FRIDAY 17 June Henning Basold (UL)
Gemini-zuid 3A13

Introduction to Dependent Type Theory for Computer-Assisted Proofs

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.