Program

Time	Room: TBA
	Wednesday Oct. 01	Thursday Oct. 02	Friday Oct. 03
10:00 - 10:30	Coffee
10:30 - 12:00	Chair: TBD	Chair: TBD	Chair: TBD
	TBD	TBD	TBD
12:00 - 14:00	Lunch
14:00 - 15:30	Chair: TBD	Chair: TBD	Chair: TBD
	TBD	TBD	TBD
15:30 - 16:00	Coffee Break		-
16:00 - 17:30	Chair: TBD	Chair: TBD
	TBD	TBD

Confirmed Talks

Frank de Boer

Title: Contract-based proof system for actors

Abstract: sI will present a contract-based proof system for actors. Asynchronous method calls are specified and verified in terms of the contracts of the called methods. The interaction between actors is specified and verified using histories which consist of 3 kinds of events, which indicate a method call, a method selection, and a method return, respectively. Apart from a contract, a specification of a class consists of a local class invariant. We illustrate the proof system by a parametric specification and verification of an actor-based encoding of the good old dining philosophers.

Ferruccio Damiani

Title: A Language for Resilient Distributed Systems

Abstract: Choreographies and multitier programming are effective paradigms for simplifying the development of distributed systems by promoting modular, declarative designs while ensuring correctness properties. However, existing approaches often struggle with resilience to message loss and flexibility under dynamic and heterogeneous network topologies—critical challenges in real-world distributed systems.

In this talk, I introduce the Placed eXchange Calculus (PXC), a novel (yet unpublished) variant of the eXchange Calculus (XC ) aggregate programming framework, integrating placed data types from multitier programming. PXC combines the strengths of these frameworks, offering expressive and statically verifiable models for distributed computation while addressing resilience to unreliable networks and adapting to dynamic topologies. By leveraging placed data types, PXC supports heterogeneous devices with diverse capabilities, enabling fine-tuned optimizations and static checks of communication correctness across varying deployment environments.

Daniel Drodt

Title: Is the Rust’s Tokio Runtime Fair?

Abstract: Tokio is the most popular runtime for asynchronous Rust programs. Its scheduler gives informal fairness guarantees for the scheduled tasks. We formalize these guarantees and, using a Locally Abstract, Globally Concrete-style Rust semantics, attempt to show formally the fairness of Tokio’s scheduler.

Reiner Hähnle

Title: An LAGC Semantics for Timed Rebeca

Abstract: Timed Rebeca is an actor-based language for modeling and analyzing timed reactive systems. Timed Rebeca has a formal SOS-style semantics, as well as one in terms of rewrite rules. While the latter is suitable for model exploration and bounded model checking, it is less so for the purpose of deductive verification. Since we believe there is great potential in deductive verification of Timed Rebeca programs, as a preparatory step, in the present paper we provide a locally abstract, globally concrete (LAGC) semantics. This is a new approach to the semantic foundation of programming languages. An LAGC semantics is a highly modular, incremental trace semantics, particularly suited to ensure soundness of global program analyses such as deductive verification. We provide the first LAGC-style semantics for Timed Rebeca and discuss possible future applications.

Michael Lienhardt

Title: Orchestrating Multi-Physical Simulations

Abstract: A physical Simulator is a complex software dedicated to the simulation of a specific physical phenomenon (fluid, solid, light, chemistry, etc.). Consequently, to simulate multiple and interacting phenomena, we need to orchestrate several simulators together. This requires identifying which data should be communicated between which solver and at which point of the simulation. An important difficulty is that the exchange frequency may change at runtime, depending on the complexity of the physical phenomena at play. In this talk, we illustrate the difficulties related to such an orchestration and present a generic approach to express such an orchestration.

Michele Loreti

Title: A gentle introduction to YODA and its tools

Abstract: Modern software solutions are composed of many interacting entities, each with its own properties. These entities, called agents, operate without centralised control to reach local and global goals. To model and reason about these systems, tools are needed to specify not only the behaviour of entities, but also the environment where they operate. In this talk, the language YODA (Yet anOther agent Description lAnguage) is presented together with the tools that can be used to forecast emerging behaviour and to verify expected properties.

Jorge Pérez

Title: Asynchronous Session-based Concurrency: Deadlock Freedom by Typing

Abstract: In this talk, I will discuss asynchronous communication in the context of session-based concurrency, the model of computation in which session types specify the structure of the two-party protocols implemented by the channels of a communicating process. I will overview recent work on addressing the challenge of ensuring the deadlock-freedom property for message-passing processes that communicate asynchronously in cyclic process networks governed by session types. I will offer a gradual presentation of three typed process frameworks and outline how they may be used to guarantee deadlock freedom for a concurrent functional language with sessions.

Davide Sangiorgi

Title: asyncrony in process calculi

Abstract: This talk will be mainly a literature review on the meaning of asynchrony in process calculi. I will also discuss some recent ongoing work of mine on this subject (a collaboration with K. Sakayori, Tokyo)

Rudi Schlatte

Title: ABS status update

Abstract: Recent developments and status of the ABS toolchain

Riccardo Sieve

Title: BedreFlyt: Improving Patient Flows through Hospital Wards with Digital Twins

Abstract: Digital twins are emerging as a valuable tool for short-term decision-making as well as for long-term strategic planning across numerous domains. This talk reports on our ongoing work on designing a digital twin to enhance resource planning in a hospital ward. The proper handling of resources at a hospital is crucial to efficient operations. The dynamic allocation of resources is necessary to efficiently manage the workflow of patients and adjust it to avoid bottlenecks in operations, and to improve the prioritization and utilization of available resources. By connecting simulation models to live data, a digital twin can have more accurate simulations that reflect the actual resource allocation problems of a hospital ward. Our proposed solution uses the executable formal model to turn a stream of arriving patients, who need to be hospitalized, into a stream of optimization problems, e.g., capturing daily inpatient ward needs, that can be solved by SMT techniques. The knowledge base, which formalizes domain knowledge, is used to model the needed configuration in the digital twin, allowing the twin to support both short-term decision-making and long-term strategic planning by generating scenarios spanning average-case, worst-case resource needs, what-if scenarios and ward reconfiguration, depending on the expected flow of patients, as well as ranging over variations in available resources, e.g., bed distribution in different rooms, opening/closing of temporary rooms, etc. We illustrate our digital twin architecture by considering the problem of bed bay allocation in a hospital ward.

Asmae Heydari Tabar

Title: Title: Correctness-by-construction for ABS and verification of ABS programs, a full circle