Photo by Maxime Dufour

Invited Speakers

DisCoTec 2025 has invited speakers to give keynote talks and tutorials.

Keynote Talks

DisCoTec 2025 will host a keynote talk at each conference as well as a DisCoTec-wide keynote. The invited speakers are Alysson Bessani (DAIS), Hélène Coullon (DisCoTec-wide), Omar Inverso (COORDINATION), and Burcu Ozkan (FORTE).

Alysson Bessani (Universidade de Lisboa, Portugal) - DAIS

Alysson Bessani is a professor of the University of Lisbon Faculty of Sciences, Portugal, and the director of the LASIGE research unit. He received his Ph.D. in Electrical Engineering from UFSC (Brazil) in 2006, was a visiting professor at Carnegie Mellon University (2010) and a visiting researcher at Microsoft Research Cambridge (2014).

Alysson coordinated/collaborated in 13 international projects and co-authored more than 120 peer-reviewed publications on dependability, security, Byzantine fault tolerance, and cloud storage. He is also the principal researcher behind the BFT-SMaRt consensus library and a co-founder of the Vawlt dependable & secure cloud storage startup. More information about him can be found at http://www.di.fc.ul.pt/~bessani.

Hélène Coullon (IMT Atlantique, France) - DisCoTec-wide

Title: Efficient Reconfigurations with Programmable Life Cycles: Contributions to Safety, Declarativity, and Decentralization

Abstract: Large distributed software systems are now ubiquitous. A distributed system is typically deployed on heterogeneous distributed infrastructures with deployment dependencies between software entities that require coordination mechanisms. Once deployed, distributed systems may need to be reconfigured. Reconfiguring a system consists of changing the configuration while the system is running.

Reconfigurations are critical procedures typically triggered when: the system enters an invalid or unstable state because of internal or external events or needs to be optimized (or updated) for energy, security, or quality-of-service reasons. As a consequence, reconfiguration should be done as fast as possible.

Reconfiguration procedures manipulate a cornerstone element: the life cycles of software entities. In this presentation, I present a full study on introducing programmable life cycles of software entities and their automatic coordination during reconfigurations. This programmability offers more opportunities for parallelism and concurrency. In consequence, programmable life cycles significantly reduce the execution time of reconfigurations. However, as more complexity is introduced, it is more difficult to guarantee other good properties offered in the literature: the safety of reconfigurations; the declarativity of reconfigurations; and the decentralization of the reconfiguration process.

In this presentation, I will explore the feasibility of all these properties combined with programmable life cycles.

Bio: Hélène Coullon is an associate professor at IMT Atlantique, France. She received her Ph.D. in 2014 from the University of Orléans (France). Her research topics are large-scale distributed and geo-distributed systems, in particular their deployment and dynamic reconfiguration. She combines expertise from different fields including Component-Based Software Engineering (CBSE), Infrastructure-as-Code (IaC), formal methods and languages, parallelism, and domain specific languages.

Omar Inverso (GSSI, Italy) - COORDINATION

Title: Towards Automated Analysis of Emerging Behaviour: Preliminary Insights and Research Directions

Abstract: In several classes of collective systems, sophisticated dynamics may occur for the combined effect of the elementary actions of the individuals. For instance, foraging ants in a colony are able to collectively work out the most convenient path while carrying food back to their nest. Somehow similarly, unintended order may arise spontaneously among the involved parties of some economic systems.

Fascinating phenomena of this kind are studied in a variety of disciplines, from biology to physics, where the main challenge is to understand the relationship between the way individuals behave in isolation and what happens over time at a global level in the system.

This talk summarises a few proofs of concept on the automated analysis of different systems, such as stable matchings, flocks of birds, colonies of ants, and applauding audiences, and relevant emerging properties thereof. The underlying methodology follows an integrated approach to formal specification and analysis to leverage intuitive specification languages as well as existing mature verification technology and decision procedures for general-purpose applications.

Bio: Omar Inverso is an associate professor at the Gran Sasso Science Institute in L’Aquila, Italy. His research interests include formal languages and methods, automated analysis, and decision procedures, with applications to concurrent and distributed systems, and so-called collective or complex systems at large.

Burcu Kulahcioglu Ozkan (TU Delft, The Netherlands) - FORTE

Title: From Formal Methods to Testing of Distributed Systems

Abstract: Distributed systems are prone to software bugs due to the concurrency of distributed events and potential network and process faults during execution. Detecting these bugs is notoriously challenging because they often occur only in specific, subtle interleavings of the events. In principle, these bugs could be detected by model-checking techniques, which explore all possible event schedules. However, systematic exploration does not scale to large distributed systems, and it is only practical to test a subset of their executions. Alternatively, randomized testing is a practical method to apply to large systems, but it comes with limitations in its effectiveness.

Our recent works narrow the gap between formal verification and randomized testing of distributed systems, bringing together the effectiveness of formal methods and the practicality of randomized testing. In this talk, we will overview the key ideas in our recent works and discuss how transferring ideas from formal methods and verification improves the effectiveness of randomized test generation.

Bio: Burcu Kulahcioglu Ozkan is an assistant professor and Delft Technology Fellow in the Software Engineering Research Group at TU Delft. She received her PhD from Koç University in Istanbul, Turkey, followed by postdoctoral research at the Max Planck Institute for Software Systems (MPI-SWS) in Kaiserslautern, Germany. Her research focuses on formal methods, model checking, software testing, and debugging of concurrent programs and distributed systems. She is a recipient of the academic research awards and grants from Amazon Research and Stellar Development Foundation.

Tutorials

DisCoTec 2025 will host a tutorial at each conference. The invited speakers are Baptiste Jonglez (DAIS), Robbert Krebbers (COORDINATION), and Emilio Tuosto (FORTE).

Baptiste Jonglez (Inria, France) - DAIS

Title: Driving distributed system experiments on the edge-to-cloud continuum with EnOSlib

Abstract: EnOSlib is a Python library that facilitates the design and execution of reproducible experiments across distributed computing infrastructures. Originally developed to simplify experimentation on testbeds such as Grid’5000 and Chameleon Cloud, its scope is expanding to include edge testbeds. In addition, edge-to-cloud experiments are facilitated thanks to a new feature: EnOSlib now supports multi-provider deployments, allowing simultaneous resource reservation and deployment across several diverse testbeds at the same time.

EnOSlib also provides reusable services, for example fine-grained energy measurements, automated Kubernetes cluster deployments, classical monitoring stacks, or enhanced network emulation. All these features enable users to model and study complex, realistic scenarios such as latency-sensitive edge-to-cloud applications.

The tutorial illustrates these capabilities through a distributed video processing use-case that spans edge and cloud platforms.

Robbert Krebbers (Radboud University Nijmegen, The Netherlands) - COORDINATION

Title: Mechanized Type Soundness for Substructural Types using Iris

Abstract: Substructural type systems are a good fit to enforce strong safety properties of higher-order, imperative and concurrent programs. Key examples are the Rust type system (which enforces the absence of undefined behavior and data races) and session types (which enforce correct usage of message-passing channels). Formally proving that these type systems “do their job” (i.e., they enjoy the “type soundness” property) is challenging. This challenge is exacerbated when considering combinations of language features (“feature interaction”) and linking against “unsafe” libraries (which have to be verified manually), thus providing the desire for a scalable approach with support for machine-checked proofs.

In this tutorial I will give an introduction to the “logical approach” to type soundness, which is well-suited to prove soundness of substructural type systems. I will explain the theory of the logical approach in the context of a very simple language, which I then gradually scale up to a session-typed language. I will also demonstrate that the logical approach is well-suited for the mechanization of challenging type systems in the Rocq proof assistant using the Iris framework for concurrent separation logic.

Emilio Tuosto (GSSI, Italy) - FORTE

Title: A choreographic view of Smart Contracts

Joint work with Elvis Konjoh Selabi (UniCam and GSSI), Maurizio Murgia (GSSI), and António Ravara (NOVA, Lisbon).

Abstract: We recently proposed a coordination model that blends together ideas from smart contracts, choreographies, and typestates to formalise and reason about interactions of distributed components. Our framework is based on symbolic finite-state machines dubbed DAFSMs (after Data-Aware Finite-State Machines) to holistically capture coordination protocols which, akin smart contracts, expose an API that distributed components use to interact according to the role they play in the protocol. As global specifications such as global types, DAFSMs allow us to define so-called well-formedness properties, while abstracting away from run-time details such as the number of number of components’ instances enacting the roles of the protocol. Interestingly DAFSMs can represent data-dependency. This is a quintessential aspect to handle properties that, like well-formedness, depend on the payloads of components’ interactions such as those typical in smart contracts.

The tutorial will show how to use DAFSMs to formalise coordination protocols and analyse their well-formedness using a Tool for Resource-Aware Coordination (TRAC), designed to support our approach.