SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025

This program is tentative and subject to change.

Thu 16 Oct 2025 13:45 - 14:00 at Orchid West - Reasoning

We study the implementability problem for an expressive class of symbolic communication protocols involving multiple participants. Our symbolic protocols describe infinite states and data values using dependent refinement predicates. Implementability asks whether a global protocol specification admits a distributed, asynchronous implementation, namely one for each participant, that is deadlock-free and exhibits the same behavior as the specification. We provide a unified explanation of seemingly disparate sources of non-implementability through a precise semantic characterization of implementability for infinite protocols. Our characterization reduces the problem of implementability to (co)reachability in the global protocol restricted to each participant. This compositional reduction yields the first sound and relatively complete algorithm for checking implementability of symbolic protocols. We use our characterization to show that for finite protocols, implementability is co-NP-complete for explicit representations and PSPACE-complete for symbolic representations. The finite, explicit fragment subsumes a previously studied fragment of multiparty session types for which our characterization yields a PTIME decision procedure, improving upon a prior PSPACE upper bound.

This program is tentative and subject to change.

Thu 16 Oct

Displayed time zone: Perth change

13:45 - 15:30
ReasoningOOPSLA at Orchid West
13:45
15m
Talk
Characterizing Implementability of Global Protocols with Infinite States and Data
OOPSLA
Elaine Li NYU, Felix Stutz University of Luxembourg, Luxembourg, Thomas Wies New York University, Damien Zufferey SonarSource
14:00
15m
Talk
Checking Observational Correctness of Database Systems
OOPSLA
Lauren Pick The Chinese University of Hong Kong, Amanda Xu University of Wisconsin-Madison, Ankush Desai Amazon Web Services, Sanjit A. Seshia University of California, Berkeley, Aws Albarghouthi University of Wisconsin-Madison
14:15
15m
Talk
Correct Black-Box Monitors for Distributed Deadlock Detection: Formalisation and Implementation
OOPSLA
Radosław Jan Rowicki Technical University of Denmark, Adrian Francalanza University of Malta, Alceste Scalas Technical University of Denmark
DOI Pre-print
14:30
15m
Talk
Correct-By-Construction: Certified Individual Fairness through Neural Network Training
OOPSLA
Ruihan Zhang Singapore Management University (SMU), Jun Sun Singapore Management University
14:45
15m
Talk
Modular Reasoning about Global Variables and Their Initialization
OOPSLA
João Pereira ETH Zurich, Isaac van Bakel ETH Zurich, Patricia Firlejczyk ETH Zurich, Marco Eilers ETH Zurich, Peter Müller ETH Zurich
15:00
15m
Talk
P³: Reasoning about Patches via Product Programs
OOPSLA
Arindam Sharma Imperial College London, Daniel Schemmel Imperial College London, Cristian Cadar Imperial College London
15:15
15m
Talk
Reasoning about External Calls
OOPSLA
Julian Mackay Kry10 Ltd, Sophia Drossopoulou Imperial College London, James Noble Independent. Wellington, NZ, Susan Eisenbach Imperial College London