Program

The workshop will take place at the Department of Computer Science of the Faculty of Sciences of the University of Porto, room FC6.106 FC6.142 of building FC6.

Time	Building FC6, room FC6.142 (first floor - entrance is on the ground floor)
	Wednesday Oct. 01	Thursday Oct. 02	Friday Oct. 03
10:00 - 10:20	Coffee	Coffee
10:20 - 10:30	José Proença and S. Lizeth Tapia Tarifa: Welcome and Practicalities
10:30 - 12:00	Chair: Einar Broch Johnsen	Chair: Frank de Boer	Chair: Ferruccio Damiani
10:30 - 11:15	Davide Sangiorgi: asyncrony in process calculi	Charaf Eddine Dridi: Resource Contracts for Active Objects	Jorge Pérez: Asynchronous Session-based Concurrency: Deadlock Freedom by Typing
11:15 - 12:00	Ferruccio Damiani: A Language for Resilient Distributed Systems	Ulises Torrella: Fair Termination for Resource-Aware Active Objects	Maurice ter Beek and José Proença: Towards Asynchronous Communication in Team Automata
12:00 - 14:00	Lunch
14:00 - 15:30	Chair: Rudi Schlatte	Chair: S. Lizeth Tapia Tarifa	Chair: Violet Ka I Pun
14:00 - 14:45	Daniel Drodt: Is the Rust’s Tokio Runtime Fair?	Reiner Hähnle: An Introduction to LAGC Semantics	Riccardo Sieve: BedreFlyt - Improving Patient Flows through Hospital Wards with Digital Twins
14:45 - 15:30	Michele Loreti: A gentle introduction to YODA and its tools	Frank de Boer: First Order Hybrid Separation~Logic	Michael Lienhardt: Resource Contracts for Active Objects
15:30 - 16:00	Coffee Break		-
16:00 - 17:30	Chair: Volker Stolz	Chair: Reiner Hähnle
16:00 - 16:45	Frank de Boer: Contract-based proof system for actors	Rudi Schlatte: ABS and update in its status
16:45 - 17:30	Einar Broch Johnsen: Declarative Dynamic Object Reclassification	Discussion

Abstracts of the Talks

Wednesday, 1st of October.

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)

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.

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.

Frank de Boer

Title: Contract-based proof system for actors

Abstract: I 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.

Einar Broch Johnsen

Title: Declarative Dynamic Object Reclassification

Abstract: In object-oriented languages, dynamic object reclassification is a technique to change the class binding of an object at runtime. Current approaches express when and how to reclassify inside the program’s business code, while maintaining internal consistency. These approaches are less suited for programs that need to be consistent with an external context, such as autonomous systems interacting with a knowledge base. This talk presents declarative dynamic object reclassification, a novel technique that provides a separation of concerns between a program’s business code and its adaptation logic for reclassification, expressed via a knowledge base. We present Featherweight Semantically Reflected Java, a minimal calculus for declarative dynamic object reclassification that enables the programmer to define consistency both internally (using a type system) and externally (using declarative classification queries). We use this calculus to study how internal and external consistency interact for declarative dynamic object reclassification. We further implement the technique by extending SMOL, a language for reflective programming via external knowledge bases.

Thursday, 2nd of October.

Charaf Eddine Dridi

Title: Resource Contracts for Active Objects [Slides]

Abstract: Workflows coordinate tasks across departments or organisations, where correct execution depends not only on control dependencies but also on the availability of shared resources. This paper presents ReAct, a resource-aware active object language for workflow modelling. In ReAct, method declarations serve as contracts: they specify alternative resource profiles in their signatures, giving methods multiple execution options when resources are limited. Methods can be invoked only once their dependency conditions are satisfied; at activation, a feasible resource profile is then selected and allocated. We encode the language in Maude and show how workflows can be executed, simulated, and verified against their declared dependencies and resource requirements.

Ulises Torrella

Title: Fair Termination for Resource-Aware Active Objects

Abstract: Active object systems are a model of distributed computation that has been adopted for modelling distributed systems and business process workflows. This field of modelling is, in essence, concurrent and resource-aware, motivating the development of resource-aware formalisations on the active object model. The contributions of this work are the development of a core calculus for resource-aware active objects together with a type system ensuring that well-typed programs are fairly terminating, i.e., they can always eventually terminate. To achieve this, we combine techniques from graded semantics and type systems, which are quite well understood for sequential programs, with those for fair termination, which have been developed for synchronous sessions.

Reiner Hähnle

Title: An Introduction to LAGC Semantics

Abstract: Formal, mathematically rigorous programming language semantics are the essential prerequisite for the design of logics and calculi that permit automated reasoning about concurrent programs. This talk introduces Locally Abstract Globally Concrete semantics, which separates local evaluation of expressions and statements performed in an abstract, symbolic environment from their composition into global computations, at which point they are concretised. This makes incremental addition of new language concepts possible, without the need to revise the framework. The basis is a generalisation of the notion of a program trace as a sequence of evolving states that are enriched with event descriptors and trailing continuation markers. This allows to postpone scheduling constraints from the level of local evaluation to the global composition stage, where well-formedness predicates over the event structure declaratively characterise a wide range of concurrency models.

Frank de Boer

Title: First Order Hybrid Separation~Logic

Rudi Schlatte

Title: ABS status update

Abstract: Recent developments and status of the ABS toolchain

Title: Discussion

Possible topics: (1) further development of the ABS language and runtime, (2) use-cases used to showcase different asynchronous models, (3) APM2026, (4) …

Friday, 3rd of October.

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.

Maurice ter Beek and José Proença

Title: Towards Asynchronous Communication in Team Automata

Abstract: Team Automata is a formalism for interacting component-based systems proposed in 1997, whereby multiple sending and receiving actions from concurrent automata can synchronise, and since then, team automata have been studied and applied in many different contexts. In this talk, we first revisit the specific notion of constrained multi-party synchronisation in the composition of team automata. We then focus on several aspects that we recently investigated for team automata, like communication properties (can receptiveness and responsiveness be guaranteed?), realisability (how to decompose a global model into local components?), featured team automata (integrating variability to permit family-based analysis), and tool support (what has been implemented?). After this snapshot of recent research on team automata, we unveil ongoing research on implementing asynchronous communication in team automata and the possible impact on communication properties and realisability.

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.

Michael Lienhardt

Title: Orchestrating Multi-Physical Simulations [Slides]

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.