IPAndemic afternoon Wednesday June 23rd 2021

Formal Methods

An IPA online afternoon (IPAndemic afternoon, if you will) will take place Wednesday, June 23rd, starting at 13:00 (social chat open at 12:30).

The afternoon has a formal methods flavour, with speakers from IPA’s formal methods ‘blood group’, and the afternoon will also feature introductory talks by some of the many IPA PhD students who joined IPA in the last year, as well as ample breaks and other opportunities to foster interaction.

After the last talk, the social chat (2D audio/video SpatialChat) will stay open, but it’ll be `bring your own drink’.

Confirmed speakers

Jeroen Keiren (TU/e)
Jorge Perez (RUG)
Jurriaan Rot (RU)
Freek Verbeek (OU and Virginia Tech)

Schedule

12:30 Social chat open

13:00 Opening — Loek Cleophas (IPA research school)

13:05–13:35 Freek Verbeek (OU and Virginia Tech) — Formally Proven Correct Algorithms For Decompilation. Decompilation aims at recovering source code out of an executable and is useful in security analyses, binary patching and formal verification. A perfect decompiler produces sound (functionally equivalent to the binary) and recompilable source code. Such a decompiler does not exist, as the decompilation problem is undecidable. We are studying an approach to formally proven correct decompilation that takes as input an executable and produces C code. We present preliminary results on FoxDec: a formally proven correct x86-64 decompiler and discuss its current possibilities as well as the work that needs to be done in order to obtain a fully formally proven correct decompilation tool.

13:35–14:05 Jeroen Keiren (TU/e) —Understanding Dekker’s Mutual Exclusion Algorithm using mCRL2’s counterexamples. In a recent IPA course, Jan Friso Groote and Tim Willemse introduced mCRL2. In this talk, we will show how the mCRL2 toolset was used to get a better understanding of Dekker’s mutual exclusion algorithm and the properties that it satisfies. We will first introduce Dekker’s algorithm and its history as the first algorithm to solve mutual exclusion between two processes. During this explanation, we will follow following Dijkstra’s 1962 paper “Over de sequentialiteit van procesbeschrijvingen” (EWD35), and show that some simplier attempts fail. Ultimately, we will show that starvation freedom of Dekker’s algorithm requires the assumption of strong fairness. This assumption is typically not mentioned explicitly in the literature.

30 min. break (social chat open)

14:35–15:05 Jorge Perez (RUG) — Session Types for Message-Passing Concurrency. Protocols provide the unifying glue in concurrent and distributed software today; verifying that message-passing programs conform to such governing protocols is important but difficult. Originated within concurrency theory and programming languages, session types are an approach to avoid protocol violations and deadlocks in message-passing programs.
In this talk, I will explain what session types are, illustrate them by examples, and discuss open research questions.

15:05–15:15 PhD intro talk: Jan Martens (TU/e)

15:15–15:25 PhD intro talk: Lukas Armborst (UT)

35 min. break (social chat open)

16:00–16:30 Jurriaan Rot (RU) — Learning weighted automata. Automata learning is a popular technique for inferring minimal automata through membership and equivalence queries. We describe the classical L* algorithm for DFA learning, and then move to weighted automata, which involve quantities – and provide some nice challenges for learning.
Based on joint work with Gerco van Heerdt, Clemens Kupke and Alexandra Silva.

16:30–ca. 17:30 Social chat open, `bring your own drink’

Registration

Registration has now closed. Please register ASAP (we just ask for your e-mail, first and last name, affiliation, and background (IPA / non-IPA, PhD student / staff member)

Registration closes Tuesday June 22nd 13:00, after which the meeting link (likely MS Teams) and details will be sent around.

IPAndemic online events beyond this one

We plan to offer an IPAndemic online event every 3–4 weeks, by default alternating between online course days (usually 10:00–16:00 with ample breaks) and afternoons (usually 13:00 until 17:30 including `bring your own drink’ socializing) with talks and networking such as this event.

Theme-wise, both event types will rotate over the three IPA `blood groups’ (Algorithmics & Complexity; Formal Methods; Software Engineering).