PLDI 2026

108 papers

1. &inator: Correct, Precise C-to-Rust Interface Translation · Victor Chen, Ayden Coughlin, Michael D. Bond
2. A Categorical Basis for Robust Program Analysis · Zachary Kincaid, Shaowei Zhu
3. A Compiler for Fused Relational Operations on Multisets · James Dong, Fredrik Kjolstad
4. A Deductive System for Contract Satisfaction Proofs · Arthur Correnson, Haoyi Zeng, Jana Hofmann
5. A Formally Verified Foundation for Compositional Heterogeneous Coherence · An Qi Zhang, Andrés Goens, Daniel J. Sorin, Vijay Nagarajan
6. A Hierarchy of Supermartingales for ω-Regular Verification · Satoshi Kura, Hiroshi Unno
7. A Mechanized Algebra of Verified Data Structures for Optimizing Sparse Tensor Programs · Amanda Liu, Gilbert Louis Bernstein, Shoaib Kamil, Adam Chlipala, Jonathan Ragan-Kelley
8. A Verified Parallel Scheduler for OCaml 5 · Clément Allain, Gabriel Scherer
9. Abstract Interpretation with Confidence: Quantifying the Precision of Dataflow Analysis with Probabilities · Yuanfeng Shi, Ziyue Jin, Xin Zhang
10. An Efficient Algorithm for Streaming BPE Tokenization · Konstantinos Mamouras, Angela W. Li, Yudi Yang
11. Analyzing Bytes: Pre-Disassembly Static Binary Analysis · Huan Nguyen, Soumyakant Priyadarshan, Chencheng Jiang, R. Sekar
12. Backwards-Compatible Row-Based Exceptions in ML · Simcha van Collem, Paulo Emílio de Vilhena, Robbert Krebbers
13. Bonsai: Compiling Queries to Pruned Tree Traversals · Alexander J. Root, Christophe Gyurgyik, Purvi Goel, Kayvon Fatahalian, Jonathan Ragan-Kelley, Andrew Adams + 1 more
14. Bridging Coverage and Confidence: Reliable Static False Alarm Elimination via Input-Agnosticity · Jiayi Wang, Yu Wang, Linzhang Wang, Ke Wang
15. CRIS: The Power of Imagination in Hybrid Verification · Yonghee Kim, Taeyoung Yoon, Sanghyun Yi, Jaehyung Lee, Soonwon Moon, Yeji Han + 6 more
16. Categorical Semantics of Probabilistic Symbolic Execution · John M. Li, Jack Czenszak, Steven Holtzen
17. Causality and Semantic Separation · Anna Zhang, Qinglan Luo, London Bielicke, Eunice Jun, Adam Chlipala
18. Cerisier: A Program Logic for Attestation in a Capability Machine · June Rousseau, Denis Carnier, Thomas Van Strydonck, Steven Keuchel, Dominique Devriese, Lars Birkedal
19. Choose, Don't Label: Multiple-Choice Query Synthesis for Program Disambiguation · Celeste Barnaby, Danny Ding, Osbert Bastani, Isil Dillig
20. CoTenN: Constrained Optimization with Tensor Networks · Ritvik Sharma, Cheng Peng, Siddharth Dangwal, Sara Achour
21. Cobble: Compiling Block Encodings for Quantum Computational Linear Algebra · Charles Yuan
22. Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows · Zain K. Aamer, Rini Banerjee, Hiroyuki Katsura, David Kaloper-Mersinjak, Dimitrios J. Economou, Kayvan Memarian + 5 more
23. Compiling Strassen-like Matrix Multiplication Algorithms to Fast CUDA Kernels · Abhinav Jangda
24. Compiling to Recurrent Neurons · Joey Velez-Ginorio, Nada Amin, Konrad P. Kording, Steve Zdancewic
25. Contextual Embeddings: Implementing Bound Variables through Instance Resolution · Samantha Frohlich, Jessica Foster, G. A. Kavvos, Meng Wang
26. Contextual Refinement of Higher-Order Concurrent Probabilistic Programs · Kwing Hei Li, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal
27. Corrigendum: Falcon: A Scalable Analytical Cache Model · Arjun Pitchanathan, Kunwar Grover, Tobias Grosser
28. Cpp2Rust: Automatic Translation of C++ to Safe Rust · Lucian Popescu, Francisco Gouveia, Henrique Preto, João Silveira, Dmytro Hrybenko, José Fragoso Santos + 1 more
29. Decoupling Data Layouts from Bounding Volume Hierarchies · Christophe Gyurgyik, Alexander J. Root, Fredrik Kjolstad
30. Diagramming Program Values by Spatial Refinement · Siddhartha Prasad, Michael Tu, Karan Kashyap, Tim Nelson, Shriram Krishnamurthi
31. Dynamically Checked Deep Immutability in Python · Fridtjof Peer Stoldt, Sylvan Clebsch, Matthew A. Johnson, Matthew J. Parkinson, Tobias Wrigstad
32. EREQ: Regular Expressions with Quantifiers and Incremental Quantifier Elimination · Ekaterina Zhuchko, Ian Erik Varatalu, Margus Veanes, Nikolaj S. Bjørner
33. Editorial Message · Manu Sridharan
34. Enumerating Ill-Typed Programs for Testing Type Analyzers · Thodoris Sotiropoulos, Zhendong Su
35. Equality Saturation for Quantum Circuit Optimization · Ganxiang Yang, Paige Raun, Runzhou Tao, Ronghui Gu
36. Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for Reachability Types · Songlin Jia, Guannan Wei, Siyuan He, Yuyan Bao, Tiark Rompf
37. Evolving Abstract Transformers for Gradient-Guided, Adaptable Abstract Interpretation · Shaurya Gomber, Debangshu Banerjee, Gagandeep Singh
38. Expecto: Extracting Formal Specifications from Natural Language Description for Trustworthy Oracles · Dongjae Lee, Kihong Heo
39. Exploiting Sophisticated Static Analysis for Verilog · Qinlin Chen, Nairen Zhang, Jinpeng Wang, Jiacai Cui, Tian Tan, Xiaoxing Ma + 3 more
40. Fast Atomicity Monitoring · Hünkar Can Tunç, Yifan Dong, Andreas Pavlogiannis
41. Fixed Parameter Tractable Linearizability Monitoring · Lee Zheng Han, Umang Mathur
42. FlexHeap: Dynamic I/O-Aware Heap Resizing for Managed Applications · Iacovos G. Kolokasis, Shoaib Akram, Foivos S. Zakkak, Polyvios Pratikakis, Angelos Bilas
43. Flow-Analysis-Based Closure Optimization · John H. Reppy, Olin Shivers, Byron Zhong
44. Fungible Memories for Automated Technology Mapping and Retargeting · Zachary D. Sisco, Sijie Kong, Daniel Ruelas-Petrisko, Jingtao Xia, Julian Springer, Varun Rao + 4 more
45. GradInf: Gradient Estimation as Probabilistic Inference · Gaurav Arya, Mathieu Huot, Moritz Schauer, Alexander K. Lew, Feras A. Saad
46. Hayroll: A Modular Wrapper for Translating C Macros and Conditional Compilation to Rust · Haoran Peng, Baris Kasikci, Gilbert Louis Bernstein, Michael D. Ernst
47. Heterogeneous Dynamic Logic: Provability Modulo Program Theories · Samuel Teuber, Mattias Ulbrich, André Platzer, Bernhard Beckert
48. Hybrid Path-Sums for Hybrid Quantum Programs · Christophe Chareton, Jad Issa, Mathieu Nguyen, Nicolas Blanco, Sébastien Bardin
49. Hyper Separation Logic · Trayan Gospodinov, Peter Müller, Thibault Dardinier
50. Implementability of Global Distributed Protocols Modulo Network Architectures · Elaine Li, Thomas Wies
51. Improving Equality Saturation for EDA via Semantic E-Graphs · Sijie Kong, Jingtao Xia, Daniel Ruelas-Petrisko, Zachary D. Sisco, Jonathan Balkind, Gus Henry Smith
52. Incremental Computation for Efficient Programmable Inference in Probabilistic Programs · Fabian Zaiser, Jack Czenszak, Martin C. Rinard, Vikash K. Mansinghka, Alexander K. Lew
53. Intrinsically Correct Algorithms and Recursive Coalgebras · Cass Alexandru, Henning Urbat, Thorsten Wißmann
54. Iris-WasmFX: Modular Reasoning for Wasm Stack Switching · Maxime Legoupil, Mathias Pedersen, Lars Birkedal, Sam Lindley, Jean Pichon-Pharabod
55. Kuiper: Correct and Efficient GPU Programming with Dependent Types and Separation Logic · Guido Martínez, Bastian Köpcke, Jonás Fiala, Gabriel Ebner, Tahina Ramananandro, Michel Steuwer + 2 more
56. Let It Flow: A Formally Verified Compilation Framework for Asynchronous Dataflow · Zhengyao Lin, Yi Cai, Milijana Surbatovich
57. MatchBox: A Semantic Foundation for Data Plane Portability · Eric Hayden Campbell, Robert Zhang, Divyanshu Saxena, Aditya Akella, Isil Dillig
58. Modular GPU Programming with Typed Perspectives · Manya Bansal, Daniel Sainati, Joseph W. Cutler, Saman P. Amarasinghe, Jonathan Ragan-Kelley
59. Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic · Philipp G. Haselwarter, Alejandro Aguirre, Simon Oddershede Gregersen, Kwing Hei Li, Joseph Tassarotti, Lars Birkedal
60. NEURA: A Unified and Retargetable Compilation Framework for Coarse-Grained Reconfigurable Architectures · Shangkun Li, Jinming Ge, Diyuan Tao, Zeyu Li, Jiawei Liang, Linfeng Du + 3 more
61. Navigating AND-OR Graph Modifications to Debug Failing Proof Search · Justin Lubin, Marlena Preigh, Max Willsey, Sarah E. Chasins
62. Neptune: Advanced ML Operator Fusion for Locality and Parallelism on GPUs · Yifan Zhao, Egan Johnson, Prasanth Chatarasi, Vikram S. Adve, Sasa Misailovic
63. Nested Inductive Types: Justified and Usable Nested Inductive Types in Lean and Rocq · Thomas Lamiaux, Yannick Forster, Matthieu Sozeau, Nicolas Tabareau
64. Neuro-symbolic Hierarchical Learning for Long-Horizon Robotic Tasks · Yu Huang, Ziji Wu, Zhengyi Ma, Kexin Ma, Ji Wang
65. Optimal Predicate Pushdown Synthesis · Robert Zhang, Eric Hayden Campbell, Dixin Tang, Isil Dillig
66. Optimism in Equality Saturation · Russel Arbore, Alvin Cheung, Max Willsey
67. Pantomime: Constructive Leakage Proofs via Simulation · Robin Webbers, Robert Schenck, Wind Wong, Kristina Sojakova, Klaus von Gleissenthall
68. Parameterized Algorithms and Complexity for Function Merging with Branch Reordering · Amir Kafshdar Goharshady, Kerim Kochekov, Tian Shu, Ahmed Khaled Zaher
69. Path-Sensitive Abstract Interpretation for WCET Estimation · Shangshang Xiao, Mengxia Sun, Wei Zhang, Naijun Zhan, Lei Ju
70. Persistent Iterators with Value Semantics · Yihe Li, Gregory J. Duck
71. Presynthesis: Towards Scaling Up Program Synthesis with Finer-Grained Abstract Semantics · Rui Dong, Qingyue Wu, Danny Ding, Zheng Guo, Ruyi Ji, Xinyu Wang
72. Pure Borrow: Linear Haskell Meets Rust-Style Borrowing · Yusuke Matsushita, Hiromi Ishii
73. Redundant Array Computation Elimination · Zixuan Wang, Liang Yuan, Xianmeng Jiang, Kun Li, Junmin Xiao, Yunquan Zhang
74. Responsive Parallelism with Dynamic and First-Class Priorities · Marelle León, My Dinh, Stefan K. Muller
75. Restart and Refine: Scalable IFDS Taint Analysis across Memory Budgets · Yujiang Gui, Yonggang Tao, Jingling Xue
76. Revisiting Partial Tracing for Safe, Efficient, and Concurrent Garbage Collection in Unmanaged Languages · Jeonghyeon Kim, Jongse Park, Youngjin Kwon, Jeehoon Kang
77. SAIL: Sound Abstract Interpreters with LLMs · Qiuhan Gu, Avaljot Singh, Gagandeep Singh
78. SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits · Nengkun Yu, Jens Palsberg, Thomas Reps
79. SIMT-Step Execution: A Flexible Operational Semantics for GPU Subgroup Behavior · Zheyuan Chen, Naomi Rehman, Guido Martínez, Tyler Sorensen
80. SSA without Dominance for Higher-Order Programs · Roland Leißa, Johannes Griebler
81. Scalable Floating-Point Satisfiability via Staged Optimization · Yuanzhuo Zhang, Zhoulai Fu, Binoy Ravindran
82. Semantic Reification: A New Paradigm for Random Program Generation · Kavya Chopra, Cong Li, Thodoris Sotiropoulos, Zhendong Su
83. Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy · Eden Frenkel, Kenneth L. McMillan, Oded Padon, Sharon Shoham
84. Solvable Tuple Patterns and Their Applications to Program Verification · Naoki Kobayashi, Ryosuke Sato, Ayumi Shinohara, Ryo Yoshinaka
85. Soteria: Efficient Symbolic Execution as a Functional Library: Perhaps You Should Write Your Own Symbolic Execution Engine! · Sacha-Élie Ayoun, Opale Sjöstedt, Azalea Raad
86. SparseZETA: Intelligent Auto-tuner for Designing High-Performance SpMV Programs · Zhen Du, Ying Liu, Xionghui Chen, Yanbo Zhao, Xiaobing Feng, Huimin Cui + 1 more
87. State Space Estimation for DPOR-Based Model Checkers · A. R. Balasubramanian, Mohammad Hossein Khoshechin Jorshari, Rupak Majumdar, Umang Mathur, Minjian Zhang
88. SuperCollider: Scalable and Effective Data Race Detection for CUDA · Mark Stephenson, Sana Damani, Mohamed Tarek Ibn Ziad, Anis Ladram, Michael Garland
89. SuperDP: Differential Privacy Refutation via Supermartingales · Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Dorde Zikelic
90. Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification · Satoshi Kura, Hiroshi Unno, Takeshi Tsukada
91. SureDistrib: Verifying Almost-Sure Termination of Composite Asynchronous Byzantine Protocols · Longfei Qiu, Jingqi Xiao, Ji-Yong Shin, Zhong Shao
92. Syntactic Implicit Parameters with Static Overloading · Daan Leijen, Tim Whiting
93. Synthesizing Backward Error Bounds, Backward · Laura Zielinski, Justin Hsu
94. The Downgrading Semantics of Memory Safety · René Rydhof Hansen, Andreas Stenbæk Larsen, Aslan Askarov
95. The Search for Constrained Random Generators · Harrison Goldstein, Hila Peleg, Cassia Torczon, Daniel Sainati, Leonidas Lampropoulos, Benjamin C. Pierce
96. Towards Efficient Matching of Regexes with Backreferences using Register Set Automata · Vojtech Havlena, Lukás Holík, Ondrej Lengál, Jan Vasák, Sabína Gulcíková
97. Towards Removing Undef Values from LLVM IR · Pedro Lobo, John McIver, George Mitenkov, Juneyoung Lee, Kirshanthan Sundararajah, Nuno P. Lopes
98. Trace-Guided Synthesis of Effectful Test Generators · Zhe Zhou, Ankush Desai, Benjamin Delaware, Suresh Jagannathan
99. TreeCoder: Systematic Exploration and Optimisation of Decoding and Constraints for LLM Code Generation · Henrijs Princis, Arindam Sharma, Cristina David
100. Typestate via Revocable Capabilities · Songlin Jia, Craig Liu, Siyuan He, Haotian Deng, Yuyan Bao, Tiark Rompf
101. Uniformity Analysis in the WebGPU Shading Language · James Lee-Jones, John Wickerson, Alastair F. Donaldson
102. Verification Modulo Tested Library Contracts · Abhishek Uppar, Omar Muhammad, Sumanth Prabhu S, Deepak D'Souza, P. Madhusudan, Adithya Murali
103. Verification of Recursively Defined Quantum Circuits · Mingsheng Ying, Zhicheng Zhang
104. Verifying Array Properties in Pure Data-Parallel Programs · Nikolaj Hey Hinnerskov, Robert Schenck, Cosmin E. Oancea
105. Versioned E-Graphs · Jahrim Gabriele Cesario, George Zakhour, Pascal Weisenburger, Guido Salvaneschi
106. VerusBelt: A Semantic Foundation for Verus's Proof-Oriented Extensions to the Rust Type System · Travis Hance, Laila Elbeheiry, Yusuke Matsushita, Derek Dreyer
107. Virtualizing Continuations · Cong Ma, Jonghyun Jung, Yizhou Zhang
108. Weighted NetKAT: A Programming Language for Quantitative Network Verification · Emmanuel Suárez Acevedo, Tiago Ferreira, Kevin Batz, Oliver Bøving, Nate Foster, Alexandra Silva