PLDI 2025
Mon 16 - Fri 20 June 2025 Seoul, South Korea

This program is tentative and subject to change.

Thu 19 Jun 2025 11:50 - 12:10 at Grand Ball Room 1 - Verification 1

We report the first formal verification of a lock-free list, skiplist, and a skiplist-based priority queue against a strong specification in relaxed memory consistency (RMC). RMC allows relaxed behaviors in which memory accesses may be reordered with other operations, posing two significant challenges for the verification of lock-free traversals. (1) <em>Specification challenge</em>: formulating a specification that is flexible enough to capture relaxed behaviors, yet simple enough to be easily understood and used. We address this challenge by proposing the <em>per-key linearizable history specification</em> that enforces a total order of operations for each key that respects causality, rather than a total order of all operations. (2) <em>Verification challenge</em>: devising verification techniques for reasoning about the reachability of edges for traversing threads, which can read stale edges due to relaxed behaviors. We address this challenge by introducing the <em>shadowed-by relation</em> that formalizes the notion of outdated edges. This relation enables us to establish a total order of edges and thus their associated operations for each key, required to satisfy the strong specification. All our proofs are mechanized on the iRC11 relaxed memory separation logic, built on the Iris framework in Rocq.

This program is tentative and subject to change.

Thu 19 Jun

Displayed time zone: Seoul change

10:30 - 12:10
10:30
20m
Talk
A Hybrid Approach to Semi-automated Rust Verification
PLDI Research Papers
Sacha-Élie Ayoun Imperial College London, Xavier Denis ETH Zurich, Petar Maksimović Nethermind; Imperial College London, Philippa Gardner Imperial College London
DOI Pre-print
10:50
20m
Talk
RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free Schedulers
PLDI Research Papers
Kimaya Bedarkar Max Planck Institute for Software Systems (MPI-SWS), Laila Elbeheiry MPI-SWS, Michael Sammler ETH Zurich; ISTA, Lennard Gäher MPI-SWS, Björn Brandenburg MPI-SWS, Derek Dreyer MPI-SWS, Deepak Garg MPI-SWS
DOI
11:10
20m
Talk
Certified Compilers à la Carte
PLDI Research Papers
Oghenevwogaga Ebresafe University of Waterloo, Ian Zhao University of Waterloo, Ende Jin University of Waterloo, Arthur Bright University of Waterloo, Charles Jian University of Waterloo, Yizhou Zhang University of Waterloo
DOI
11:30
20m
Talk
Destabilizing Iris
PLDI Research Papers
Simon Spies MPI-SWS, Niklas Mück MPI-SWS, Haoyi Zeng Saarland University, Michael Sammler ETH Zurich; ISTA, Andrea Lattuada MPI-SWS, Peter Müller ETH Zurich, Derek Dreyer MPI-SWS
DOI
11:50
20m
Talk
Verifying Lock-Free Traversals in Relaxed Memory Separation Logic
PLDI Research Papers
Sunho Park KAIST, Jaehwang Jung Rebellions Inc, Janggun Lee KAIST, Jeehoon Kang KAIST
DOI