POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
Thu 15 Jan 2026 11:35 - 12:00 at Nef - Concurrency: Testing and Verification Chair(s): Ramanathan S. Thinniyam

A key computational question underpinning the automated testing and verification of concurrent programs is the \emph{consistency question} — \emph{given a partial execution history, can it be completed in a consistent manner?} Due to its importance, consistency testing has been studied extensively for memory models, as well as for database isolation levels. A common theme in all these settings is the use of shared-memory as the primal mode of interthread communication. On the other hand, modern programming languages, such as Go, Rust and Kotlin, advocate a paradigm shift towards channel-based (i.e., message-passing) communication. However, the consistency question for channel-based concurrency is currently poorly understood.

In this paper we lift the study of fundamental consistency problems to channels, taking into account various input parameters, such as the number of threads executing, the number of channels, and the channel capacities. We draw a rich complexity landscape, including upper bounds that become polynomial when certain input parameters are fixed, as well as hardness lower bounds. Our upper bounds are based on algorithms that can drive the verification of channel consistency in automated verification tools. Our lower bounds characterize minimal input parameters that are sufficient for hardness to arise, and thus shed light on the intricacies of testing channel-based concurrency. In combination, our upper and lower bounds characterize the boundary of \emph{tractability/intractability} of verifying channel consistency, and imply that our algorithms are often (nearly) optimal. We have also implemented our main consistency checking algorithm
and designed optimizations to enhance its performance. We evaluated the performance of our implementation over a set of 103 instances obtained from open source Go projects, and compared it against a constraint-solving based algorithm. Our experimental results demonstrate the power of our consistency-checking algorithm; it scales to around 1M events, and is significantly faster in running-time performance, compared to a constraint-solving approach.

Thu 15 Jan

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

10:20 - 12:00
Concurrency: Testing and VerificationPOPL at Nef
Chair(s): Ramanathan S. Thinniyam Uppsala University
10:20
25m
Talk
(TOPLAS) Will it Fit? Verifying Heap Space Bounds of Concurrent Programs under Garbage Collection
POPL
Alexandre Moine New York University, Arthur Charguéraud Inria, François Pottier Inria
DOI
10:45
25m
Talk
Verifying Almost-Sure Termination for Randomized Distributed Algorithms
POPL
Constantin Enea LIX, CNRS, Ecole Polytechnique, Rupak Majumdar MPI-SWS, Harshit Jitendra Motwani MPI-SWS, V.R. Sathiyanarayana MPI-SWS
DOI
11:10
25m
Talk
Zoo: A Framework for the Verification of Concurrent OCaml 5 Programs using Separation Logic
POPL
Clément Allain INRIA, Gabriel Scherer Université Paris Cité - Inria - CNRS
DOI
11:35
25m
Talk
The Complexity of Testing Message-Passing Concurrency
POPL
Zheng Shi National University of Singapore, Lasse Møldrup Aarhus University, Umang Mathur National University of Singapore, Andreas Pavlogiannis Aarhus University
DOI Pre-print