PLDI 2025
Proceedings of the ACM on Programming Languages, Volume 9, Number PLDI

Title Page

Editorial Message

Sponsors

Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic
Jaehwang Jung, Sunho Park, Janggun Lee, Jeho Yeon, and Jeehoon Kang
(KAIST, Republic of Korea)

Article Search Artifacts Available

Leveraging Immutability to Validate Hazard Pointers for Optimistic Traversals
Janggun Lee, Jeonghyeon Kim, and Jeehoon Kang
(KAIST, Republic of Korea)

Article Search Artifacts Available

Verifying Lock-Free Traversals in Relaxed Memory Separation Logic
Sunho Park, Jaehwang Jung, Janggun Lee, and Jeehoon Kang
(KAIST, Republic of Korea)

Article Search Artifacts Available

RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free Schedulers
Kimaya Bedarkar, Laila Elbeheiry, Michael Sammler, Lennard Gäher, Björn Brandenburg, Derek Dreyer, and Deepak Garg
(MPI-SWS, Germany; ETH Zurich, Switzerland; ISTA, Austria)

Article Search

Nola: Later-Free Ghost State for Verifying Termination in Iris
Yusuke Matsushita and Takeshi Tsukada
(Kyoto University, Japan; Chiba University, Japan)

Article Search Artifacts Available

Random Variate Generation with Formal Guarantees
Feras A. Saad and Wonyeol Lee
(Carnegie Mellon University, USA; POSTECH, Republic of Korea)

Article Search Artifacts Available

Efficient Timestamping for Sampling-Based Race Detection
Minjian Zhang, Daniel Wee Soong Lim, Mosaad Al Thokair, Umang Mathur, and Mahesh Viswanathan
(University of Illinois at Urbana-Champaign, USA; National University of Singapore, Singapore; Saudi Aramco, Saudi Arabia)

Article Search Artifacts Available

Encoder-Decoder Quantum Circuit Optimization with SPARE
Ritvik Sharma and Sara Achour
(Stanford University, USA)

Article Search

Relaxing Alias Analysis: Exploring the Unexplored Space
Michel Weber, Theodoros Theodoridis, and Zhendong Su
(ETH Zurich, Switzerland)

Article Search Artifacts Available

Support Triangle Machine
Jiaying Li and Chunxue Hao
(OmniVision Technologies, Singapore; China CITIC Bank, China)

Article Search

Ripple: Asynchronous Programming for Spatial Dataflow Architectures
Souradip Ghosh, Yufei Shi, Brandon Lucia, and Nathan Beckmann
(Carnegie Mellon University, USA)

Article Search

StacKAT: Infinite State Network Verification
Jules Jacobs, Nate Foster, Tobias Kappé, Dexter Kozen, Lily Saada, Alexandra Silva, and Jana Wagemaker
(Cornell University, USA; Jane Street, USA; Leiden University, Netherlands; Radboud University Nijmegen, Netherlands)

Article Search

Circuit Optimization using Arithmetic Table Lookups
Raghav Malik, Vedant Paranjape, and Milind Kulkarni
(Purdue University, USA)

Preprint Artifacts Available

Partial Evaluation, Whole-Program Compilation
Chris Fallin and Maxwell Bernstein
(F5, USA; Recurse Center, USA)

Article Search

Exploiting Undefined Behavior in C/C++ Programs for Optimization: A Study on the Performance Impact
Lucian Popescu and Nuno P. Lopes
(INESC-ID, Portugal; Instituto Superior Técnico - University of Lisbon, Portugal)

Preprint

Certified Compilers à la Carte
Oghenevwogaga Ebresafe, Ian Zhao, Ende Jin, Arthur Bright, Charles Jian, and Yizhou Zhang
(University of Waterloo, Canada)

Article Search

Task-Based Tensor Computations on Modern GPUs
Rohan Yadav, Michael Garland, Alex Aiken, and Michael Bauer
(Stanford University, USA; NVIDIA, USA)

Article Search

Semantics of Integrating and Differentiating Singularities
Jesse Michel, Wonyeol Lee, and Hongseok Yang
(Massachusetts Institute of Technology, USA; POSTECH, Republic of Korea; KAIST, Republic of Korea)

Article Search Artifacts Available

Programming by Navigation
Justin Lubin, Parker Ziegler, and Sarah E. Chasins
(University of California at Berkeley, USA)

Article Search Artifacts Available

DR.FIX: Automatically Fixing Data Races at Industry Scale
Farnaz Behrang, Zhizhou Zhang, Georgian-Vlad Saioc, Peng Liu, and Milind Chabbi
(Uber Technologies, USA; Aarhus University, Denmark)

Article Search

Link-Time Optimization of Dynamic Casts in C++ Programs
Xufan Lu and Nuno P. Lopes
(INESC-ID, Portugal; Instituto Superior Técnico - University of Lisbon, Portugal)

Preprint

Robustifying Debug Information Updates in LLVM via Control-Flow Conformance Analysis
Shan Huang, Jingjing Liang, Ting Su, and Qirun Zhang
(East China Normal University, China; Georgia Institute of Technology, USA)

Article Search

A Uniform Framework for Handling Position Constraints in String Solving
Yu-Fang Chen, Vojtěch Havlena, Michal Hečko, Lukáš Holík, and Ondřej Lengál
(Academia Sinica, Taiwan; Brno University of Technology, Czech Republic; Aalborg University, Denmark)

Preprint Artifacts Available

MarQSim: Reconciling Determinism and Randomness in Compiler Optimization for Quantum Simulation
Xiuqi Cao, Junyu Zhou, Yuhao Liu, Yunong Shi, and Gushu Li
(University of Pennsylvania, USA; AWS Quantum Technologies, USA)

Article Search

Type-Aware Constraining for LLM Code Generation
Niels Mündler, Jingxuan He, Hao Wang, Koushik Sen, Dawn Song, and Martin Vechev
(ETH Zurich, Switzerland; University of California at Berkeley, USA)

Preprint Artifacts Available

Optimization-Directed Compiler Fuzzing for Continuous Translation Validation
Jaeseong Kwon, Bongjun Jang, Juneyoung Lee, and Kihong Heo
(KAIST, Republic of Korea; AWS, USA)

Article Search Info Artifacts Available

CompCertOC: Verified Compositional Compilation of Multi-threaded Programs with Shared Stacks
Ling Zhang, Yuting Wang, Yalun Liang, and Zhong Shao
(Shanghai Jiao Tong University, China; Yale University, USA)

Article Search

Dynamic Robustness Verification against Weak Memory
Roy Margalit, Michalis Kokologiannakis, Shachar Itzhaky, and Ori Lahav
(Tel Aviv University, Israel; ETH Zurich, Switzerland; Technion, Israel)

Article Search

Fast Direct Manipulation Programming with Patch-Reconciliation Correspondence
Parker Ziegler, Justin Lubin, and Sarah E. Chasins
(University of California at Berkeley, USA)

Article Search Info Artifacts Available

Solving Floating-Point Constraints with Continuous Optimization
Qian Chen, Chenqi Cui, Fengjuan Gao, Yu Wang, Ke Wang, and Linzhang Wang
(Nanjing University, China; Nanjing University of Science and Technology, China; Visa Research, USA)

Article Search

Webs and Flow-Directed Well-Typedness Preserving Program Transformations
Benjamin Quiring, David Van Horn, John Reppy, and Olin Shivers
(University of Maryland, USA; University of Chicago, USA; Northeastern University, USA)

Article Search

Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus
Steven Schaefer, Nathan Varner, Pedro Henrique Azevedo de Amorim, and Max S. New
(University of Michigan, USA; University of Oxford, UK)

Preprint Artifacts Available

Reductive Analysis with Compiler-Guided Large Language Models for Input-Centric Code Optimizations
Xiangwei Wang, Xinning Hui, Chunhua Liao, and Xipeng Shen
(North Carolina State University, USA; Lawrence Livermore National Laboratory, USA)

Article Search

Quantum Register Machine: Efficient Implementation of Quantum Recursive Programs
Zhicheng Zhang and Mingsheng Ying
(University of Technology Sydney, Australia)

Preprint

Destabilizing Iris
Simon Spies, Niklas Mück, Haoyi Zeng, Michael Sammler, Andrea Lattuada, Peter Müller, and Derek Dreyer
(MPI-SWS, Germany; Saarland University, Germany; ETH Zurich, Switzerland; ISTA, Austria)

Article Search Artifacts Available

Iso: Request-Private Garbage Collection
Tianle Qiu and Stephen M. Blackburn
(Australian National University, Australia; Google, Australia)

Article Search

Probabilistic Kleene Algebra with Angelic Nondeterminism
Shawn Ong, Stephanie Ma, and Dexter Kozen
(Cornell University, USA)

Article Search

Program Skeletons for Automated Program Translation
Bo Wang, Tianyu Li, Ruishi Li, Umang Mathur, and Prateek Saxena
(National University of Singapore, Singapore)

Preprint Info Artifacts Available

CRGC: Fault-Recovering Actor Garbage Collection in Pekko
Dan Plyukhin, Gul Agha, and Fabrizio Montesi
(University of Southern Denmark, USA; University of Illinois at Urbana-Champaign, USA; University of Southern Denmark, Denmark)

Article Search Artifacts Available

A Hybrid Approach to Semi-automated Rust Verification
Sacha-Élie Ayoun, Xavier Denis, Petar Maksimović, and Philippa Gardner
(Imperial College London, UK; ETH Zurich, Switzerland; Nethermind, UK)

Article Search Artifacts Available

QVM: Quantum Gate Virtualization Machine
Nathaniel Tornow, Emmanouil Giortamis, and Pramod Bhatotia
(TU Munich, Germany; LRZ, Germany)

Article Search Artifacts Available

Tree Borrows
Neven Villani, Johannes Hostert, Derek Dreyer, and Ralf Jung
(University of Grenoble Alpes - VERIMAG, France; ETH Zurich, Switzerland; MPI-SWS, Germany)

Article Search Artifacts Available

Lightweight and Locality-Aware Composition of Black Box Functions
Manya Bansal, Dillon Sharlet, Jonathan Ragan-Kelley, and Saman Amarasinghe
(Massachusetts Institute of Technology, USA; Google, USA)

Article Search

Efficient Formal Verification of Quantum Error Correcting Programs
Qifan Huang, Li Zhou, Wang Fang, Mengyu Zhao, and Mingsheng Ying
(Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; University of Edinburgh, UK; University of Technology Sydney, Australia)

Article Search Artifacts Available

Verified Foundations for Differential Privacy
Markus de Medeiros, Muhammad Naveed, Tancrède Lepoint, Temesghen Kahsai, Tristan Ravitch, Stefan Zetzsche, Anjali Joshi, Joseph Tassarotti, Aws Albarghouthi, and Jean-Baptiste Tristan
(New York University, USA; Amazon, USA; Amazon, UK)

Preprint Artifacts Available

Active Learning of Symbolic NetKAT Automata
Mark Moeller, Tiago Ferreira, Thomas Lu, Nate Foster, and Alexandra Silva
(Cornell University, USA; University College London, UK; Jane Street, USA)

Article Search

Efficient, Portable, Census-Polymorphic Choreographic Programming
Mako Bates, Shun Kashiwa, Syed Jafri, Gan Shen, Lindsey Kuper, and Joseph P. Near
(University of Vermont, USA; University of California at San Diego, USA; University of California at Santa Cruz, USA)

Article Search Artifacts Available

Taking out the Toxic Trash: Recovering Precision in Mixed Flow-Sensitive Static Analyses
Fabian Stemmler, Michael Schwarz, Julian Erhard, Sarah Tilscher, and Helmut Seidl
(TU Munich, Germany; LMU Munich, Germany)

Article Search Artifacts Available

Relational Abstractions Based on Labeled Union-Find
Dorian Lesbre, Matthieu Lemerre, Hichem Rami Ait-El-Hara, and François Bobot
(Université Paris-Saclay - CEA LIST, France; OCamlPro, France)

Article Search Artifacts Available

Functional Meaning for Parallel Streaming
Nick Rioux and Steve Zdancewic
(University of Pennsylvania, USA)

Preprint

Membership Testing for Semantic Regular Expressions
Yifei Huang, Matin Amini, Alexis Le Glaunec, Konstantinos Mamouras, and Mukund Raghothaman
(University of Southern California, USA; Rice University, USA)

Preprint Artifacts Available

MISAAL: Synthesis-Based Automatic Generation of Efficient and Retargetable Semantics-Driven Optimizations
Abdul Rafae Noor, Dhruv Baronia, Akash Kothari, Muchen Xu, Charith Mendis, and Vikram S. Adve
(University of Illinois at Urbana-Champaign, USA)

Article Search

An Interactive Debugger for Rust Trait Errors
Gavin Gray, Will Crichton, and Shriram Krishnamurthi
(Brown University, USA)

Article Search Artifacts Available

Polygon: Symbolic Reasoning for SQL using Conflict-Driven Under-Approximation Search
Pinhan Zhao, Yuepeng Wang, and Xinyu Wang
(University of Michigan, USA; Simon Fraser University, Canada)

Article Search Artifacts Available

Automated Exploit Generation for Node.js Packages
Filipe Marques, Mafalda Ferreira, André Nascimento, Miguel E. Coimbra, Nuno Santos, Limin Jia, and José Fragoso Santos
(INESC-ID, Portugal; Instituto Superior Técnico - University of Lisbon, Portugal; Carnegie Mellon University, USA)

Article Search Artifacts Available

Divergence-Aware Testing of Graphics Shader Compiler Back-Ends
Dongwei Xiao, Shuai Wang, Zhibo Liu, Yiteng Peng, Daoyuan Wu, and Zhendong Su
(Hong Kong University of Science and Technology, China; ETH Zurich, Switzerland)

Article Search

LiDO-DAG: A Framework for Verifying Safety and Liveness of DAG-Based Consensus Protocols
Longfei Qiu, Jingqi Xiao, Ji-Yong Shin, and Zhong Shao
(Yale University, USA; Northeastern University, USA)

Article Search Artifacts Available

Pointer Analysis for Database-Backed Applications
Yufei Liang, Teng Zhang, Ganlin Li, Tian Tan, Chang Xu, Chun Cao, Xiaoxing Ma, and Yue Li
(Nanjing University, China)

Article Search Artifacts Available

Principal Type Inference under a Prefix: A Fresh Look at Static Overloading
Daan Leijen and Wenjia Ye
(Microsoft Research, USA; National University of Singapore, Singapore; University of Hong Kong, China)

Article Search

First-Class Verification Dialects for MLIR
Mathieu Fehr, Yuyou Fan, Hugo Pompougnac, John Regehr, and Tobias Grosser
(University of Edinburgh, UK; University of Utah, USA; Inria, France; University of Cambridge, UK)

Article Search Artifacts Available

Robust Constant-Time Cryptography
Matthew Kolosick, Basavesh Ammanaghatta Shivakumar, Sunjay Cauligi, Marco Patrignani, Marco Vassena, Ranjit Jhala, and Deian Stefan
(University of California at San Diego, USA; Virginia Tech, USA; ICSI, Germany; University of Trento, Italy; Utrecht University, Netherlands)

Article Search

PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs
Gabriel Ebner, Guido Martínez, Aseem Rastogi, Thibault Dardinier, Megan Frisella, Tahina Ramananandro, and Nikhil Swamy
(Microsoft Research, USA; Microsoft Research, India; ETH Zurich, Switzerland; University of Washington, USA)

Article Search Artifacts Available

Synthesizing Optimal Object Selection Predicates for Image Editing using Lattices
Yang He, Xiaoyu Liu, and Yuepeng Wang
(Simon Fraser University, Canada)

Article Search Artifacts Available

Dynamic Region Ownership for Concurrency Safety
Fridtjof Peer Stoldt, Brandt Bucher, Sylvan Clebsch, Matthew A. Johnson, Matthew J. Parkinson, Guido van Rossum, Eric Snow, and Tobias Wrigstad
(Uppsala University, Sweden; Microsoft, USA; Microsoft Azure Research, UK)

Article Search Artifacts Available

Multi-stage Relational Programming
Michael Ballantyne, Rafaello Sanna, Jason Hemann, William E. Byrd, and Nada Amin
(Northeastern University, USA; Harvard University, USA; Seton Hall University, USA; University of Alabama at Birmingham, USA)

Article Search Artifacts Available

Scalable, Validated Code Translation of Entire Projects using Large Language Models
Hanliang Zhang, Cristina David, Meng Wang, Brandon Paulsen, and Daniel Kroening
(University of Bristol, UK; Amazon, USA)

Article Search Artifacts Available

Program Synthesis From Partial Traces
Margarida Ferreira, Victor Nicolet, Joey Dodds, and Daniel Kroening
(Carnegie Mellon University, USA; INESC-ID, Portugal; Instituto Superior Técnico - University of Lisbon, Portugal; Amazon, Canada; Amazon, USA)

Article Search Artifacts Available

Probabilistic Refinement Session Types
Qiancheng Fu, Ankush Das, and Marco Gaboardi
(Boston University, USA)

Article Search Info Artifacts Available

Smooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs and Compilers
Owen Conoly, Andres Erbsen, and Adam Chlipala
(Massachusetts Institute of Technology, USA; Google, USA)

Article Search Artifacts Available

Graphiti: Bridging Graph and Relational Database Queries
Yang He, Ruijie Fang, Işıl Dillig, and Yuepeng Wang
(Simon Fraser University, Canada; University of Texas at Austin, USA)

Article Search Artifacts Available

Verifying Solutions to Semantics-Guided Synthesis Problems
Charlie Murphy, Keith J.C. Johnson, Thomas Reps, and Loris D'Antoni
(University of Wisconsin-Madison, USA; University of California at San Diego, USA)

Article Search

Handling the Selection Monad
Gordon Plotkin and Ningning Xie
(Google DeepMind, USA)

Article Search

Spineless Traversal for Layout Invalidation
Marisa Kirisame, Tiezhi Wang, and Pavel Panchekha
(University of Utah, USA; Tongji University, China)

Article Search

Exact Loop Bound Analysis
Daniel Riley and Grigory Fedyukovich
(Florida State University, USA)

Article Search

Bean: A Language for Backward Error Analysis
Ariel E. Kellison, Laura Zielinski, David Bindel, and Justin Hsu
(Cornell University, USA)

Article Search Artifacts Available

Stochastic Lazy Knowledge Compilation for Inference in Discrete Probabilistic Programs
Maddy Bowers, Alexander K. Lew, Joshua B. Tenenbaum, Armando Solar-Lezama, and Vikash K. Mansinghka
(Massachusetts Institute of Technology, USA; Yale University, USA)

Article Search Artifacts Available

Slotted E-Graphs: First-Class Support for (Bound) Variables in E-Graphs
Rudi Schneider, Marcus Rossel, Amir Shaikhha, Andrés Goens, Thomas Kœhler, and Michel Steuwer
(Technische Universität Berlin, Germany; Barkhausen Institut, Germany; University of Edinburgh, UK; University of Amsterdam, Netherlands; CNRS - ICube Lab, France)

Preprint

Usability Barriers for Liquid Types
Catarina Gamboa, Abigail Reese, Alcides Fonseca, and Jonathan Aldrich
(Carnegie Mellon University, USA; University of Lisbon, Portugal)

Preprint Artifacts Available

Efficient Linearizability Monitoring
Parosh Aziz Abdulla, Samuel Grahn, Bengt Jonsson, Shankaranarayanan Krishna, and Om Swostik Mishra
(Uppsala University, Sweden; Mälardalen University, Sweden; IIT Bombay, India)

Article Search Artifacts Available

Morello-Cerise: A Proof of Strong Encapsulation for the Arm Morello Capability Hardware Architecture
Angus Hammond, Ricardo Almeida, Thomas Bauereiss, Brian Campbell, Ian Stark, and Peter Sewell
(University of Cambridge, UK; University of Glasgow, UK; University of Edinburgh, UK)

Article Search Artifacts Available

Guided Tensor Lifting
Yixuan Li, José Wesley de Souza Magalhães, Alexander Brauckmann, Michael F. P. O'Boyle, and Elizabeth Polgreen
(University of Edinburgh, UK)

Article Search

Making Concurrent Hardware Verification Sequential
Thomas Bourgeat, Jiazheng Liu, Adam Chlipala, and Arvind
(EPFL, Switzerland; Massachusetts Institute of Technology, USA)

Article Search

Correctly Rounded Math Libraries without Worrying about the Application’s Rounding Mode
Sehyeok Park, Justin Kim, and Santosh Nagarakatte
(Rutgers University, USA)

Article Search

Thrust: A Prophecy-Based Refinement Type System for Rust
Hiromi Ogawa, Taro Sekiyama, and Hiroshi Unno
(University of Tsukuba, Japan; National Institute of Informatics, Japan; Tohoku University, Japan)

Article Search

Roulette: A Language for Expressive, Exact, and Efficient Discrete Probabilistic Programming
Cameron Moy, Jack Czenszak, John M. Li, Brianna Marshall, and Steven Holtzen
(Northeastern University, USA)

Article Search Artifacts Available

Modular Construction and Optimization of the UZP Sparse Format for SpMV on CPUs
Alonso Rodriguez-Iglesias, Santoshkumar T. Tongli, Emily Tucker, Louis-Noël Pouchet, Gabriel Rodríguez, and Juan Tourino
(Universidade da Coruña, Spain; Colorado State University, USA)

Article Search Artifacts Available

A Concurrent Approach to String Transformation Synthesis
Yuantian Ding and Xiaokang Qiu
(Purdue University, USA)

Article Search Info Artifacts Available

RRR-SMR: Reduce, Reuse, Recycle: Better Methods for Practical Lock-Free Data Structures
Md Amit Hasan Arovi and Ruslan Nikolaev
(Pennsylvania State University, USA)

Article Search Info Artifacts Available

Practical Type Inference with Levels
Andong Fan, Han Xu, and Ningning Xie
(University of Toronto, Canada; Princeton University, USA)

Article Search

AWDIT: An Optimal Weak Database Isolation Tester
Lasse Møldrup and Andreas Pavlogiannis
(Aarhus University, Denmark)

Preprint Artifacts Available