POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
Tue 13 Jan 2026 14:45 - 15:07 at Belvédère - Program verification Chair(s): Clement Pit-Claudel

This paper introduces a novel proof technique to show that parallel or distributed programs exhibit confluent behavior, even when the execution of these programs is inherently non-deterministic. The proposed method allows us to prove the confluence of programs for which standard properties such as strong confluence or commutativity of operations do not hold. Our technique builds on a method to prove the confluence of rewrite systems by de Bruijn, which we first adapt and formalize in Rocq. This method can be seen as a specialized induction principle for proving confluence. The paper further considers how this induction principle can be used in the context of programming languages. We show how the proof method can be instantiated to establish confluence conditions for programs in a small Actor-like programming language and demonstrate the application of the method to prove the confluence of a class of programs that cannot be proven to have deterministic behaviours by standard techniques.

Tue 13 Jan

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

14:00 - 15:30
Program verificationCPP at Belvédère
Chair(s): Clement Pit-Claudel EPFL
14:00
22m
Talk
Certified Symbolic Finite Transducers: Formalization and Applications to String Analysis
CPP
Shuanglong Kan Barkhausen Institute, Dresden, Anthony Widjaja Lin TU Kaiserslautern; MPI-SWS
14:22
22m
Talk
Enhancing Symbolic Execution with Machine-Checked Safety Proofs
CPP
David Trabish Technion, Shachar Itzhaky Technion
Pre-print
14:45
22m
Talk
Layers of Confluence for Actors
CPP
Ludovic Henrio University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, Einar Broch Johnsen University of Oslo, Åsmund Aqissiaq Arild Kløvstad University of Oslo (UiO), Violet Ka I Pun Western Norway University of Applied Sciences, Yannick Zakowski Inria
15:07
22m
Talk
Towards composable proofs of cache coherence protocols
CPP