Venues / PLDI /

PLDI 2025

89 papers

A Concurrent Approach to String Transformation Synthesis · Yuantian Ding, Xiaokang Qiu
A Hybrid Approach to Semi-automated Rust Verification · Sacha-Élie Ayoun, Xavier Denis, Petar Maksimovic, Philippa Gardner
A Uniform Framework for Handling Position Constraints in String Solving · Yu-Fang Chen, Vojtech Havlena, Michal Hecko, Lukás Holík, Ondrej Lengál
AWDIT: An Optimal Weak Database Isolation Tester · Lasse Møldrup, Andreas Pavlogiannis
Active Learning of Symbolic NetKAT Automata · Mark Moeller, Tiago Ferreira, Thomas Lu, Nate Foster, Alexandra Silva
An Interactive Debugger for Rust Trait Errors · Gavin Gray, Will Crichton, Shriram Krishnamurthi
Automated Exploit Generation for Node.js Packages · Filipe Marques, Mafalda Ferreira, André Nascimento, Miguel E. Coimbra, Nuno Santos, Limin Jia + 1 more
Bean: A Language for Backward Error Analysis · Ariel E. Kellison, Laura Zielinski, David Bindel, Justin Hsu
CRGC: Fault-Recovering Actor Garbage Collection in Pekko · Dan Plyukhin, Gul Agha, Fabrizio Montesi
Certified Compilers à la Carte · Oghenevwogaga Ebresafe, Ian Zhao, Ende Jin, Arthur Bright, Charles Jian, Yizhou Zhang
Circuit Optimization using Arithmetic Table Lookups · Raghav Malik, Vedant Paranjape, Milind Kulkarni
CompCertOC: Verified Compositional Compilation of Multi-threaded Programs with Shared Stacks · Ling Zhang, Yuting Wang, Yalun Liang, Zhong Shao
Correctly Rounded Math Libraries without Worrying about the Application's Rounding Mode · Sehyeok Park, Justin Kim, Santosh Nagarakatte
DR.FIX: Automatically Fixing Data Races at Industry Scale · Farnaz Behrang, Zhizhou Zhang, Georgian-Vlad Saioc, Peng Liu, Milind Chabbi
Destabilizing Iris · Simon Spies, Niklas Mück, Haoyi Zeng, Michael Sammler, Andrea Lattuada, Peter Müller + 1 more
Divergence-Aware Testing of Graphics Shader Compiler Back-Ends · Dongwei Xiao, Shuai Wang, Zhibo Liu, Yiteng Peng, Daoyuan Wu, Zhendong Su
Dynamic Region Ownership for Concurrency Safety · Fridtjof Peer Stoldt, Gary Brandt Bucher II, Sylvan Clebsch, Matthew A. Johnson, Matthew J. Parkinson, Guido van Rossum + 2 more
Dynamic Robustness Verification against Weak Memory · Roy David Margalit, Michalis Kokologiannakis, Shachar Itzhaky, Ori Lahav
Efficient Formal Verification of Quantum Error Correcting Programs · Qifan Huang, Li Zhou, Wang Fang, Mengyu Zhao, Mingsheng Ying
Efficient Linearizability Monitoring · Parosh Aziz Abdulla, Samuel Grahn, Bengt Jonsson, Shankaranarayanan Krishna, Om Swostik Mishra
Efficient Timestamping for Sampling-Based Race Detection · Minjian Zhang, Daniel Wee Soong Lim, Mosaad Al Thokair, Umang Mathur, Mahesh Viswanathan
Efficient, Portable, Census-Polymorphic Choreographic Programming · Mako Bates, Shun Kashiwa, Syed Jafri, Gan Shen, Lindsey Kuper, Joseph P. Near
Exact Loop Bound Analysis · Daniel Riley, Grigory Fedyukovich
Exploiting Undefined Behavior in C/C++ Programs for Optimization: A Study on the Performance Impact · Lucian Popescu, Nuno P. Lopes
Fast Direct Manipulation Programming with Patch-Reconciliation Correspondence · Parker Ziegler, Justin Lubin, Sarah E. Chasins
First-Class Verification Dialects for MLIR · Mathieu Fehr, Yuyou Fan, Hugo Pompougnac, John Regehr, Tobias Grosser
Functional Meaning for Parallel Streaming · Nick Rioux, Steve Zdancewic
Graphiti: Bridging Graph and Relational Database Queries · Yang He, Ruijie Fang, Isil Dillig, Yuepeng Wang
Guided Tensor Lifting · Yixuan Li, José Wesley de Souza Magalhães, Alexander Brauckmann, Michael F. P. O'Boyle, Elizabeth Polgreen
Handling the Selection Monad · Gordon D. Plotkin, Ningning Xie
Intrinsic Verification of Parsers and Formal Grammar Theory in Dependent Lambek Calculus · Steven Schaefer, Nathan Varner, Pedro Henrique Azevedo de Amorim, Max S. New
Iso: Request-Private Garbage Collection · Tianle Qiu, Stephen M. Blackburn
Leveraging Immutability to Validate Hazard Pointers for Optimistic Traversals · Janggun Lee, Jeonghyeon Kim, Jeehoon Kang
LiDO-DAG: A Framework for Verifying Safety and Liveness of DAG-Based Consensus Protocols · Longfei Qiu, Jingqi Xiao, Ji-Yong Shin, Zhong Shao
Lightweight and Locality-Aware Composition of Black-Box Subroutines · Manya Bansal, Dillon Sharlet, Jonathan Ragan-Kelley, Saman P. Amarasinghe
Link-Time Optimization of Dynamic Casts in C++ Programs · Xufan Lu, Nuno P. Lopes
MISAAL: Synthesis-Based Automatic Generation of Efficient and Retargetable Semantics-Driven Optimizations · Abdul Rafae Noor, Dhruv Baronia, Akash Kothari, Muchen Xu, Charith Mendis, Vikram S. Adve
Making Concurrent Hardware Verification Sequential · Thomas Bourgeat, Jiazheng Liu, Adam Chlipala, Arvind
MarQSim: Reconciling Determinism and Randomness in Compiler Optimization for Quantum Simulation · Xiuqi Cao, Junyu Zhou, Yuhao Liu, Yunong Shi, Gushu Li
Membership Testing for Semantic Regular Expressions · Yifei Huang, Matin Amini, Alexis Le Glaunec, Konstantinos Mamouras, Mukund Raghothaman
Modular Construction and Optimization of the UZP Sparse Format for SpMV on CPUs · Alonso Rodríguez-Iglesias, Santoshkumar T. Tongli, Emily Tucker, Louis-Noël Pouchet, Gabriel Rodríguez, Juan Touriño
Morello-Cerise: A Proof of Strong Encapsulation for the Arm Morello Capability Hardware Architecture · Angus Hammond, Ricardo Almeida, Thomas Bauereiss, Brian Campbell, Ian Stark, Peter Sewell
Multi-stage Relational Programming · Michael Ballantyne, Rafaello Sanna, Jason Hemann, William E. Byrd, Nada Amin
Nola: Later-Free Ghost State for Verifying Termination in Iris · Yusuke Matsushita, Takeshi Tsukada
Optimization-Directed Compiler Fuzzing for Continuous Translation Validation · Jaeseong Kwon, Bongjun Jang, Juneyoung Lee, Kihong Heo
Optimizing Ancilla-Based Quantum Circuits with SPARE · Ritvik Sharma, Sara Achour
Partial Evaluation, Whole-Program Compilation · Chris Fallin, Maxwell Bernstein
Pointer Analysis for Database-Backed Applications · Yufei Liang, Teng Zhang, Ganlin Li, Tian Tan, Chang Xu, Chun Cao + 2 more
Polygon: Symbolic Reasoning for SQL using Conflict-Driven Under-Approximation Search · Pinhan Zhao, Yuepeng Wang, Xinyu Wang
Practical Type Inference with Levels · Andong Fan, Han Xu, Ningning Xie
Principal Type Inference under a Prefix: A Fresh Look at Static Overloading · Daan Leijen, Wenjia Ye
Probabilistic Kleene Algebra with Angelic Nondeterminism · Shawn Ong, Stephanie Ma, Dexter Kozen
Probabilistic Refinement Session Types · Qiancheng Fu, Ankush Das, Marco Gaboardi
Program Skeletons for Automated Program Translation · Bo Wang, Tianyu Li, Ruishi Li, Umang Mathur, Prateek Saxena
Program Synthesis from Partial Traces · Margarida Ferreira, Victor Nicolet, Joey Dodds, Daniel Kroening
Programming by Navigation · Justin Lubin, Parker Ziegler, Sarah E. Chasins
PulseCore: An Impredicative Concurrent Separation Logic for Dependently Typed Programs · Gabriel Ebner, Guido Martínez, Aseem Rastogi, Thibault Dardinier, Megan Frisella, Tahina Ramananandro + 1 more
QVM: Quantum Gate Virtualization Machine · Nathaniel Tornow, Emmanouil Giortamis, Pramod Bhatotia
Quantum Register Machine: Efficient Implementation of Quantum Recursive Programs · Zhicheng Zhang, Mingsheng Ying
RRR-SMR: Reduce, Reuse, Recycle: Better Methods for Practical Lock-Free Data Structures · Md Amit Hasan Arovi, Ruslan Nikolaev
Random Variate Generation with Formal Guarantees · Feras A. Saad, Wonyeol Lee
Reductive Analysis with Compiler-Guided Large Language Models for Input-Centric Code Optimizations · Xiangwei Wang, Xinning Hui, Chunhua Liao, Xipeng Shen
RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free Schedulers · Kimaya Bedarkar, Laila Elbeheiry, Michael Sammler, Lennard Gäher, Björn B. Brandenburg, Derek Dreyer + 1 more
Relational Abstractions Based on Labeled Union-Find · Dorian Lesbre, Matthieu Lemerre, Hichem Rami Ait El Hara, François Bobot
Relaxing Alias Analysis: Exploring the Unexplored Space · Michel Weber, Theodoros Theodoridis, Zhendong Su
Ripple: Asynchronous Programming for Spatial Dataflow Architectures · Souradip Ghosh, Yufei Shi, Brandon Lucia, Nathan Beckmann
Robust Constant-Time Cryptography · Matthew Kolosick, Basavesh Ammanaghatta Shivakumar, Sunjay Cauligi, Marco Patrignani, Marco Vassena, Ranjit Jhala + 1 more
Robustifying Debug Information Updates in LLVM via Control-Flow Conformance Analysis · Shan Huang, Jingjing Liang, Ting Su, Qirun Zhang
Roulette: A Language for Expressive, Exact, and Efficient Discrete Probabilistic Programming · Cameron Moy, Jack Czenszak, John M. Li, Brianna Marshall, Steven Holtzen
Scalable, Validated Code Translation of Entire Projects using Large Language Models · Hanliang Zhang, Cristina David, Meng Wang, Brandon Paulsen, Daniel Kroening
Semantics of Integrating and Differentiating Singularities · Jesse Michel, Wonyeol Lee, Hongseok Yang
Slotted E-Graphs: First-Class Support for (Bound) Variables in E-Graphs · Rudi Schneider, Marcus Rossel, Amir Shaikhha, Andrés Goens, Thomas Koehler, Michel Steuwer
Smooth, Integrated Proofs of Cryptographic Constant Time for Nondeterministic Programs and Compilers · Owen Conoly, Andres Erbsen, Adam Chlipala
Solving Floating-Point Constraints with Continuous Optimization · Qian Chen, Chenqi Cui, Fengjuan Gao, Yu Wang, Ke Wang, Linzhang Wang
Spineless Traversal for Layout Invalidation · Marisa Kirisame, Tiezhi Wang, Pavel Panchekha
StacKAT: Infinite State Network Verification · Jules Jacobs, Nate Foster, Tobias Kappé, Dexter Kozen, Lily Saada, Alexandra Silva + 1 more
Stochastic Lazy Knowledge Compilation for Inference in Discrete Probabilistic Programs · Maddy Bowers, Alexander K. Lew, Joshua B. Tenenbaum, Armando Solar-Lezama, Vikash K. Mansinghka
Support Triangle Machine · Jiaying Li, Chunxue Hao
Taking Out the Toxic Trash: Recovering Precision in Mixed Flow-Sensitive Static Analyses · Fabian Stemmler, Michael Schwarz, Julian Erhard, Sarah Tilscher, Helmut Seidl
Task-Based Tensor Computations on Modern GPUs · Rohan Yadav, Michael Garland, Alex Aiken, Michael Bauer
Thrust: A Prophecy-Based Refinement Type System for Rust · Hiromi Ogawa, Taro Sekiyama, Hiroshi Unno
Tree Borrows · Neven Villani, Johannes Hostert, Derek Dreyer, Ralf Jung
Type-Constrained Code Generation with Language Models · Niels Mündler, Jingxuan He, Hao Wang, Koushik Sen, Dawn Song, Martin T. Vechev
Usability Barriers for Liquid Types · Catarina Gamboa, Abigail Reese, Alcides Fonseca, Jonathan Aldrich
Verified Foundations for Differential Privacy · Markus de Medeiros, Muhammad Naveed, Tancrède Lepoint, Temesghen Kahsai, Tristan Ravitch, Stefan Zetzsche + 4 more
Verifying General-Purpose RCU for Reclamation in Relaxed Memory Separation Logic · Jaehwang Jung, Sunho Park, Janggun Lee, Jeho Yeon, Jeehoon Kang
Verifying Lock-Free Traversals in Relaxed Memory Separation Logic · Sunho Park, Jaehwang Jung, Janggun Lee, Jeehoon Kang
Verifying Solutions to Semantics-Guided Synthesis Problems · Charlie Murphy, Keith J. C. Johnson, Thomas Reps, Loris D'Antoni
Webs and Flow-Directed Well-Typedness Preserving Program Transformations · Benjamin Quiring, David Van Horn, John H. Reppy, Olin Shivers