ICFP 2024
Mon 2 - Sat 7 September 2024 Milan, Italy

This program is tentative and subject to change.

Mon 2 Sep 2024 14:30 - 15:00 at Orange 3 - Testing & Verification

Implementing concurrent systems based on asynchronous communications is intrinsically complex. In this work, we consider the formal framework TOAST for timed asynchronous interactions featuring mixed-choice states. TOAST extends the theory of timed asynchronous session types to support modelling of communication protocols featuring timeouts, that despite being commonplace in practice were previously out of reach for session type theory. We present ongoing work towards a practical toolchain that (a) automates the generation of correct-by-construction program stubs with timeouts in Erlang from TOAST protocols, and (b) provides an inline monitoring framework for TOAST protocols integrated with Erlang supervisors. Our toolchain generates Erlang code with a close correspondence to the source protocol by building on a formal correspondence between session types and Communicating Finite State Machines. The monitoring framework can be configured to perform either runtime verification or enforcement of process behaviour against the source protocol, ensuring communication safety.

This program is tentative and subject to change.

Mon 2 Sep

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:00 - 15:30
Testing & VerificationErlang at Orange 3
14:00
30m
Talk
Erla+: Translating TLA+ Models into Executable Actor-Based Implementations
Erlang
Marian Hristov University of Kaiserslautern-Landau, Annette Bieniusa University of Kaiserslautern-Landau
14:30
30m
Talk
Erlang on TOAST: Generating Erlang Stubs with Inline TOAST Monitors
Erlang
Jonah Pears , Laura Bocchi University of Kent, Raymond Hu Queen Mary University of London
15:00
30m
Talk
Is this really a refactoring? Automated equivalence checking for Erlang projects
Erlang
Bendegúz Seres Eötvös Loránd University, Dániel Horpácsi Eötvös Loránd University, Simon Thompson IOHK, University of Kent, and ELTE