PLDI 2026
Proceedings of the ACM on Programming Languages, Volume 10, Number PLDI

Title Page

Sponsors

Editorial Message
Manu Sridharan
(University of California at Riverside, USA)

FlexHeap: Dynamic I/O-Aware Heap Resizing for Managed Applications
Iacovos G. Kolokasis, Shoaib Akram, Foivos S. Zakkak, Polyvios Pratikakis, and Angelos Bilas
(Foundation for Research and Technology Hellas, Greece; University of Crete, Greece; Australian National University, Australia; Red Hat, Ireland)

Publisher's Version

Fast Atomicity Monitoring
Hünkar Can Tunç, Yifan Dong, and Andreas Pavlogiannis
(Uber, Netherlands; Aarhus University, Denmark)

Publisher's Version

Versioned E-Graphs
Jahrim Gabriele Cesario, George Zakhour, Pascal Weisenburger, and Guido Salvaneschi
(University of St. Gallen, Switzerland)

Publisher's Version Published Artifact Artifacts Available

Towards Removing Undef Values from LLVM IR
Pedro Lobo, John McIver, George Mitenkov, Juneyoung Lee, Kirshanthan Sundararajah, and Nuno P. Lopes
(INESC-ID, Portugal; Instituto Superior Técnico - University of Lisbon, Portugal; Virginia Tech, USA; Aptos, USA; AWS, USA)

Publisher's Version

A Deductive System for Contract Satisfaction Proofs
Arthur Correnson, Haoyi Zeng, and Jana Hofmann
(CISPA Helmholtz Center for Information Security, Germany; Harvard University, USA; MPI-SP, Germany)

Publisher's Version Published Artifact Artifacts Available

Path-Sensitive Abstract Interpretation for WCET Estimation
Shangshang Xiao, Mengxia Sun, Wei Zhang, Naijun Zhan, and Lei Ju
(Shandong University, China; Peking University, China; Zhongguancun Laboratory, China)

Publisher's Version Published Artifact Artifacts Available

Decoupling Data Layouts from Bounding Volume Hierarchies
Christophe Gyurgyik, Alexander J Root, and Fredrik Kjolstad
(Stanford University, USA)

Publisher's Version Published Artifact Artifacts Available

Equality Saturation for Quantum Circuit Optimization
Ganxiang Yang, Paige Raun, Runzhou Tao, and Ronghui Gu
(Columbia University, USA; University of Maryland, USA; CertiK, USA)

Publisher's Version Published Artifact Artifacts Available

Cobble: Compiling Block Encodings for Quantum Computational Linear Algebra
Charles Yuan
(University of Wisconsin-Madison, USA)

Publisher's Version Published Artifact Artifacts Available

Bonsai: Compiling Queries to Pruned Tree Traversals
Alexander J Root, Christophe Gyurgyik, Purvi Goel, Kayvon Fatahalian, Jonathan Ragan-Kelley, Andrew Adams, and Fredrik Kjolstad
(Stanford University, USA; Massachusetts Institute of Technology, USA; Adobe Research, USA)

Publisher's Version

A Hierarchy of Supermartingales for ω-Regular Verification
Satoshi Kura and Hiroshi Unno
(Waseda University, Japan; Tohoku University, Japan)

Publisher's Version Published Artifact Artifacts Available

Solvable Tuple Patterns and Their Applications to Program Verification
Naoki Kobayashi, Ryosuke Sato, Ayumi Shinohara, and Ryo Yoshinaka
(University of Tokyo, Japan; Tokyo University of Agriculture and Technology, Japan; Tohoku University, Japan)

Publisher's Version Published Artifact Artifacts Available

Pure Borrow: Linear Haskell Meets Rust-Style Borrowing
Yusuke Matsushita and Hiromi Ishii
(Kyoto University, Japan; JIJ, Japan)

Publisher's Version

The Downgrading Semantics of Memory Safety
René Rydhof Hansen, Andreas Stenbæk Larsen, and Aslan Askarov
(Aalborg University, Denmark; Aarhus University, Denmark)

Publisher's Version Published Artifact Artifacts Available

A Mechanized Algebra of Verified Data Structures for Optimizing Sparse Tensor Programs
Amanda Liu, Gilbert Louis Bernstein, Shoaib Kamil, Adam Chlipala, and Jonathan Ragan-Kelley
(Massachusetts Institute of Technology, USA; University of Washington, USA; Adobe, USA)

Publisher's Version Published Artifact Artifacts Available

Flow-Analysis-Based Closure Optimization
John Reppy, Olin Shivers, and Byron Zhong
(University of Chicago, USA; Northeastern University, USA)

Publisher's Version Published Artifact Artifacts Available

Let It Flow: A Formally Verified Compilation Framework for Asynchronous Dataflow
Zhengyao Lin, Yi Cai, and Milijana Surbatovich
(Carnegie Mellon University, USA; University of Maryland at College Park, USA)

Publisher's Version Published Artifact Artifacts Available

Trace-Guided Synthesis of Effectful Test Generators
Zhe Zhou, Ankush Desai, Benjamin Delaware, and Suresh Jagannathan
(Purdue University, USA; Snowflake, USA)

Publisher's Version Published Artifact Artifacts Available

Contextual Refinement of Higher-Order Concurrent Probabilistic Programs
Kwing Hei Li, Alejandro Aguirre, Joseph Tassarotti, and Lars Birkedal
(Aarhus University, Denmark; New York University, USA)

Publisher's Version Published Artifact Artifacts Available

Cpp2Rust: Automatic Translation of C++ to Safe Rust
Lucian Popescu, Francisco Gouveia, Henrique Preto, João Silveira, Dmytro Hrybenko, José Fragoso Santos, and Nuno P. Lopes
(INESC-ID, Portugal; Instituto Superior Técnico - University of Lisbon, Portugal; Google, USA)

Publisher's Version

Compiling Strassen-like Matrix Multiplication Algorithms to Fast CUDA Kernels
Abhinav Jangda
(Microsoft Research, USA)

Publisher's Version

Semantic Reification: A New Paradigm for Random Program Generation
Kavya Chopra, Cong Li, Thodoris Sotiropoulos, and Zhendong Su
(ETH Zurich, Switzerland)

Publisher's Version

Contextual Embeddings: Implementing Bound Variables through Instance Resolution
Samantha Frohlich, Jessica Foster, G. A. Kavvos, and Meng Wang
(University of Bristol, UK)

Publisher's Version

&inator: Correct, Precise C-to-Rust Interface Translation
Victor Chen, Ayden Coughlin, and Michael D. Bond
(Ohio State University, USA)

Publisher's Version Published Artifact Artifacts Available

Iris-WasmFX: Modular Reasoning for Wasm Stack Switching
Maxime Legoupil, Mathias Pedersen, Lars Birkedal, Sam Lindley, and Jean Pichon-Pharabod
(Nanyang Technological University, Singapore; Aarhus University, Denmark; University of Edinburgh, UK)

Publisher's Version Published Artifact Artifacts Available

CoTenN: Constrained Optimization with Tensor Networks
Ritvik Sharma, Cheng Peng, Siddharth Dangwal, and Sara Achour
(Stanford University, USA; SLAC National Accelerator Laboratory, USA; University of Chicago, USA)

Publisher's Version

Verification of Recursively Defined Quantum Circuits
Mingsheng Ying and Zhicheng Zhang
(University of Technology Sydney, Australia)

Publisher's Version

Causality and Semantic Separation
Anna Zhang, Qinglan Luo, London Bielicke, Eunice Jun, and Adam Chlipala
(Massachusetts Institute of Technology, USA; Wellesley College, USA; University of California at Los Angeles, USA)

Publisher's Version Published Artifact Artifacts Available

Diagramming Program Values by Spatial Refinement
Siddhartha Prasad, Michael Tu, Karan Kashyap, Tim Nelson, and Shriram Krishnamurthi
(Brown University, USA)

Publisher's Version Published Artifact Artifacts Available

Hayroll: A Modular Wrapper for Translating C Macros and Conditional Compilation to Rust
Haoran Peng, Baris Kasikci, Gilbert Louis Bernstein, and Michael D. Ernst
(University of Washington, USA)

Publisher's Version

MatchBox: A Semantic Foundation for Data Plane Portability
Eric Hayden Campbell, Robert Zhang, Divyanshu Saxena, Aditya Akella, and Işıl Dillig
(University of Texas at Austin, USA)

Publisher's Version Published Artifact Artifacts Available

Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows
Zain K. Aamer, Rini Banerjee, Hiroyuki Katsura, David Kaloper-Meršinjak, Dimitrios J. Economou, Kayvan Memarian, Dhruv Makwana, Neel Krishnaswami, Benjamin C. Pierce, Christopher Pulte, and Peter Sewell
(University of Pennsylvania, USA; University of Cambridge, UK; University of Oxford, UK)

Publisher's Version

Choose, Don’t Label: Multiple-Choice Query Synthesis for Program Disambiguation
Celeste Barnaby, Danny Ding, Osbert Bastani, and Işıl Dillig
(University of Texas at Austin, USA; University of Pennsylvania, USA)

Publisher's Version

Kuiper: Correct and Efficient GPU Programming with Dependent Types and Separation Logic
Guido Martínez, Bastian Köpcke, Jonáš Fiala, Gabriel Ebner, Tahina Ramananandro, Michel Steuwer, Tyler Sorensen, and Nikhil Swamy
(Microsoft Research, USA; TU Berlin, Germany; ETH Zurich, Switzerland)

Publisher's Version

Towards Efficient Matching of Regexes with Backreferences using Register Set Automata
Vojtěch Havlena, Lukáš Holík, Ondřej Lengál, Jan Vašák, and Sabína Gulčíková
(Brno University of Technology, Czech Republic; Aalborg University, Denmark)

Publisher's Version

Parameterized Algorithms and Complexity for Function Merging with Branch Reordering
Amir K. Goharshady, Kerim Kochekov, Tian Shu, and Ahmed Khaled Zaher
(University of Oxford, UK; Hong Kong University of Science and Technology, Hong Kong)

Publisher's Version

A Compiler for Fused Relational Operations on Multisets
James Dong and Fredrik Kjolstad
(Stanford University, USA)

Publisher's Version

SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits
Nengkun Yu, Jens Palsberg, and Thomas Reps
(Stony Brook University, USA; University of California at Los Angeles, USA; University of Wisconsin-Madison, USA)

Publisher's Version

NEURA: A Unified and Retargetable Compilation Framework for Coarse-Grained Reconfigurable Architectures
Shangkun Li, Jinming Ge, Diyuan Tao, Zeyu Li, Jiawei Liang, Linfeng Du, Jiang Xu, Wei Zhang, and Cheng Tan
(Hong Kong University of Science and Technology, Hong Kong; Independent Researcher, China; Hong Kong University of Science and Technology, Guangzhou, China; Google, USA; Arizona State University, USA)

Publisher's Version Published Artifact Artifacts Available

SSA without Dominance for Higher-Order Programs
Roland Leißa and Johannes Griebler
(University of Göttingen, Germany)

Publisher's Version Published Artifact Artifacts Available

Cerisier: A Program Logic for Attestation in a Capability Machine
June Rousseau, Denis Carnier, Thomas Van Strydonck, Steven Keuchel, Dominique Devriese, and Lars Birkedal
(Aarhus University, Denmark; KU Leuven, Belgium; Fortanix, Netherlands)

Publisher's Version Published Artifact Artifacts Available

Presynthesis: Towards Scaling Up Program Synthesis with Finer-Grained Abstract Semantics
Rui Dong, Qingyue Wu, Danny Ding, Zheng Guo, Ruyi Ji, and Xinyu Wang
(University of Michigan, USA; University of Texas at Austin, USA)

Publisher's Version

Virtualizing Continuations
Cong Ma, Jonghyun Jung, and Yizhou Zhang
(University of Waterloo, Canada)

Publisher's Version Published Artifact Artifacts Available

Modular GPU Programming with Typed Perspectives
Manya Bansal, Daniel Sainati, Joseph W. Cutler, Saman Amarasinghe, and Jonathan Ragan-Kelley
(Massachusetts Institute of Technology, USA; University of Pennsylvania, USA)

Publisher's Version

State Space Estimation for DPOR-Based Model Checkers
A. R. Balasubramanian, Mohammad Hossein Khoshechin Jorshari, Rupak Majumdar, Umang Mathur, and Minjian Zhang
(MPI-SWS, Germany; National University of Singapore, Singapore; University of Illinois Urbana-Champaign, USA)

Publisher's Version Published Artifact Artifacts Available

Analyzing Bytes: Pre-Disassembly Static Binary Analysis
Huan Nguyen, Soumyakant Priyadarshan, Chencheng Jiang, and R. Sekar
(Google, USA; Stony Brook University, USA)

Publisher's Version

SureDistrib: Verifying Almost-Sure Termination of Composite Asynchronous Byzantine Protocols
Longfei Qiu, Jingqi Xiao, Ji-Yong Shin, and Zhong Shao
(Yale University, USA; University of Hong Kong, China; Northeastern University, USA)

Publisher's Version Published Artifact Artifacts Available

Fungible Memories for Automated Technology Mapping and Retargeting
Zachary D. Sisco, Sijie Kong, Daniel Ruelas-Petrisko, Jingtao Xia, Julian Springer, Varun Rao, Spencer Wang, Gus Henry Smith, Ben Hardekopf, and Jonathan Balkind
(Chinese University of Hong Kong, Shenzhen, China; University of California at Santa Barbara, USA; University of Washington, USA; TU Berlin, Germany; University of California at Berkeley, USA; Southmountain Research, USA)

Publisher's Version Published Artifact Artifacts Available

Heterogeneous Dynamic Logic: Provability Modulo Program Theories
Samuel Teuber, Mattias Ulbrich, André Platzer, and Bernhard Beckert
(KIT, Germany)

Publisher's Version Published Artifact Artifacts Available

SuperDP: Differential Privacy Refutation via Supermartingales
Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, and Đorđe Žikelić
(IST Austria, Austria; Singapore Management University, Singapore)

Publisher's Version

SIMT-Step Execution: A Flexible Operational Semantics For GPU Subgroup Behavior
Zheyuan Chen, Naomi Rehman, Guido Martínez, and Tyler Sorensen
(University of California at Santa Cruz, USA; University of California at Santa Barbara, USA; Microsoft Research, USA)

Publisher's Version Published Artifact Artifacts Available

Neptune: Advanced ML Operator Fusion for Locality and Parallelism on GPUs
Yifan Zhao, Egan Johnson, Prasanth Chatarasi, Vikram S. Adve, and Sasa Misailovic
(University of Illinois Urbana-Champaign, USA; IBM Research, USA)

Publisher's Version

Improving Equality Saturation for EDA via Semantic E-Graphs
Sijie Kong, Jingtao Xia, Daniel Ruelas-Petrisko, Zachary D. Sisco, Jonathan Balkind, and Gus Henry Smith
(University of California at Santa Barbara, USA; University of Washington, USA; Chinese University of Hong Kong, Shenzhen, China; Southmountain Research, USA)

Publisher's Version

Exploiting Sophisticated Static Analysis for Verilog
Qinlin Chen, Nairen Zhang, Jinpeng Wang, Jiacai Cui, Tian Tan, Xiaoxing Ma, Chang Xu, Jian Lu, and Yue Li
(Nanjing University, China)

Publisher's Version Published Artifact Artifacts Available

Bridging Coverage and Confidence: Reliable Static False Alarm Elimination via Input-Agnosticity
Jiayi Wang, Yu Wang, Linzhang Wang, and Ke Wang
(Nanjing University, China)

Publisher's Version Published Artifact Artifacts Available

Optimism in Equality Saturation
Russel Arbore, Alvin Cheung, and Max Willsey
(University of California at Berkeley, USA)

Publisher's Version Published Artifact Artifacts Available

Backwards-Compatible Row-Based Exceptions in ML
Simcha van Collem, Paulo Emílio de Vilhena, and Robbert Krebbers
(Radboud University Nijmegen, Netherlands; Imperial College London, UK)

Publisher's Version Published Artifact Artifacts Available

Verifying Array Properties in Pure Data-Parallel Programs
Nikolaj Hey Hinnerskov, Robert Schenck, and Cosmin Oancea
(University of Copenhagen, Denmark; Northeastern University, USA)

Publisher's Version Published Artifact Artifacts Available

Verification Modulo Tested Library Contracts
Abhishek Uppar, Omar Muhammad, Sumanth Prabhu S, Deepak D'Souza, P. Madhusudan, and Adithya Murali
(IISc Bangalore, India; Relyance AI, India; University of Illinois Urbana-Champaign, USA; University of Wisconsin-Madison, USA)

Publisher's Version Published Artifact Artifacts Available

Soteria: Efficient Symbolic Execution as a Functional Library
Sacha-Élie Ayoun, Opale Sjöstedt, and Azalea Raad
(Imperial College London, UK; Soteria Tools, UK)

Publisher's Version Published Artifact Artifacts Available

A Categorical Basis for Robust Program Analysis
Zachary Kincaid and Shaowei Zhu
(Princeton, USA)

Publisher's Version

SAIL: Sound Abstract Interpreters with LLMs
Qiuhan Gu, Avaljot Singh, and Gagandeep Singh
(University of Illinois Urbana-Champaign, USA)

Publisher's Version Published Artifact Artifacts Available

Intrinsically Correct Algorithms and Recursive Coalgebras
Cass Alexandru, Henning Urbat, and Thorsten Wißmann
(RPTU Kaiserslautern-Landau, Germany; Friedrich-Alexander University Erlangen-Nürnberg, Germany)

Publisher's Version Published Artifact Artifacts Available

Revisiting Partial Tracing for Safe, Efficient, and Concurrent Garbage Collection in Unmanaged Languages
Jeonghyeon Kim, Jongse Park, Youngjin Kwon, and Jeehoon Kang
(KAIST, Republic of Korea; FuriosaAI, Republic of Korea)

Publisher's Version Published Artifact Artifacts Available

Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic
Philipp G. Haselwarter, Alejandro Aguirre, Simon Oddershede Gregersen, Kwing Hei Li, Joseph Tassarotti, and Lars Birkedal
(Aarhus University, Denmark; New York University, USA)

Publisher's Version

Optimal Predicate Pushdown Synthesis
Robert Zhang, Eric Hayden Campbell, Dixin Tang, and Işıl Dillig
(University of Texas at Austin, USA)

Publisher's Version

SparseZETA: Intelligent Auto-tuner for Designing High-Performance SpMV Programs
Zhen Du, Ying Liu, Xionghui Chen, Yanbo Zhao, Xiaobing Feng, Huimin Cui, and Jiajia Li
(Institute of Computing Technology at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; Nanjing University, China; North Carolina State University, USA)

Publisher's Version

Hybrid Path-Sums for Hybrid Quantum Programs
Christophe Chareton, Sébastien Bardin, Jad Issa, Mathieu Nguyen, and Nicolas Blanco
(CEA List - Université Paris-Saclay, France)

Publisher's Version Published Artifact Artifacts Available

Fixed Parameter Tractable Linearizability Monitoring
Zheng Han Lee and Umang Mathur
(National University of Singapore, Singapore)

Publisher's Version

Incremental Density Calculation for Efficient Programmable Inference in Probabilistic Programs
Fabian Zaiser, Jack Czenszak, Martin C. Rinard, Vikash K. Mansinghka, and Alexander K. Lew
(Massachusetts Institute of Technology, USA; Yale University, USA)

Publisher's Version Published Artifact Artifacts Available

CRIS: The Power of Imagination in Hybrid Verification
Yonghee Kim, Taeyoung Yoon, Sanghyun Yi, Jaehyung Lee, Soonwon Moon, Yeji Han, Seonho Lee, Taeyoung Rhee, Yujin Im, Donghyun Nam, Jieung Kim, and Chung-Kil Hur
(Seoul National University, Republic of Korea; Yonsei University, Republic of Korea)

Publisher's Version Published Artifact Artifacts Available

Weighted NetKAT: A Programming Language For Quantitative Network Verification
Emmanuel Suárez Acevedo, Tiago Ferreira, Kevin Batz, Oliver Bøving, Nate Foster, and Alexandra Silva
(Cornell University, USA; University College London, UK; Technical University of Denmark, Denmark; EPFL, Switzerland; Jane Street, USA)

Publisher's Version

Implementability of Global Distributed Protocols Modulo Network Architectures
Elaine Li and Thomas Wies
(New York University, USA)

Publisher's Version Published Artifact Artifacts Available

Enumerating Ill-Typed Programs for Testing Type Analyzers
Thodoris Sotiropoulos and Zhendong Su
(ETH Zurich, Switzerland)

Publisher's Version

GradInf: Gradient Estimation as Probabilistic Inference
Gaurav Arya, Mathieu Huot, Moritz Schauer, Alexander K. Lew, and Feras A. Saad
(Carnegie Mellon University, USA; Massachusetts Institute of Technology, USA; Chalmers University of Technology - University of Gothenburg, Sweden; Yale University, USA)

Publisher's Version Published Artifact Artifacts Available

Nested Inductive Types: Justified and Usable Nested Inductive Types in Lean and Rocq
Thomas Lamiaux, Yannick Forster, Matthieu Sozeau, and Nicolas Tabareau
(Nantes Université, France; Inria, France)

Publisher's Version

Typestate via Revocable Capabilities
Songlin Jia, Craig Liu, Siyuan He, Haotian Deng, Yuyan Bao, and Tiark Rompf
(Purdue University, USA; Augusta University, USA)

Publisher's Version

Persistent Iterators with Value Semantics
Yihe Li and Gregory J. Duck
(National University of Singapore, Singapore)

Publisher's Version Published Artifact Artifacts Available

VerusBelt: A Semantic Foundation for Verus’s Proof-Oriented Extensions to the Rust Type System
Travis Hance, Laila Elbeheiry, Yusuke Matsushita, and Derek Dreyer
(MPI-SWS, Germany; Kyoto University, Japan)

Publisher's Version Published Artifact Artifacts Available

Restart and Refine: Scalable IFDS Taint Analysis across Memory Budgets
Yujiang Gui, Yonggang Tao, and Jingling Xue
(UNSW, Australia)

Publisher's Version Published Artifact Artifacts Available

Redundant Array Computation Elimination
Zixuan Wang, Liang Yuan, Xianmeng Jiang, Kun Li, Junmin Xiao, and Yunquan Zhang
(Institute of Computing Technology at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China)

Publisher's Version

Hyper Separation Logic
Trayan Gospodinov, Peter Müller, and Thibault Dardinier
(INSAIT at Sofia University St. Kliment Ohridski, Bulgaria; ETH Zurich, Switzerland)

Publisher's Version Published Artifact Artifacts Available

The Search for Constrained Random Generators
Harrison Goldstein, Hila Peleg, Cassia Torczon, Daniel Sainati, Leonidas Lampropoulos, and Benjamin C. Pierce
(SUNY Buffalo, USA; Technion, Israel; University of Pennsylvania, USA; University of Maryland at College Park, USA)

Publisher's Version

An Efficient Algorithm for Streaming BPE Tokenization
Konstantinos Mamouras, Angela W. Li, and Yudi Yang
(Rice University, USA)

Publisher's Version

Uniformity Analysis in the WebGPU Shading Language
James Lee-Jones, John Wickerson, and Alastair F. Donaldson
(Imperial College London, UK)

Publisher's Version Published Artifact Artifacts Available

Expecto: Extracting Formal Specifications from Natural Language Description for Trustworthy Oracles
Dongjae Lee and Kihong Heo
(KAIST, Republic of Korea)

Publisher's Version Published Artifact Artifacts Available

Synthesizing Backward Error Bounds, Backward
Laura Zielinski and Justin Hsu
(Cornell University, USA)

Publisher's Version Published Artifact Artifacts Available

Responsive Parallelism with Dynamic and First-Class Priorities
Marelle León, My Dinh, and Stefan K. Muller
(Illinois Institute of Technology, USA; University of Connecticut, USA)

Publisher's Version Published Artifact Artifacts Available

Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for Reachability Types
Songlin Jia, Guannan Wei, Siyuan He, Yuyan Bao, and Tiark Rompf
(Purdue University, USA; Tufts University, USA; Augusta University, USA)

Publisher's Version

Syntactic Implicit Parameters with Static Overloading
Daan Leijen and Tim Whiting
(Microsoft Research, USA; Brigham Young University, USA)

Publisher's Version

A Verified Parallel Scheduler for OCaml 5
Clément Allain and Gabriel Scherer
(Inria, France)

Publisher's Version

Neuro-symbolic Hierarchical Learning for Long-Horizon Robotic Tasks
Yu Huang, Ziji Wu, Zhengyi Ma, Kexin Ma, and Ji Wang
(National University of Defense Technology, China)

Publisher's Version Published Artifact Artifacts Available

SuperCollider: Scalable and Effective Data Race Detection for CUDA
Mark Stephenson, Sana Damani, Mohamed Tarek Ibn Ziad, Anis Ladram, and Michael Garland
(NVIDIA, USA)

Publisher's Version Published Artifact Artifacts Available

Pantomime: Constructive Leakage Proofs via Simulation
Robin Webbers, Robert Schenck, Wind Wong, Kristina Sojakova, and Klaus von Gleissenthall
(Vrije Universiteit Amsterdam, Netherlands; Northeastern University, USA)

Publisher's Version Published Artifact Artifacts Available

Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy
Eden Frenkel, Kenneth L. McMillan, Oded Padon, and Sharon Shoham
(Tel Aviv University, Israel; University of Texas at Austin, USA; Weizmann Institute of Science, Israel)

Publisher's Version Published Artifact Artifacts Available

Scalable Floating-Point Satisfiability via Staged Optimization
Yuanzhuo Zhang, Zhoulai Fu, and Binoy Ravindran
(Virginia Tech, USA; SUNY Korea, Republic of Korea; Stony Brook University, USA)

Publisher's Version Published Artifact Artifacts Available

Categorical Semantics of Probabilistic Symbolic Execution
John M. Li, Jack Czenszak, and Steven Holtzen
(Northeastern University, USA; Yale University, USA)

Publisher's Version Published Artifact Artifacts Available

Navigating AND–OR Graph Modifications to Debug Failing Proof Search
Justin Lubin, Marlena Preigh, Max Willsey, and Sarah E. Chasins
(University of California at Berkeley, USA)

Publisher's Version Published Artifact Artifacts Available

Compiling to Recurrent Neurons
Joey Velez-Ginorio, Nada Amin, Konrad Kording, and Steve Zdancewic
(University of Pennsylvania, USA; Harvard University, USA)

Publisher's Version Published Artifact Artifacts Available

Evolving Abstract Transformers for Gradient-Guided, Adaptable Abstract Interpretation
Shaurya Gomber, Debangshu Banerjee, and Gagandeep Singh
(University of Illinois Urbana-Champaign, USA)

Publisher's Version Published Artifact Artifacts Available

TreeCoder: Systematic Exploration and Optimisation of Decoding and Constraints for LLM Code Generation
Henrijs Princis, Arindam Sharma, and Cristina David
(University of Bristol, UK)

Publisher's Version Published Artifact Artifacts Available

Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification
Satoshi Kura, Hiroshi Unno, and Takeshi Tsukada
(Waseda University, Japan; Tohoku University, Japan; Chiba University, Japan)

Publisher's Version Published Artifact Artifacts Available

EREQ: Regular Expressions with Quantifiers and Incremental Quantifier Elimination
Ekaterina Zhuchko, Ian Erik Varatalu, Margus Veanes, and Nikolaj Bjørner
(Tallinn University of Technology, Estonia; Microsoft Research, USA)

Publisher's Version

A Formally Verified Foundation for Compositional Heterogeneous Coherence
An Qi Zhang, Andrés Goens, Daniel Sorin, and Vijay Nagarajan
(University of Utah, USA; TU Darmstadt, Germany; Duke University, USA)

Publisher's Version Published Artifact Artifacts Available

Abstract Interpretation with Confidence
Yuanfeng Shi, Ziyue Jin, and Xin Zhang
(Peking University, China)

Publisher's Version

Dynamically Checked Deep Immutability in Python
Fridtjof Stoldt, Sylvan Clebsch, Matthew A. Johnson, Matthew J. Parkinson, and Tobias Wrigstad
(Uppsala University, Sweden; Microsoft Azure Research, USA; Microsoft Azure Research, UK)

Publisher's Version Published Artifact Artifacts Available