POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France

This program is tentative and subject to change.

Fri 16 Jan 2026 16:35 - 17:00 at Nef - Automata 2

We address the reachability problem for concurrent programs with an arbitrary number of threads running over the Intel x-86 architecture. We consider the formal model eTSO for Intel x-86 defined by Raad et al. in POPL 2022. This model takes into account multiple memory types and non-temporal writes, combining in a complex way features in the TSO and PSO weak memory models. In PLDI 2024, Abdulla et al. proved that this problem is undecidable for eTSO in general, but that it is decidable under $k$-alternation bounding when computations have, for some fixed bound $k$, at most $k$ alternations of TSO segments (with TSO writes only) and PSO segments (with PSO writes only) for each thread. The proof of this result assumes that the number of threads is fixed, and relies crucially on referring to thread identities. In this paper, we prove the decidability of the $k$-alternation bounded reachability problem of eTSO in the parametrized setting when the number of threads is a parameter that can be arbitrarily high. The proof is nontrivial as it cannot refer to thread identities, their number being unbounded. We show that it is possible to overcome this difficulty using a novel and quite complex reduction to reachability in well-structured systems on domains that are BQOs (Better Quasi Orders). This is the first time that BQO-based well-structured systems are used to prove the decidability of verification of infinite state programs.

This program is tentative and subject to change.

Fri 16 Jan

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

16:10 - 17:25
Automata 2POPL at Nef
16:10
25m
Talk
Counting and Sampling Traces in Regular Languages
POPL
Alexis de Colnet TU Wien, Kuldeep S. Meel University of Toronto, Umang Mathur National University of Singapore
DOI Pre-print
16:35
25m
Talk
Parametrised Verification of Intel-x86 Programs
POPL
Parosh Aziz Abdulla Uppsala University; Mälardalen University, Mohamed Faouzi Atig Uppsala University, Ahmed Bouajjani Université Paris Cité, K Narayan Kumar Chennai Mathematical Institute, Prakash Saivasan Institute of Mathematical Sciences
DOI
17:00
25m
Talk
General Decidability Results for Systems with Continuous Counters
POPL
A. R. Balasubramanian Technical University of Munich, Matthew Hague Royal Holloway University of London, Rupak Majumdar MPI-SWS, Ramanathan S. Thinniyam Uppsala University, Georg Zetzsche MPI-SWS
DOI