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

Title Page


Article: pldi26foreword-fm000-p doi:

Sponsors


Article: pldi26foreword-fm003-p doi:

Editorial Message
Manu Sridharan
(University of California at Riverside, USA)
The Proceedings of the ACM series presents the highest-quality research conducted in diverse areas of computer science, as represented by the ACM Special Interest Groups (SIGs). The Proceedings of the ACM on Programming Languages (PACMPL) focuses on research on all aspects of programming languages, from design to implementation and from mathematical formalisms to empirical studies. The journal operates in close collaboration with the ACM Special Interest Group on Programming Languages (SIGPLAN) and is committed to making high-quality peer-reviewed scientific research in programming languages free of restrictions on both access and use.

Publisher's Version Article: pldi26editorial-fm001-p doi:10.1145/3818664

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)
Popular JVM-based search and analytics systems, such as Elasticsearch and Spark, rely on the OS page cache (I/O cache) to accelerate storage access. However, dividing memory between the JVM heap and the I/O cache creates a trade-off: enlarging the heap reduces garbage collection (GC) overhead but starves the I/O cache, while shrinking it improves I/O performance but raises GC cost. Existing heap resizing mechanisms ignore I/O and thus fail to address this trade-off, resulting in inefficient memory utilization and degraded performance.
In this paper, we propose FlexHeap, a heap resizing mechanism for Garbage First (G1), the default OpenJDK garbage collector, that dynamically partitions a fixed DRAM budget between the JVM heap and the I/O cache. Between GC intervals, it estimates the CPU time lost to GC and to I/O stalls and repartitions DRAM to reduce their combined cost. FlexHeap relies on three concepts: (1) It makes resizing decisions using G1 collection boundaries. (2) It uses a history-based approach to estimate the cost of GC and I/O stalls for the future intervals. (3) It uses an adaptive resizing step that scales with changes in the combined cost.
We implement FlexHeap in OpenJDK 21’s G1 garbage collector and evaluate it on two widely used systems: the Elasticsearch search engine and the Spark analytic framework. Compared to the G1 heap resizing mechanism, FlexHeap improves performance by an average of 30% in Elasticsearch and by an average of 33% in Spark. It outperforms Vertical G1, a state-of-the-art enhancement to the default G1 heap resizing mechanism, that returns unused memory to the OS eagerly, by 50% on average in throughput, demonstrating that JVM heap resizing needs to consider I/O overhead in search and analytics applications.

Publisher's Version Published Artifact Artifacts Available Article: pldi26main-p2-p doi:10.1145/3808247

Fast Atomicity Monitoring
Hünkar Can Tunç, Yifan Dong, and Andreas Pavlogiannis
(Uber, Netherlands; Aarhus University, Denmark)
Atomicity is a fundamental abstraction in concurrency, specifying that program behavior can be understood by considering specific code blocks executing atomically. However, atomicity invariants are tricky to maintain while also optimizing for code efficiency, and atomicity violations are a common root cause of many concurrency bugs. To address this problem, several dynamic techniques have been developed for testing whether a program execution adheres to an atomicity specification, most often instantiated as conflict serializability. The efficiency of the analysis has been targeted in various papers, with the state-of-the-art algorithms RegionTrack and Aerodrome achieving a time complexity O(nk³) and O(nk(k + v + ℓ)), respectively, for a trace σ of n events, k threads, v locations, and ℓ locks.
In this paper we introduce AtomSanitizer, a new algorithm for testing conflict serializability, with time complexity O(nk²). AtomSanitizer operates in an efficient streaming style, is theoretically faster than all existing algorithms, and also has a smaller memory footprint. Moreover, AtomSanitizer is the first algorithm designed to incur minimal locking when deployed in a concurrent monitoring setting. Experiments on standard benchmarks indicate that AtomSanitizer is always faster in practice than all existing conflict-serializability testers. Finally, we also implement AtomSanitizer inside the TSAN framework, for monitoring atomicity in real time. Our experiments reveal that AtomSanitizer incurs minimal time and space overhead compared to the data-race detection engine of TSAN, and thus is the first algorithm for conflict serializability demonstrated to be suitable for a runtime monitoring setting.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p10-p doi:10.1145/3808248

Versioned E-Graphs
Jahrim Gabriele Cesario, George Zakhour, Pascal Weisenburger, and Guido Salvaneschi
(University of St. Gallen, Switzerland)
E-Graphs are an efficient encoding for discovering and maintaining sets of equalities, commonly adopted in the context of formal proofs, program analysis, and optimization. In several scenarios, equalities may hold only conditionally, i.e., under certain assumptions. For example, in automated provers the proof is often split into multiple branches, such that each branch considers a different set of equalities. A limitation of traditional e-graphs is that they can only encode a single set of equalities at a time. Conditional equalities are then handled by maintaining multiple e-graphs, e.g., one for each branch in the proof, which is inefficient as equalities shared among branches are simply replicated many times.
In this paper, we introduce versioned e-graphs, which efficiently encode multiple equivalence sets at the same time, maximizing shared information among them. We formalize for versioned e-graphs and prove their correctness. We evaluate our solution against widely-adopted solutions which maintain multiple e-graphs and show that versioned e-graphs are up to 5–30 % more memory efficient and up to 4× faster depending on the case study, especially when solution spaces are large both in explored program terms and number of branches.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p12-p doi:10.1145/3808249

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 Labs, UK; AWS, USA)
LLVM’s intermediate representation (IR) has two deferred undefined behavior (UB) values: undef and poison. The existence of these two values has been a persistent source of bugs. Reasoning about the correctness of analyses and optimizations for the regular cases is already tricky; ensuring that these are sound for all UB cases is highly non-trivial.
Undef values, in particular, are one of the most misunderstood concepts of LLVM IR. On paper, the definition is simple: they represent an arbitrary value of the underlying type, and can yield a different value each time they are observed. However, this property makes even simple algebraic rewrites, such as replacing 2 × y with y + y, unsound in LLVM.
Because reasoning about undef is hard, and the benefits of having it are limited, we have set a roadmap to eliminate it altogether from LLVM IR. The last remaining use of undef is the value of uninitialized memory, which has implications on the lowering of bitfields, as well as raw data copies and comparisons.
In this paper, we propose an extension to LLVM IR that includes a raw memory value type and a freezing load. We show that these two constructs are sufficient to replace the remaining uses of undef in LLVM. Our implementation shows that these changes have minimal impact on both run-time and compile-time performance. By removing the final hurdle to eliminating undef from LLVM IR, this work paves the way for a simpler semantic model and easier reasoning about the soundness of IR analyses and optimizations.

Publisher's Version ACM SIGPLAN Distinguished Paper Award Article: pldi26main-p14-p doi:10.1145/3808250

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)
Hardware-software contracts are abstract specifications of a CPU's leakage behavior. They enable verifying the security of high-level programs against side-channel attacks without having to explicitly reason about the microarchitectural details of the CPU. Using the abstraction powers of a contract requires proving that the targeted CPU satisfies the contract in the sense that the contract over-approximates the CPU's leakage. Besides pen-and-paper reasoning, proving contract satisfaction has been approached mostly from the model-checking perspective, with approaches based on a (semi-)automated search for the necessary invariants.
As an alternative, this paper explores how such proofs can be conducted in interactive proof assistants. We start by observing that contract satisfaction is an instance of a more general problem we call relative trace equality, and we introduce relative bisimulation as an associated proof technique. Leveraging recent advances in the field of coinductive proofs, we develop a deductive proof system for relative trace equality. Our system is provably sound and complete, and it enables a modular and incremental proof style. It also features several reasoning principles to simplify proofs by exploiting symmetries and transitivity properties. We formalized our deductive system in the Rocq proof assistant and applied it to two challenging contract satisfaction proofs.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p15-p doi:10.1145/3808251

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)
Worst-Case Execution Time (WCET) analysis provides an upper bound on a program’s execution time and is fundamental to the design and verification of real-time systems. Accurate modeling of cache behavior is critical for WCET estimation, as cache-miss latency is typically orders of magnitude larger than cache-hit latency. Since cache behavior is path dependent, existing methods commonly use abstract interpretation to estimate cache behaviors without enumerating all paths. However, conventional abstract interpretation is context-agnostic—adopting the most conservative case across paths—and thus may produce an overestimated WCET bound. To bridge the gap between scalability and accuracy, we propose a path-sensitive abstract-interpretation-based cache analysis that maintains a set of cache states drawn from critical execution paths to derive context-aware cache behavior. This path-sensitive cache analysis integrates seamlessly into standard WCET frameworks, resulting in tight yet provably sound WCET bounds. Experiments show that our approach improves WCET accuracy by an average of 24.83% without sacrificing scalability.

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: pldi26main-p17-p doi:10.1145/3808252

Decoupling Data Layouts from Bounding Volume Hierarchies
Christophe Gyurgyik, Alexander J Root, and Fredrik Kjolstad
(Stanford University, USA)
Bounding volume hierarchies are ubiquitous acceleration structures in graphics, scientific computing, and data analytics. Their performance depends critically on data layout choices that affect cache utilization, memory bandwidth, and vectorization---increasingly dominant factors in modern computing. Yet, in most programming systems, these layout choices are hopelessly entangled with the traversal logic. This entanglement prevents developers from independently optimizing data layouts and algorithms across different contexts, perpetuating a false dichotomy between performance and portability. We introduce Scion, a domain-specific language and compiler for specifying the data layouts of bounding volume hierarchies independent of tree traversal algorithms. We show that Scion can express a broad spectrum of layout optimizations used in high-performance computing while remaining architecture-agnostic. We demonstrate empirically that Pareto-optimal layouts (along performance and memory footprint axes) vary across algorithms, architectures, and workload characteristics. Through systematic design exploration, we also identify a novel ray tracing layout that combines optimization techniques from prior work, achieving Pareto-optimality across diverse architectures and scenes.

Publisher's Version Published Artifact Artifacts Available Article: pldi26main-p19-p doi:10.1145/3808253

Equality Saturation for Quantum Circuit Optimization
Ganxiang Yang, Paige Raun, Runzhou Tao, and Ronghui Gu
(Columbia University, USA; University of Maryland, USA; CertiK, USA)
Optimizing a quantum circuit is hard because it requires exploring a vast space of functionally equivalent circuits, produced by applying local circuit rewrites such as gate cancellation and commutation. Each additional rewrite can exponentially expand the space of equivalent circuits, so existing optimizers can only explore a tiny fraction of this space and often produce suboptimal results. We present Quasar, a new quantum circuit optimizer that can generate a step-limited optimal circuit: given a bound on rewrite iterations, it returns the lowest-cost circuit reachable within that bound. To achieve this, Quasar constructs two complementary e-graphs for the quantum circuit’s graph and sequence representations. Quasar then infers an atomic rewrite set for application on both e-graphs, which improves optimization performance by orders of magnitude. Finally, Quasar employs a series of new optimization techniques to ensure both soundness and scalability of equality saturation on quantum circuits. Across standard benchmarks, Quasar achieves geometric-mean reductions of 20.2% in 2-qubit gate count, 33.5% in total gate count, and 24.2% in circuit depth, and a 21.4% fidelity improvement over unoptimized circuits, outperforming or matching state-of-the-art rewrite-based optimizers on 75%, 92%, 62%, and 80% of circuits, respectively.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p23-p doi:10.1145/3808254

Cobble: Compiling Block Encodings for Quantum Computational Linear Algebra
Charles Yuan
(University of Wisconsin-Madison, USA)
Quantum algorithms for computational linear algebra promise up to exponential speedups for applications such as simulation and regression, making them prime candidates for hardware realization. But these algorithms execute in a model that cannot efficiently store matrices in memory like a classical algorithm does, instead requiring developers to implement complex expressions for matrix arithmetic in terms of correct and efficient quantum circuits. Among the challenges for the developer is navigating a cost model in which conventional optimizations for linear algebra, such as subexpression reuse, can be inapplicable or unprofitable.
In this work, we present Cobble, a language for programming with quantum computational linear algebra. Cobble enables developers to express and manipulate the quantum representations of matrices, known as block encodings, using high-level notation that automatically compiles to correct quantum circuits. Cobble features analyses that compute the time and space usage of programs, as well as optimizations that reduce overhead and generate efficient circuits using state-of-the-art techniques such as the quantum singular value transformation. We evaluate Cobble on benchmark kernels for simulation, regression, search, and other applications, showing 2.6x-25.4x speedups on these benchmarks compared to the unoptimized baseline.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable ACM SIGPLAN Distinguished Paper Award Article: pldi26main-p24-p doi:10.1145/3808255

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)
Trees can accelerate queries that search or aggregate values over large collections. They achieve this by storing metadata that enables quick pruning (or inclusion) of subtrees when predicates on that metadata can prove that none (or all) of the data in a subtree affect the query result. Existing systems implement this pruning logic manually for each query predicate and data structure. We generalize and mechanize this class of optimization. Our method derives conditions for when subtrees can be pruned (or included wholesale), expressed in terms of the metadata available at each node. We efficiently generate these conditions using symbolic interval analysis, extended with new rules to handle geometric predicates (e.g., intersection, containment). Additionally, our compiler fuses compound queries (e.g., reductions on filters) into a single tree traversal. These techniques enable the automatic derivation of generalized single-index and dual-index tree joins that support a wide class of join predicates beyond standard equality and range predicates. The generated traversals match the behavior of expert-written code that implements query-specific traversals, and can asymptotically outperform the linear scans and nested-loop joins that existing systems fall back to when hand-written cases do not apply.

Publisher's Version Published Artifact Artifacts Available ACM SIGPLAN Distinguished Paper Award Article: pldi26main-p25-p doi:10.1145/3808256

A Hierarchy of Supermartingales for ω-Regular Verification
Satoshi Kura and Hiroshi Unno
(Waseda University, Japan; Tohoku University, Japan)
We propose new supermartingale-based certificates for verifying almost sure satisfaction of ω-regular properties: (1) generalised Streett supermartingales (GSSMs) and their lexicographic extension (LexGSSMs), (2) distribution-valued Streett supermartingales (DVSSMs), and (3) progress-measure supermartingales (PMSMs) and their lexicographic extension (LexPMSMs). GSSMs, LexGSSMs, and DVSSMs are derived from least-fixed point characterisations of positive recurrence and null recurrence of Markov chains with respect to given Streett conditions; and PMSMs and LexPMSMs are probabilistic extensions of parity progress measures. We study the hierarchy among these certificates and existing certificates, namely Streett supermartingales, by comparing the classes of problems that can be verified by each type of certificates. Notably, we show that our certificates are strictly more powerful than Streett supermartingales. We also prove completeness of GSSMs for positive recurrence and of DVSSMs for null recurrence: DVSSMs are, in theory, the most powerful certificates in the sense that for any Markov chain that almost surely satisfies a given ω-regular property, there exists a DVSSM certifying it. We provide a sound and relatively complete algorithm for synthesising LexPMSMs, the second most powerful certificates in the hierarchy. We have implemented a prototype tool based on this algorithm, and our experiments show that our tool can successfully synthesise certificates for various examples including those that cannot be certified by existing supermartingales.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p28-p doi:10.1145/3808257

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)
Despite the recent progress of automated program verification techniques, fully automated verification of programs manipulating recursive data structures remains a challenge. We introduce solvable tuple patterns (STPs) and conjunctive STPs (CSTPs), novel formalisms for expressing and inferring invariants between list-like recursive data structures. A distinguishing feature of STPs is that they can be efficiently inferred from only a small number of positive samples; no negative samples are required. After presenting properties and inference algorithms of STPs and CSTPs, we show how to incorporate the CSTP inference into a CHC (Constrained Horn Clauses) solver supporting list-like data structures, which serves as a uniform backend for automated program verification tools. A CHC solver incorporating the (C)STP inference has won the ADT-LIN category of CHC-COMP 2025 by a significant margin.

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: pldi26main-p33-p doi:10.1145/3808258

Pure Borrow: Linear Haskell Meets Rust-Style Borrowing
Yusuke Matsushita and Hiromi Ishii
(Kyoto University, Japan; JIJ, Japan)
A promising approach to unifying functional and imperative programming paradigms is to localize mutation using linear or affine types. Haskell, a purely functional language, was recently extended with linear types by Bernardy et al., in the name of Linear Haskell. However, it remained unknown whether such a pure language could safely support non-local borrowing in the style of Rust, where each borrower can be freely split and dropped without direct communication of ownership back to the lender.
We answer this question affirmatively with Pure Borrow, a novel framework that realizes Rust-style borrowing in Linear Haskell with purity. Notably, it features parallel state mutation with affine mutable references inside pure computation, unlike the IO and ST monads and existing Linear Haskell APIs. It also enjoys purity, lazy evaluation, first-class polymorphism and leak freedom, unlike Rust. We implement Pure Borrow simply as a library in Linear Haskell and demonstrate its power with a case study in parallel computing. We formalize the core of Pure Borrow and build a metatheory that works toward establishing safety, leak freedom and confluence, with a new, history-based model of borrowing.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p38-p doi:10.1145/3808259

The Downgrading Semantics of Memory Safety
René Rydhof Hansen, Andreas Stenbæk Larsen, and Aslan Askarov
(Aalborg University, Denmark; Aarhus University, Denmark)
Memory safety is traditionally characterized in terms of bad things that cannot happen. This approach is currently embraced in the literature on formal methods for memory safety. However, a general semantic principle for memory safety, that implies the negative items, remains elusive.
This paper focuses on the allocator-specific aspects of memory safety, such as null-pointer dereference, use after free, double free, and heap overflow. To that extent, we propose a notion of gradual allocator independence that accurately captures the allocator-dependent aspects of memory safety. Our approach is inspired by the previously suggested connection between memory safety and noninterference, but extends that connection in a fundamentally important direction towards downgrading.
We consider a low-level language with access to an allocator that provides malloc and free primitives in a flat memory model. Pointers are just integers, and as such it is trivial to write memory-unsafe programs. The basic intuition of gradual allocator independence is that of noninterference, namely that allocators must not influence program execution. This intuition is refined in two important ways that account for the allocators running out-of-memory and for programs to have pointer-to-integer casts. The key insight of the definition is to treat these extensions as forms of downgrading and give them satisfactory technical treatment using the state-of-the-art information flow machinery.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p49-p doi:10.1145/3808260

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)
In this paper, we introduce a verified framework for defining and composing sparse tensor formats. We extend the ATL tensor language and scheduling framework, which formerly could only express dense tensor kernels. We define a levelized abstraction to describe per-dimension tensor formats via their encoding routines, access and iteration functions, and formal properties enforcing soundness of the sparse structures as representations of the original dense tensors. Using this abstraction, we compositionally define format-agnostic, multidimensional compression and decompression functions that are used to express the top-level soundness theorem for these abstract sparse tensor formats. We then use this soundness theorem as an adjoint-pair rewrite theorem to introduce sparse data structures and iteration into a dense tensor kernel via the existing scheduling-rewrite framework of ATL. Overall, we are able to start with a program computing over dense operands and derive a proven semantically equivalent, optimized program computing over sparse structures. We further prove a minimal set of instances of the level-format abstraction, which can be composed and passed as parameters to compression to capture a broad range of canonical, multidimensional tensor-compression formats.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p53-p doi:10.1145/3808261

Flow-Analysis-Based Closure Optimization
John Reppy, Olin Shivers, and Byron Zhong
(University of Chicago, USA; Northeastern University, USA)
One of the key implementation challenges for higher-order functional languages is managing the representation of first-class function values. The standard approach to this problem is closure conversion, which is a compiler transformation that introduces an explicit data structure to represent the environment of a function value. Constructing the closure for a nested function usually involves copying data from the enclosing function’s closure. To avoid this copying, one might use linked representations, but that choice makes variable access slow and can introduce space leaks. Shao and Appel developed an effective closure converter that reduces copying and is safe-for-space, but their converter is based on a weak, first-order analysis.
In this paper, we present a new safe-for-space closure converter that uses a higher-order flow analysis to inform closure-representation decisions. We describe how this information can be used to improve two aspects of closure optimization: sharing heap-allocated tuples of variables and spreading variables into argument registers. We have implemented our converter in the Standard ML of New Jersey system and demonstrated that it produces better code on average than the Shao and Appel converter, with significant performance gains for some benchmarks.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p54-p doi:10.1145/3808262

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)
Dataflow architectures have gained renewed interest due to their balance between energy efficiency and performance. In (spatial) dataflow architectures, a program is represented as a set of entirely distributed and dynamically scheduled dataflow operators that communicate through asynchronous channels, which greatly improves data locality and parallelism. However, compiling to dataflow architectures remains an error-prone process, due to the difficulty of maintaining determinacy while enabling pipelining. Determinacy means that the result of a dataflow program is deterministic and independent of the schedule of operator execution, and pipelining is an important optimization in spatial dataflow that enables parallelism across loop iterations.
In this work, we present Wavelet, the first effort to formally verify a compiler for asynchronous dataflow. We use a mix of techniques to achieve this goal. Our frontend uses a novel capability type system with fences to synchronize conflicting memory accesses and enable pipelining. We then verify a Lean formalization of two core compiler passes that translate elaborated programs from the type checker to dataflow graphs, proving important properties of forward simulation and determinacy. Notably, our formalization semantically propagates the soundness guarantees of the frontend type system, ensuring modularity between simulation and determinacy proofs. In our evaluation, we show that dataflow graphs compiled by Wavelet have comparable quality to those produced by unverified dataflow compilers from RipTide and LLVM CIRCT.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p56-p doi:10.1145/3808263

Trace-Guided Synthesis of Effectful Test Generators
Zhe Zhou, Ankush Desai, Benjamin Delaware, and Suresh Jagannathan
(Purdue University, USA; Snowflake, USA)
Several recently proposed program logics have incorporated notions of underapproximation into their design, enabling them to reason about reachability rather than safety. In this paper, we explore how similar ideas can be integrated into an expressive type and effect system. We use the resulting underapproximate type specifications to guide the synthesis of test generators that probe the behavior of effectful black-box systems. A key novelty of our type language is its ability to capture underapproximate behaviors of effectful operations using symbolic traces that expose latent data and control dependencies, constraints that must be preserved by the test sequences the generator outputs. We implement this approach in a tool called , and evaluate it on a diverse range of applications by integrating ’s synthesized generators into property-based testing frameworks like QCheck and model-checking tools like P. In both settings, the generators synthesized by are significantly more effective than the default testing strategy, and are competitive with state-of-the-art, handwritten solutions.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p68-p doi:10.1145/3808264

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)
We present Foxtrot, the first higher-order separation logic for proving contextual refinement of higher-order concurrent probabilistic programs with higher-order local state. From a high level, Foxtrot inherits various concurrency reasoning principles from standard concurrent separation logic, e.g. invariants and ghost resources, and supports advanced probabilistic reasoning principles for reasoning about complex probability distributions induced by concurrent threads, e.g. tape presampling and induction by error amplification. The integration of these strong reasoning principles is highly non-trivial due to the combination of probability and concurrency in the language and the complexity of the Foxtrot model; the soundness of the logic relies on a version of the axiom of choice within the Iris logic, which is not used in earlier work on Iris-based logics. We demonstrate the expressiveness of Foxtrot on a wide range of examples, including the adversarial von Neumann coin and the randombytes_uniform function of the Sodium cryptography software library.
All results have been mechanized in the Rocq proof assistant and the Iris separation logic framework.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p77-p doi:10.1145/3808265

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, Germany)
About 70% of security vulnerabilities in widely deployed software originate from memory-safety bugs in languages such as C and C++. Despite decades of investment in mitigations, from static analysis and sanitizers to hardware isolation, attackers continue to exploit unsafe memory operations. A promising long-term solution is to migrate existing C++ codebases to memory-safe languages such as Rust, but doing so manually is prohibitively expensive and error-prone.
In this paper, we present Cpp2Rust, the first system capable of translating C++ programs into functionally equivalent and memory-safe Rust code automatically. By trading some performance for security, Cpp2Rust addresses the fundamental mismatch between C++’s unrestricted aliasing and Rust’s ownership model by inserting runtime-enforced ownership and mutability checks, ensuring safety while preserving semantics. To mitigate the performance overhead of dynamic checks, we developed a suite of source-to-source optimizations for Rust code that eliminate redundant ownership operations and recover much of the lost performance.
We evaluate Cpp2Rust on two real-world C++ programs, totaling 13k lines of code: WOFF2, a font compression library, and Brunsli, a JPEG lossless compression library. Cpp2Rust achieves full memory safety with only a 2% performance penalty on WOFF2 compression, while being 6× slower on Brunsli due to heavy usage of pointer arithmetic. These results demonstrate that automated, semantics-preserving translation from C++ to safe Rust is practical for some safety-critical applications, offering a viable path toward eliminating memory-safety vulnerabilities in legacy systems.

Publisher's Version Article: pldi26main-p91-p doi:10.1145/3808266

Compiling Strassen-like Matrix Multiplication Algorithms to Fast CUDA Kernels
Abhinav Jangda
(Microsoft Research, USA)
Matrix multiplication is a key operation in scientific computing and machine learning, with GPU libraries like NVIDIA Cutlass and cuBLAS providing optimized implementations of the three nested loop cubic algorithm. While sub-cubic algorithms, like the Strassen algorithm and its variants, are theoretically faster, their recursive structure makes it challenging to implement efficient GPU kernels. This is why existing approaches either do excessive memory accesses or do not effectively overlap memory accesses and computations, leading to sub-optimal performance compared to theoretical expectations.
This paper presents SubCuber, a domain-specific compiler that generates efficient CUDA kernels for Strassen-like matrix multiplication algorithms. SubCuber contains two novel CUDA kernels that are designed to minimize memory input loads and effectively overlap computation with memory loads. To generate efficient code, SubCuber constructs the dependency graph of a Strassen-like algorithm, selects efficient kernel schedules, and applies fusion strategies tailored to a recursion level, matrix sizes, and GPU. Our evaluation on NVIDIA A100 and H200 GPUs shows that for both single- and half-precision floating point matrix multiplications, SubCuber’s generated code outperforms state-of-the-art CUDA implementations for matrix multiplication and the Strassen algorithm. SubCuber is up to 12% faster for one recursion level and 22% for two recursion levels over Cutlass and cuBLAS, while existing approaches are only up to 8% faster for one-level and 16% faster for two-levels. Furthermore, SubCuber makes matrix multiplication in language models like Phi-4 14B, Qwen-3 32B, and LLaMA-3 405b, up to 16% faster for inference scenarios.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p97-p doi:10.1145/3808267

Semantic Reification: A New Paradigm for Random Program Generation
Kavya Chopra, Cong Li, Thodoris Sotiropoulos, and Zhendong Su
(ETH Zurich, Switzerland)
We introduce semantic reification, a novel paradigm for random program generation that centers on program semantics rather than syntax. Our key insight is to reformulate random program generation to capture two types of program semantics: (1) compile-time semantics (what a program can do), represented by the control flow graph (CFG), and (2) runtime semantics (what a program actually does), represented by execution paths within the CFG. For any CFG and any execution path on it, semantic reification constructs a program guaranteed to be well-behaved with respect to a specific input and output. This means that when executed with this input, the program deterministically follows the designated execution path to produce the expected output. This paradigm differs from existing work by supporting arbitrary control flow such as unbounded loops and irreducible regions, while still ensuring that the generated programs are semantically correct and terminating. We develop a practical realization of this paradigm. First, we introduce symbolic function reification that integrates a lightweight form of symbolic execution into the generation process to generate an individual, leaf function (i.e., a function that is free of function calls). Each leaf function satisfies the constraints of a given CFG and a selected execution path. Second, we compose multiple leaf functions into a larger, more complex program via semantics-preserving peephole rewriting, guided by an arbitrary call graph. Over five months, our implementation for C compilers, Reify, has uncovered 59 bugs in GCC and LLVM (57 confirmed, 27 fixed), 24 of which are long-latent. Among them, 36 are wrong-code bugs, many are high-priority issues, and most of them involve semantic characteristics overlooked by existing tools. We believe semantic reification opens new directions for research beyond compilers, such as validating debuggers, analyzers, and verifiers.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p100-p doi:10.1145/3808268

Contextual Embeddings: Implementing Bound Variables through Instance Resolution
Samantha Frohlich, Jessica Foster, G. A. Kavvos, and Meng Wang
(University of Bristol, UK)
Representing bound variables in embedded languages is a challenging problem, often requiring painful trade-offs between expressivity and usability. On the one hand, first-order representations using de Bruijn indices have many nice properties, but quickly become difficult to read and write. On the other hand, higher-order representations can piggy-back on the host language's binders to offer a more ergonomic interface, at a variety of costs depending on the technique. The current state-of-the-art is unembedding, i.e. a translation from the higher-order representation to the first-order and back again to get the best of both worlds. Unfortunately, the fact that this translation is type-safe relies on external metatheoretic arguments, holding unembedding back from its true potential. We solve this problem with a new embedding technique that uses instance resolution to define a context-directed isomorphism between an ergonomic higher-order interface and a first-order representation. Unlike previous techniques, this also applies to embedded languages with modal and substructural (e.g. linear) type systems, making unembedding relevant for modern languages.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p102-p doi:10.1145/3808269

&inator: Correct, Precise C-to-Rust Interface Translation
Victor Chen, Ayden Coughlin, and Michael D. Bond
(Ohio State University, USA)
Automatically translating system software from C to Rust is an appealing but challenging problem, as it requires whole-program reasoning to satisfy Rust’s ownership and borrowing discipline. A key enabling step in whole-program translation is interface translation, which produces Rust declarations for the C program’s top-level declarations (i.e., structs and function signatures), enabling modular and incremental code translation.
This paper introduces correct, precise C-to-Rust interface translation, called &inator. &inator employs a novel constraint-based formulation of semantic equivalence and type correctness including borrow-checking rules to produce a Rust interface that is correct (i.e., the interface admits a semantics-preserving implementation in safe Rust) and precise (i.e., it uses the simplest, least costly types). Our results show &inator produces correct, precise Rust interfaces for real C programs, but support for certain C features and scaling to large programs are challenges left for future work. This work advances the state of the art by being the first correct, precise approach to C-to-Rust interface translation.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p110-p doi:10.1145/3808270

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)
WasmFX is a proposed extension of Wasm, a low-level portable bytecode, with primitives for explicitly manipulating execution stacks as continuations. By exposing an interface of effect handlers, WasmFX enables non-local control flow features to be compiled in a modular way: one handcrafts a library that directly implements such features in WasmFX, and compilation then merely calls into the library. Alas, code involving non-local control flow is notoriously challenging, and so this proposal raises the questions of the soundness of the language extension, and of the correctness of such handcrafted libraries. In this paper, we first describe WasmFXCert, a mechanisation of WasmFX in Rocq, and prove the expected type soundness result. We then develop Iris-WasmFX, a program logic to reason about Wasm programs that use effect handlers, and illustrate its application to two key use cases of effect handlers: a coroutine library, and a generator. Together, these validate the design of WasmFX, and provide a modular framework for verifying future effect-based libraries.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p111-p doi:10.1145/3808271

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)
Simulation of physics problems is one of the most important use cases of quantum computing. For this class of problems, the goal is typically to find the minimum energy state, or the ground state, of a physical system’s Hamiltonian. These problems frequently have constraints, such as symmetry conditions, which must also be satisfied. To solve such problems, researchers in computational physics use quantum-inspired algorithms that execute on classical computers. In particular, tensor network-based eigensolvers such as DMRG have become popular.
However, to use these eigensolvers, the constrained optimization problem must first be encoded as a tensor network that implements a low-rank decomposition of the system’s Hamiltonian and state vector. These tensor network encodings are highly flexible, allowing for variables with ≥ 2 quantum states and supporting efficient constraint encodings that directly constrain the state vector. A critical challenge to developing tensor network-based encodings is that, currently, the encoding process is manual; significant effort is required to identify an efficient encoding for a new physics problem. In this work, we introduce a quantum constrained optimization problem (QCOP), a general abstraction for describing minimization problems over quantum variables that are subject to hard constraints. We present Masq, the first constraint programming language for QCOPs implementable with tensor networks, and CoTenN, a compiler that automatically maps QCOPs specified with Masq programs to tensor networks. To demonstrate the utility of Masq and CoTenN, we formulate two physics problems in Masq and then use CoTenN to find their ground states. We find the CoTenN-generated tensor networks generally outperform SOTA problem formulations, providing between 2.05×–53.32× total speedups across runs for QCOPs and yielding up to 2.49 · 10⁷× lower truncation errors for otherwise unconstrained problems.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p126-p doi:10.1145/3808272

Verification of Recursively Defined Quantum Circuits
Mingsheng Ying and Zhicheng Zhang
(University of Technology Sydney, Australia)
Recursive techniques have recently been introduced into quantum programming so that a variety of large quantum circuits and algorithms can be elegantly and compactly programmed. In this paper, we present a proof system for formal verification of the correctness of recursively defined quantum circuits. The soundness and (relative) completeness of the proof system are established. To demonstrate its effectiveness, we present a series of application examples, including formal verification of multi-qubit controlled gates, a quantum circuit for generating multi-qubit GHZ (Greenberger-Horne-Zeilinger) states, and more sophisticated quantum algorithms with recursive structures such as the quantum Fourier transform, quantum state preparation, and quantum random access memories (QRAMs).

Publisher's Version ACM SIGPLAN Distinguished Paper Award Article: pldi26main-p130-p doi:10.1145/3808273

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)
The design of scientific experiments deserves its own variation of formal verification to catch cases where scientists made important mistakes, such as forgetting to take confounding variables into account. One of the most fundamental underpinnings of science is causality, or what it means for interventions in the world to cause other outcomes, as formalized by computer scientists like Judea Pearl. However, these ideas had not previously been made rigorous to the standards of the programming-languages community, where one expects a (syntactic) program analysis to be proved sound with respect to a natural semantics. In the domain of causality, as the relevant “program analysis,” we focus on d-separation, a classic condition on graphs that can be used to decide when the design of an experiment controls for sufficiently many confounding variables, even though the reason that this condition works is often unintuitive. Our central result (mechanized in Rocq) is that d-separation exactly coincides with a novel semantic definition inspired by noninterference from the theory of security. This characterization provides a structural semantic foundation for d-separation and helps explain why the graph-theoretic condition is correct, independently of probabilistic assumptions. For each given automated test on the quality of an experiment design, our theorem justifies an associated method for falsifying the world-modeling hypothesis behind the experiment.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p135-p doi:10.1145/3808274

Diagramming Program Values by Spatial Refinement
Siddhartha Prasad, Michael Tu, Karan Kashyap, Tim Nelson, and Shriram Krishnamurthi
(Brown University, USA)
Diagrams enable programmers to reason, debug, and communicate. However, constructing diagrams for programming language data is unnecessarily hard. We present a declarative DSL, Spytial, that captures the essential spatial features of data. We endow Spytial with a spatial semantics, mapping values to the 2D plane, and prove key properties. Spytial uses constraint-solving to make interactive renderings. We show how Spytial can be embedded in three very different languages: Python, Rust, and Pyret. We present a novel counterfactual debugging aid for diagramming errors, combining textual and visual output. We evaluate the language and system for expressiveness, performance, and diagnostic quality. Finally, we also show how Spytial can be used to construct values interactively and visually while preserving spatial constraints.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p141-p doi:10.1145/3808275

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)
Previous C-to-Rust translators run the C preprocessor cpp on their input before translation. This discards configurability, and it loses programmer-defined abstractions expressed as C macros.
We present Hayroll, a modular wrapper that makes C-to-Rust translation preprocessor-aware without modifying the underlying translator. Hayroll consists of two cooperating layers. The conditional compilation translation layer uses symbolic execution to derive activation conditions for each line of the source code. It splits the program into a set of configuration-specific translation tasks that together cover every line of code. These tasks are then passed independently to the macro translation layer. The macro translation layer classifies macros, annotates macro-expanded nodes with tags, and sends the code through the underlying translator. It then reconstructs C macros as Rust functions or macros by retrieving these tags from the translator’s output. Because the layers communicate only through task partitioning and source-code annotations, the underlying translator remains a black box; no invasive changes are required. Our implementation uses C2Rust, but the design is translator-agnostic.
We evaluated Hayroll on CRUST-Bench, LibmCS, and zlib. Hayroll successfully reconstructs most syntactical macros and avoids configuration explosion through symbolic execution. Hayroll's output passes the same tests as the underlying C-to-Rust transpiler. These results show that decoupled preprocessor analysis can restore configurability and abstraction to C-to-Rust translation in a practical and modular way.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p150-p doi:10.1145/3808276

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)
Match-action tables are the core abstraction underlying network packet-processing systems, from fixed-function switches to eBPF-based software dataplanes. However, their concrete syntax and semantics vary widely across programming environments, reflecting differences in hardware generations, engineering practices, and vendor design choices. This syntactic and semantic variation renders portability of match-action tables across environments a persistent challenge. This paper presents MatchBox, a system for translating match-action tables across heterogeneous environments. At its core is the Match Algebra, a compositional formalism for concisely and declaratively expressing transformations on match-action tables. To ensure unambiguous semantics, MatchBox introduces a static type system based on guarded functional dependencies (GFDs) that guarantees that every well-typed Match Algebra expression denotes a well-defined function. From such specifications, the MatchBox compiler efficiently computes compact target tables that are semantically faithful. Across case studies in programmable switches, multi-cloud firewalls, and eBPF systems, MatchBox enables concise, declarative portability specifications and realizes them as compact target tables.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable ACM SIGPLAN Distinguished Paper Award Article: pldi26main-p153-p doi:10.1145/3808277

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)
We seek to enable more flexible use of rich specifications in a variety of ways that smoothly extend conventional software development practice. We show how a single specification language, based on separation logic to capture the subtle ownership disciplines of systems code, can be used for runtime assertion checking, for property-based testing, and for formal machine-checked proof—and how each of these complements and supports the others. We demonstrate all this on a challenging example: a component of a production hypervisor, running both stand-alone at user level and in situ in the hypervisor.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p155-p doi:10.1145/3808278

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)
High-level specifications of code are inherently ambiguous, and prior systems have explored interactive techniques to help users clarify their intent and resolve such ambiguities. However, most existing approaches elicit supervision through labeled examples, which are often error-prone and may fail to capture user intent. This paper introduces a new active learning paradigm for program disambiguation based on multiple-choice queries. In this paradigm, the system presents a small set of high-level behaviors as multiple-choice options, and the user simply selects the intended one. Technically, each answer option corresponds to a Hoare triple that characterizes a cluster of semantically similar candidate programs. This formulation enables formal reasoning about the informativeness and interpretability of queries, and supports systematic construction of optimal queries. Building on this insight, we develop a new active learning algorithm and implement it in a tool called Socrates, which automatically synthesizes informative multiple-choice queries for program disambiguation. We evaluate Socrates across four domains spanning both symbolic and neurosymbolic settings and show that it produces intuitive, easy-to-answer queries and achieves efficient convergence. Most importantly, Socrates identifies the intended program more reliably than existing methods, while maintaining competitive runtime performance.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p161-p doi:10.1145/3808279

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)
We introduce Kuiper, a language for safe and verified efficient CPU/GPU programming embedded as an extensible library within the F* dependently typed language. We rely on F*’s support for dependent types and its associated Pulse concurrent separation logic to develop a program logic in which to prove CPU/GPU programs safe, data-race free, and functionally correct. Our model of the GPU includes several intricacies, including the memory hierarchy, kernel launches, and synchronization within a single comprehensive framework. To do so, we extend the Pulse program logic with a novel notion of located resources and a new connective to structure reasoning about massively parallel programs, and present new proof rules to lift the per-thread view of GPU kernels to an end-to-end correctness specification.
We have used Kuiper to program and prove correct a variety of GPU kernels, including full functional correctness proofs of an optimized matrix multiplication using two levels of block tiling and tensor cores. In doing so, we have developed a range of libraries to enable programs and proofs at a high level of abstraction but without imposing any runtime overhead. These allow Kuiper programs to be polymorphic (over types, operations, memory layout, and more) and compile to efficient, specialized CUDA code, while enabling a novel form of verified auto-tuning. Our experimental evaluation confirms that Kuiper programs match the performance of their handwritten CUDA counterparts and are competitive with closed source, state-of-the-art kernels in cuBLAS.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p173-p doi:10.1145/3808280

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)
Matching regexes (regular expressions) is a common problem in many areas of computer science, with requirements on high speed and robust performance. Regexes with backreferences allow one to express certain patterns (even beyond regular) concisely, however, since the matching is usually done by backtracking, the matching speed can degrade to a degree that constitutes a service failure or a security threat. To facilitate high-speed matching of such regexes, we propose register set automata (RSAs), an extension of register automata where registers can contain sets of symbols (from a potentially infinite alphabet) and the following operations are supported: adding input values to registers, merging or clearing registers, and testing whether a register contains a value. We show that a large class of register automata can be transformed into deterministic RSAs, which can serve as a basis for fast matching of a family of regexes with single-letter capture groups and backreferences. We also give a derivative-based algorithm for transforming a large class of regexes with backreferences to register automata and show that the time complexity of matching is linear and quadratic to the length of the input for finite and infinite alphabets respectively. Our prototype implementation of a regex matcher shows that our approach can significantly improve the robustness of state-of-the-art regex matchers on regexes with backreferences. We also study the theoretical properties of the model and show that the emptiness problem for RSAs is decidable and complete for the F_ω class and that RSAs are incomparable in expressive power to other popular automata models over data words.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p181-p doi:10.1145/3808281

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)
Binary size reduction is an increasingly important optimization objective for compilers, especially in the context of mobile applications and resource-constrained embedded devices. In such domains, binary size often takes precedence over compilation time. One emerging technique that has been shown effective is function merging, where multiple similar functions are merged into one, thereby eliminating redundancy. The state-of-the-art approach to perform the merging, due to Rocha et al. [CGO 2019, PLDI 2020], is based on sequence alignment, where functions are viewed as linear sequences of instructions that are then matched in a way maximizing their alignment.
In this paper, we consider a significantly generalized formulation of the problem by allowing reordering of branches within each function, subsequently allowing for more flexible matching and better merging. We show that this makes the problem NP-hard, and thus we study it through the lens of parameterized algorithms and complexity, where we identify certain parameters of the input that govern its complexity. We look at two natural parameters: the branching factor and nesting depth of input functions.
Concretely, our input consists of two functions F₁, F₂, where each F_i has size n_i, branching factor b_i, and nesting depth d_i. Our task is to reorder the branches of F₁ and F₂ in a way that yields linearizations achieving the maximum sequence alignment. Let n=max(n₁, n₂), and define b, d similarly. Our results are as follows:
• A simple algorithm running in time 2^O(bd) n², establishing that the problem is fixed-parameter tractable (FPT) with respect to all four parameters b₁,d₁, b₂, d₂.
• An algorithm running in time 2^O(bd₂) n⁷, showing that even when one of the functions has an unbounded nesting depth, the problem remains in FPT.
• A hardness result showing that the problem is NP-hard even when constrained to constant d₁, b₂, d₂.
To the best of our knowledge, this is the first systematic study of function merging with branch reordering from an algorithmic or complexity-theoretic perspective.

Publisher's Version Article: pldi26main-p183-p doi:10.1145/3808282

A Compiler for Fused Relational Operations on Multisets
James Dong and Fredrik Kjolstad
(Stanford University, USA)
We describe a comprehensive compilation approach for relational algebra, centered on an abstract loop-based intermediate representation (IR) that can express fused implementations of relational algebra operators on both sets and multisets. The loops are abstracted away from physical data structures thus making it easier to optimize. We show how to lower relational algebra query plan trees to the IR, including the complex operators that are used in production database systems, such as outer joins, non-equi joins, and differences. We then show how to compile this IR to efficient C++ code that co-iterates over the physical data structures present in relational algebra expressions. Finally, we show that our approach is portable across data structures. Since our approach can fuse across disparate operators, it achieves a 3.8x speedup (0.8--12.1x) compared to Hyper on selected LSQB benchmarks and worst-case optimal triangle queries. Our compiler also generates code of high quality: it has similar sequential performance to Hyper on TPC-H with a 1.0x speedup (0.4--4.3x) and is approaching their parallel performance with a 0.6x speedup (0.2--1.8x).

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: pldi26main-p219-p doi:10.1145/3808283

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)
Reasoning about quantum programs remains a fundamental challenge, regardless of the programming model or computational paradigm. Existing verification techniques are insufficient -- even for quantum circuits, a deliberately restricted model that lacks classical control, but still underpins many current quantum algorithms. Many existing formal methods require exponential time and space to represent and manipulate (representations of) assertions and judgments, making them impractical for quantum circuits with many qubits. This paper presents SAQR-QC, a logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits. SAQR-QC has three characteristics: (i) some deliberate loss of precision is built into it; (ii) it has a mechanism to help the accumulated loss of precision during a sequence of reasoning steps remain small; and (iii) every reasoning step is local -- involving just a small number of qubits -- making reasoning scalable. We demonstrate the effectiveness of SAQR-QC via two case studies: the verification of GHZ circuits involving non-Clifford gates, and the analysis of quantum phase estimation -- a core subroutine in Shor's factoring algorithm.

Publisher's Version Article: pldi26main-p228-p doi:10.1145/3808284

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)
Coarse-Grained Reconfigurable Architectures (CGRAs) are a promising and versatile accelerator platform, offering a balance between the performance and efficiency of specialized accelerators and software programmability. However, their full potential is severely hindered by control flow in accelerated kernels, as control flow (e.g., loops, branches) is fundamentally incompatible with the parallel, data-driven CGRA fabric. Prior strategies to resolve this mismatch in CGRA kernel acceleration are either inefficient, sacrificing performance for generality, or lack generality due to the difficulty of adapting them across different execution models. Thus, a general and unified solution for efficient CGRA kernel acceleration remains elusive.
This paper introduces NEURA, a unified and retargetable compilation framework that systematically resolves the control-dataflow mismatch in CGRAs. NEURA's core innovation is a novel, pure dataflow intermediate representation (IR) built on a predicated type system. In this IR, control contexts are embedded as a predicate within each data, making control an intrinsic property of data. This mechanism enables NEURA to systematically flatten complex control flow into a single unified dataflow graph. This unified representation decouples kernel representation from hardware, empowering NEURA to retarget diverse CGRAs with different execution models and microarchitectural features. When targeted to a high-performance spatio-temporal CGRA, NEURA delivers a 2.20x speedup on kernel benchmarks and up to 2.71x geometric mean speedup on real-world applications over state-of-the-art (SOTA) high-performance baselines. It also provides a competitive solution against the SOTA low-power CGRA when retargeted to a spatial-only CGRA. NEURA is open-source and available at https://github.com/coredac/neura.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p234-p doi:10.1145/3808285

SSA without Dominance for Higher-Order Programs
Roland Leißa and Johannes Max Griebler
(University of Göttingen, Germany)
Dominance is a fundamental concept in compilers based on static single assignment (SSA) form. It underpins a wide range of analyses and transformations and defines a core property of SSA: every use must be dominated by its definition. We argue that this reliance on dominance has become increasingly problematic—both in terms of precision and applicability to modern higher-order languages. First, control flow overapproximates data flow, which makes dominance-based analyses inherently imprecise. Second, dominance is well-defined only for first-order control-flow graphs (CFGs). More critically, higher-order programs violate the assumptions underlying SSA and classic CFGs: without an explicit CFG, the very notion that all uses of a variable must be dominated by its definition loses meaning.
We propose an alternative foundation based on free variables. In this view, 𝜙-functions and function parameters directly express data dependencies, enabling analyses traditionally built on dominance while improving precision and naturally extending to higher-order programs. We further present an efficient technique for maintaining free-variable sets in a mutable intermediate representation (IR). For analyses requiring additional structure, we introduce the nesting tree—a relaxed analogue of the dominator tree constructed from variable dependencies rather than control flow.
Our benchmarks demonstrate that the algorithms and data structures presented in this paper scale log-linearly with program size in practice.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p239-p doi:10.1145/3808286

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)
A key feature in trusted computing is attestation, which allows encapsulated components (enclaves) to prove their identity to (local or remote) distrusting components. Reasoning about software that uses the technique requires tracking how trust evolves after successful attestation. This process is security-critical and non-trivial, but no existing formal verification technique supports modular reasoning about attestation of enclaves and their clients, or proving end-to-end properties for systems combining trusted, untrusted and attested code.
We contribute Cerisier, the first program logic for modular reasoning about trusted, untrusted and attested code, fully mechanized in the Iris separation logic and the Rocq Prover. We formalize a recent proposal, CHERI-TrEE, to extend capability machines with enclave primitives, as an extension to the Cerise capability machine and program logic. Our program logic comes with a universal contract for untrusted code, which captures both capability safety and local enclave attestation. Like Cerise, this universal contract is phrased in terms of a logical relation defining capabilities' authority. We demonstrate Cerisier by proving end-to-end properties for three representative applications of trusted computing: secure outsourced computation, mutual attestation and a modeled trusted sensor component.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p266-p doi:10.1145/3808287

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)
Abstract semantics has proven to be instrumental for accelerating search-based program synthesis, by enabling the sound pruning of a set of incorrect programs (without enumerating them). One may expect faster synthesis with increasingly finer-grained abstract semantics. Unfortunately, to the best of our knowledge, this is not the case, yet. The reason is because, as abstraction granularity increases -- while fewer programs are enumerated -- pruning becomes more costly. This imposes a fundamental limit on the overall synthesis performance, which we aim to address in this work.
Our key idea is to introduce an offline presynthesis phase, which consists of two steps. Given a DSL with abstract semantics, the first semantics modeling step constructs a tree automaton A for a space of inputs -- such that, for any program P and for any considered input I, A has a run that corresponds to P's execution on I under abstract semantics. Then, the second step builds an oracle O for A. This O enables fast pruning during synthesis, by allowing us to efficiently find exactly those DSL programs that satisfy a given input-output example under abstract semantics.
We have implemented this presynthesis-based synthesis paradigm in a framework, Foresighter. On top of it, we have developed three instantiations for SQL, string transformation, and matrix manipulation. All of them significantly outperform prior work in the respective domains.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p272-p doi:10.1145/3808288

Virtualizing Continuations
Cong Ma, Jonghyun Jung, and Yizhou Zhang
(University of Waterloo, Canada)
Effect handlers and multishot continuations are powerful abstractions for managing control flow; together, they offer concise and modular ways to express and handle nondeterminism, randomness, and more. However, implementing multishot continuations in the presence of stack-allocated lexical resources—lexical effect handlers in particular—is challenging, since stack copying invalidates references to these resources.
We present a novel implementation strategy for lexical effect handlers that fully supports multishot continuations. The key idea is to virtualize the stack space used by continuations. Each stack-allocated handler instance is assigned a virtual address, and all effect invocations through these virtual addresses are mediated by an address translation mechanism. A software-based memory management unit in the runtime system performs these translations efficiently, exploiting the lexical scoping discipline of effect handlers.
We capture the essence of our approach via a new operational semantics for lexical effect handlers and prove it correct with respect to the standard semantics. We also implement it in a compiler and runtime system. Compared to prior languages with lexical effect handlers, our implementation increases expressivity by fully supporting multishot continuations—and, as a happy consequence, unlocks significant performance gains by enabling parallel execution of multishot continuations.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p273-p doi:10.1145/3808289

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)
To achieve peak performance on modern GPUs, one must balance two frames of mind: issuing instructions to individual threads to control their behavior, while simultaneously tracking the convergence of many threads acting in concert to perform collective operations like Tensor Core instructions. The tension between these two mindsets makes modular programming error prone. Functions that encapsulate collective operations, despite being called per-thread, must be executed cooperatively by groups of threads.
In this work, we introduce Prism, a new GPU language that restores modularity while still giving programmers the low-level control over collective operations necessary for high performance. Our core idea is typed perspectives, which materialize, at the type level, the granularity at which the programmer is controlling the behavior of threads. We describe the design of Prism, implement a compiler for it, and lay its theoretical foundations in a core calculus called Bundl. We implement state-of-the-art GPU kernels in Prism and find that it offers programmers the safety guarantees needed to confidently write modular code without sacrificing performance.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable ACM SIGPLAN Distinguished Paper Award Article: pldi26main-p277-p doi:10.1145/3808290

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)
We study the estimation problem for concurrent programs: given a bounded program P, estimate the number of maximal Mazurkiewicz trace–equivalence classes induced by its interleavings. This quantity informs two practical questions for enumeration-based model checking: how long a model checking run is likely to take, and what fraction of the search space has been covered so far. We first show the counting problem is #P-hard even for restricted programs and, unless P = NP, inapproximable within any subexponential factor in polynomial time. Thus, we cannot expect efficient exact or randomized approximation algorithms. We give a Monte Carlo approach to find a polynomial-time unbiased estimator: we convert a stateless optimal DPOR algorithm into an unbiased estimator by viewing its exploration as a bounded-depth, bounded-width, tree whose leaves are the maximal Mazurkiewicz traces. A classical estimator by Knuth, when run on this tree, gives an unbiased estimation. In order to control the variance of the estimation, we apply stochastic enumeration by maintaining a small population of partial paths per depth whose evolution is coupled. We have implemented our estimator in the JMC model checker and evaluated it on shared-memory benchmarks. We find that with modest budgets, our estimator yields stable estimates—typically within a 20% band—within a few hundred trials, even when the state space has 10⁵–10⁶ classes. We also show how the same machinery estimates model-checking cost by weighting all explored traces, not only the maximal ones. Our algorithms provide the first provable poly-time unbiased estimators for counting Mazurkiewicz traces.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p279-p doi:10.1145/3808291

Analyzing Bytes: Pre-Disassembly Static Binary Analysis
Huan Nguyen, Soumyakant Priyadarshan, Chencheng Jiang, and R. Sekar
(Google, USA; Stony Brook University, USA)
Binary code analysis plays a central role in numerous applications in software security, performance optimization, reverse engineering, and so on. Existing techniques need to first disassemble binaries into functions in assembly code before an analysis can be performed. However, disassembly and function identification have proven to be major challenges for complex variable-length instruction sets such as the x86. A recent trend has been to use static analysis to improve the accuracy of these tasks. This raises a chicken-and-egg problem: a disassembly is needed for static analysis, but a static analysis is needed for accurate disassembly! We overcome this problem by developing a novel static analysis approach that can operate before committing to a disassembly. Our analysis operates on the output of exhaustive disassembly that considers each possible offset in a binary as an instruction, and constructs what is known as a super-set control-flow graph (CFG). The central technical challenge in analyzing this CFG is that it mixes legitimate instructions with unintended ones, causing analysis results from invalid code paths to pollute legitimate ones. To overcome this challenge, we begin with a key new insight that if we focus on backward analyses, we can ensure accuracy of analysis results at intended instructions even though we have no idea where these intended instructions are! Moreover, our analysis operates in time that is linear in the size of the binary. Specifically, in O(n) total time, it yields analysis results for every one of the n offsets in an n-byte binary. For this task, it is orders of magnitude faster than previous techniques, as the previous techniques typically need to repeat the analysis many times.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p284-p doi:10.1145/3808292

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)
Consensus algorithms play a central role in many distributed systems, including blockchains. The most practical consensus algorithms are based on the partial synchrony model. While partially synchronous protocols are relatively simple, they cannot maintain liveness when the message delivery latency is uncertain. Asynchronous protocols do not rely on bounded latency to maintain liveness, but they are much more difficult to understand and implement, being usually described as a composition of several layers of algorithms. Moreover, due to the FLP impossibility theorem, they only provide probabilistic liveness guarantees. These factors make the correctness of asynchronous protocols challenging to verify, and there have been liveness bugs in these protocols that remain unnoticed for years.
We introduce SureDistrib, a formal framework for specifying and verifying probabilistic safety and liveness properties of asynchronous distributed protocols. Our framework supports specifying probabilistic algorithms that depend on other probabilistic functionalities, such as binary agreement algorithms depending on common coins. We define refinement relations for such systems, and prove composition lemmas that replace the underlay functionality with an implementation, so that the composed system refines the original system with an abstract underlay. Based on our framework, we give the first mechanized proof that an asynchronous byzantine fault-tolerant binary agreement algorithm terminates with probability 1 ("almost-sure termination").

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p304-p doi:10.1145/3808293

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)
During chip development, engineers must target different technologies, such as simulation and various ASIC and FPGA technologies. Conventionally, they split parts of the code (e.g., memories) into separate technology-specialized blocks implementing the same high-level behavior. This leads to brittle code, with multiple but subtly different blocks describing the same semantic behavior, harming verification, agility, and extensibility.
We propose fungible memories, an HDL-level "write once, map anywhere" memory abstraction with rich enough semantics to automatically target all relevant technologies using a single generic interface. We incorporate fungible memories into a compiler called Memo. For designs without a specific technology mapping, we also present a memory decompiler which lifts memories from an existing gate-level design to Memo, enabling automated technology re-targeting, which is a holy grail for digital designers. We present a structure-aware equality saturation technique which scales to netlists with millions of cells and identifies memories that the state of the art cannot. We demonstrate that Memo effectively targets backends across different technology platforms (simulation, ASIC, and FPGA) over a suite of representative designs, including a RISC-V multicore SoC.

Publisher's Version Published Artifact Artifacts Available Article: pldi26main-p315-p doi:10.1145/3808294

Heterogeneous Dynamic Logic: Provability Modulo Program Theories
Samuel Teuber, Mattias Ulbrich, André Platzer, and Bernhard Beckert
(KIT, Germany)
Formally specifying, let alone verifying, properties of systems involving multiple programming languages is inherently challenging. We introduce Heterogeneous Dynamic Logic (HDL), a framework for combining reasoning principles from distinct (dynamic) program logics in a modular and compositional way. HDL mirrors the architecture of satisfiability modulo theories (SMT): Individual dynamic logics, along with their calculi, are treated as dynamic theories that can be combined to reason about heterogeneous systems whose components are verified using different program logics. HDL provides two key operations: Lifting extends an individual dynamic theory with new program constructs (e.g., the havoc operation or regular programs) and automatically augments its calculus with sound reasoning principles for the new constructs; and Combination enables cross-language reasoning in a single modality via Heterogeneous Dynamic Theories, facilitating the reuse of existing proof infrastructure. By lifting combined theories with regular programs, we obtain heterogeneous control structures that allow us to reason about intertwined cross-language behavior. We formalize dynamic theories, their lifting and combination, and prove the soundness of all proof rules in Isabelle. We also introduce a proof rule combining deductive DL-based reasoning with reasoning principles from Kleene Algebras with Tests. Furthermore, we prove relative completeness theorems for lifting and combination: Under usual assumptions, reasoning about lifted or combined theories is no harder than reasoning about the constituent dynamic theories and their common first-order structure (i.e., the data theory). We demonstrate HDL's value by verifying an automotive case study where a Java controller (formalized in Java dynamic logic) steers a plant model (formalized in differential dynamic logic).

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p324-p doi:10.1145/3808295

SuperDP: Differential Privacy Refutation via Supermartingales
Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, and Đorđe Žikelić
(IST Austria, Austria; Singapore Management University, Singapore)
Differential privacy (DP) has established itself as one of the standards for ensuring privacy of individual data. However, reasoning about DP is a challenging and error-prone task, hence methods for formal verification and refutation of DP properties have received significant interest in recent years. In this work, we present a novel method for automated formal refutation of є-DP. Our method refutes є-DP by searching for a pair of inputs together with a non-negative function over outputs whose expected value on these two inputs differs by a significant amount. The two inputs and the non-negative function over outputs are computed simultaneously, by utilizing upper expectation supermartingales and lower expectation submartingales from probabilistic program analysis, which we leverage to introduce a sound and complete proof rule for є-DP refutation. To the best of our knowledge, our method is the first method for є-DP refutation to offer the following four desirable features: (1) it is fully automated, (2) it is applicable to stochastic mechanisms with sampling instructions from both discrete and continuous distributions, (3) it provides soundness guarantees, and (4) it provides semi-completeness guarantees. Our experiments show that our prototype tool SuperDP achieves superior performance compared to the state of the art and manages to refute є-DP for a number of challenging examples collected from the literature, including ones that were out of the reach of prior methods.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p328-p doi:10.1145/3808296

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)
GPU hardware implements a SIMT execution model, where small groups of threads, called subgroups (or warps in CUDA), execute synchronously. Languages expose this through high-performance subgroup-level APIs. However, providing precise subgroup semantics in languages is challenging, as compilers may transform the program, potentially disrupting source-level synchronous behavior even if the hardware is synchronous. As a result, no GPU programming language provides rigorous semantics for subgroup execution.
In this work, we present SIMT-Step, a formal and flexible operational semantics for subgroup execution. At its core is a new semantic object, dynamic basic blocks, which enables precise specification of converged subgroup execution. SIMT-Step then provides flexibility for the execution of instructions, which can be collective, synchronous, or independent. We propose several candidate instantiations of SIMT-Step and design a suite of idiomatic tests to distinguish them, highlighting counter-intuitive behavior that arises under relaxed variants. We implement SIMT-Step in TLA+ and validate the behavior of the idiomatic tests, all of which can be verified in under one second. Finally, to investigate how closely SIMT-Step models real-world GPU behavior, we conduct a large fuzzing campaign, spanning nine GPUs and seven vendors. Our results show that, despite hesitancy to provide guarantees in official specifications, most GPUs exhibit strongly synchronous behavior. Combined, these contributions provide both a theoretical foundation and practical tools for reasoning about subgroup semantics in GPU programming languages.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p337-p doi:10.1145/3808297

Neptune: Advanced ML Operator Fusion for Locality and Parallelism on GPUs
Yifan Zhao, Egan Johnson, Prasanth Chatarasi, Vikram Adve, and Sasa Misailovic
(University of Illinois Urbana-Champaign, USA; IBM Research, USA)
Operator fusion has become a key optimization for deep learning, which combines multiple deep learning operators to improve data reuse and reduce global memory transfers. However, existing tensor compilers struggle to fuse complex reduction computations involving loop-carried dependencies, such as attention mechanisms.
This paper introduces Neptune, a tensor compiler for advanced operator fusion for sequences of reduction operators. Neptune presents a new approach for advanced operator fusion, which intentionally breaks some existing dependencies and compensates by constructing algebraic correction expressions that allow the kernel to produce the correct result. Applying Neptune’s advanced operator fusion to a plain attention operator generates operators equivalent to FlashAttention and FlashDecoding.
On ten attention-based benchmarks, Neptune, starting from a plain attention code and a high-level scheduling template, outperforms existing compilers like Triton, TVM, and FlexAttention, including Triton-based implementations of FlashAttention. Across four different GPU architectures from NVIDIA and AMD, Neptune-generated kernels have an average speedup of 1.35× over the next best alternative, with up to 2.65 × speedup on Nvidia GPUs and up to 3.32 × on AMD GPUs, demonstrating its effectiveness for deep learning workloads.

Publisher's Version Published Artifact Artifacts Available Article: pldi26main-p347-p doi:10.1145/3808298

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)
Equality saturation (eqsat) is a program optimization technique that uses syntax-based term rewriting to simultaneously explore many possible optimizations of a program, storing equivalent programs efficiently in a data structure called an e-graph. By exploring optimizations simultaneously, eqsat mitigates the phase ordering problem, where the order of optimizations significantly affects quality of results. Eqsat is especially promising for Electronics Design Automation (EDA), whose tools suffer from phase ordering. Previous eqsat-for-EDA efforts have focused on single tool stages; while they demonstrate significant benefits within a stage, they do not address phase ordering between stages. When we investigated the reason for their limited scope, we found that previous works struggle to implement an efficient hardware representation useful in both high-level (e.g. arithmetic optimization) and low-level (e.g. logic synthesis) tasks. The root issue is that such a representation must maintain equivalences between the high- and low-level portions of the language. While these equalities are conceptually simple—e.g., two high-level bitvectors are equal if they contain the same low-level bits—maintaining them using syntax-based rewrites alone proves inefficient in modern eqsat engines. In response, this paper makes two contributions. First, we introduce semantic e-graphs, an enhancement to e-graphs that improves performance of a narrow but highly useful class of semantics-based equalities. Second, we present Nextmap, a new eqsat-based hardware optimization engine whose representation uses semantic e-graphs to efficiently bridge high- and low-level hardware expressions. As a result, Nextmap simultaneously runs more EDA stages than previous eqsat-based works, more effectively mitigating phase ordering and reaching previously inaccessible optimizations. Compared with open-source and commercial tools, Nextmap provides competitive quality of results on a range of designs.

Publisher's Version Published Artifact Artifacts Available Article: pldi26main-p348-p doi:10.1145/3808299

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)
Static analysis has profoundly improved software quality over the past decades, evolving from compiler-integrated optimizations and simple linting to sophisticated analyses for bug detection, security, and program understanding. In contrast, static analysis for hardware remains underexploited, resembling the early state of software analysis. Most existing hardware static analyses are confined to compiler optimizations and linting, lacking the sophistication needed to uncover complex design flaws. Furthermore, we observe that many hardware bugs reported in recent literature could have been identified by sophisticated static analyses that account for hardware-specific semantics and data flow; however, such bug detection analyses are absent today. To exploit the untapped potential of sophisticated hardware analysis, we present a series of bug detection analyses for Verilog, the predominant hardware description language (HDL). Moreover, these analyses are built upon our fundamental analyses that capture essential hardware-specific characteristics---such as bit-vector arithmetic, register synchronization, and digital component concurrency---and enable the examination of hardware data and control flows. Together, these analyses form a well-organized analysis suite with a modular design, in which diverse fundamental analyses combine to support bug detection, hardware understanding, and other potential clients. To implement these analyses, we further offer dedicated infrastructure, including a Verilog front end, an intermediate representation (IR) for analysis, and an analysis manager. To validate the utility of our analyses, we applied them to real-world hardware projects. Unlike software, real-world hardware projects tend to contain fewer but harder-to-detect bugs, as they typically undergo extensive simulation and rigorous verification to prevent the prohibitive costs of hardware defects. Despite this, our preliminary experimental results are highly promising: applying these proposed analyses to popular real-world Verilog projects (averaging 1.5K+ GitHub stars) uncovered nine previously unknown bugs, all confirmed by developers; moreover, we successfully identified a total of 18 bugs beyond the capabilities of existing static analyses for Verilog bug detection (i.e., linters). These results underscore the transformative potential of sophisticated static analysis in hardware design. Our analysis suite and infrastructure are also highly reusable: on average, each bug-detection client built on our analysis suite requires about 270 LoC, compared to 5,700 LoC when developed from scratch. By open-sourcing the entire system, involving substantial engineering effort (100K+ LoC), we aim to encourage further innovation and applications of sophisticated static analysis for hardware, hopefully fostering a similarly vibrant ecosystem that software analysis enjoys.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p362-p doi:10.1145/3808300

Bridging Coverage and Confidence: Reliable Static False Alarm Elimination via Input-Agnosticity
Jiayi Wang, Yu Wang, Linzhang Wang, and Ke Wang
(Nanjing University, China)
Static analysis is a foundational technique for detecting software defects, yet it notoriously suffers from high false positive rates. Prior efforts to reduce false positives via model checking, symbolic execution, dynamic analysis, testing, or machine learning either fail to scale or mistakenly eliminate real defects.
This paper presents RICAN, a novel approach that leverages dynamic testing to reliably eliminate false alarms in static analysis. The key insight behind RICAN is the concept of input-agnosticity: if the validity of an alarm is independent of program inputs along each execution path, then once all such paths from the program entry to the alarm site have been exercised by tests without triggering the alarmed bug, the alarm can be safely classified as a false positive. To realize this insight, RICAN uses data-dependence analysis to identify input-agnostic alarms among all reported alarms. However, validating even input-agnostic alarms requires exploring all feasible paths, which is generally infeasible. To address this, RICAN computes a necessary set of paths by identifying only those branches and loops that may influence the alarm's validity. Finally, RICAN eliminates false alarms using existing dynamic testing and post-directed fuzzing to cover these critical paths.
We evaluate RICAN on six real-world open-source projects. Our experiments show that RICAN can reliably eliminate 1,313 (45.09%) false positives across 2,912 double free, use-after-free, and null pointer dereference alarms, while incurring negligible overhead. Our user studies further demonstrate that RICAN reduces the manual effort required for alarm inspection by over 70% on average and helps programmers find bugs more quickly and accurately, highlighting its practical usefulness in real-world static analysis.

Publisher's Version Published Artifact Artifacts Available Article: pldi26main-p363-p doi:10.1145/3808301

Optimism in Equality Saturation
Russel Arbore, Alvin Cheung, and Max Willsey
(University of California at Berkeley, USA)
Equality saturation is a program optimization technique based on non-destructive rewriting and a form of abstract interpretation called e-class analysis. Existing e-class analyses are pessimistic and therefore typically imprecise when analyzing cyclic programs, such as those in SSA form. We show that a straightforward optimistic variant of e-class analysis can result in unsoundness, due to a subtlety in how e-graphs represent programs. We propose an abstract interpretation algorithm that circumvents this issue and can optimistically analyze e-graphs during equality saturation. This results in a unified algorithm for optimistic analysis and non-destructive rewriting. We implement a prototype abstract interpreter and equality saturation tool for SSA programs. Our tool exhibits precision improvements over pure abstract interpretation (without rewriting) and pessimistic e-class analysis on example programs. Additionally, its performance is comparable to existing abstract interpretation and e-class analysis techniques.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p376-p doi:10.1145/3808302

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)
We introduce a type system that provides strong types for exception tracking in ML-style languages. Our type system employs a rich notion of row polymorphism and subtyping to ensure backwards compatibility, making sure that code without exception tracking continues to work and can be generalized gracefully to support exception tracking. We study the safety and abstraction guarantees of our type system, in particular the role of local exceptions for data abstraction. We formulate these claims using binary logical relations in a novel relational separation logic for exceptions, an independent contribution of this paper. We support a realistic subset of features from ML-style languages, such as extensible variant types, local exceptions, and concurrency. We exercise our type system and logic on a number of challenging examples taken from the OCaml standard library, from one of Jane Street's OCaml libraries, and from Filinski's PhD thesis. All our results are mechanized in the Rocq prover using Iris.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p378-p doi:10.1145/3808303

Verifying Array Properties in Pure Data-Parallel Programs
Nikolaj Hey Hinnerskov, Robert Schenck, and Cosmin Oancea
(University of Copenhagen, Denmark; Northeastern University, USA)
In functional data-parallel programs, index array computations are separated into sequences of bulk-parallel operators—map, prefix sum, scatter—and used to gather or scatter data array elements, thus determining data array properties. This programming style is problematic for general-purpose verification frameworks (e.g., Dafny, F*, Liquid Haskell), which are flexible and powerful, but require verbose annotations and non-trivial user proofs, making them inaccessible to non-experts. We present a compiler approach to verifying array properties with high automation, aimed at making verification of data-parallel programs more accessible to users without verification expertise. We support a small but powerful predefined set of properties—equivalence, range, injectivity, bijectivity, monotonicity, filtering, partitioning—that enable the compiler to (automatically) reason at a higher level of abstraction. We evaluate our approach on challenging applications with non-linear indexing, including graph algorithms, Cooley-Tukey FFT, filtering, multi-way partitioning, and flattened irregular nested parallel programs that are difficult to verify, such as batch operations on arrays of different sizes.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p388-p doi:10.1145/3808304

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)
We consider the problem of verification modulo tested library contracts as a step towards automating the verification of client programs that use complex libraries. We formulate this problem as the synthesis of modular contracts for the library methods used by the client that are adequate to prove the client correct, and that also pass the scrutiny of a testing engine that tests the library against these contracts. We also consider a new form of method contracts called contextual contracts that arise in this setting that hold in the context of the client program, and can often be simpler and easier to infer than classical modular contracts. We provide a counterexample-guided learning framework to solve this problem, in which the synthesizer interacts with a constraint solver as well as the testing engine in order to infer adequate modular/contextual method contracts and inductive invariants for the client. The main synthesis engines we use are generalizing CHC solvers that are realized using ICE learning algorithms. We realize this framework in a tool called Dualis and show its efficacy on benchmarks where clients call large libraries.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p396-p doi:10.1145/3808305

Soteria: Efficient Symbolic Execution as a Functional Library: Perhaps You Should Write Your Own Symbolic Execution Engine!
Sacha-Élie Ayoun, Opale Sjöstedt, and Azalea Raad
(Imperial College London, UK; Soteria Tools, UK)
Symbolic execution (SE) tools often rely on intermediate languages (ILs) to support multiple programming languages, promising reusability and efficiency. In practice, this approach introduces trade-offs between performance, accuracy, and language feature support. We argue that building SE engines directly for each source language is both simpler and more effective. We present Soteria, a lightweight OCaml library for writing SE engines in a functional style, without compromising on performance, accuracy or feature support. Soteria enables developers to construct SE engines that operate directly over source-language semantics, offering configurability, compositional reasoning, and ease of implementation. Using Soteria, we develop Soteria-Rust, the first Rust SE engine supporting TreeBorrows (the intricate aliasing model of Rust), and Soteria-C, a compositional SE engine for C. Both tools are competitive with or outperform state-of-the-art tools such as Kani, Infer.Pulse, CBMC and Gillian-C in performance and the number of bugs detected. We formalise the theoretical foundations of Soteria and prove its soundness, demonstrating that sound, efficient, accurate, and expressive SE can be achieved without the compromises of ILs.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p402-p doi:10.1145/3808306

A Categorical Basis for Robust Program Analysis
Zachary Kincaid and Shaowei Zhu
(Princeton University, USA)
Users of program analyses expect that results change predictably in response to changes in their programs, but many analyses do not ensure such robustness. This paper introduces a theoretical framework that provides a unified language to articulate robustness properties. We adopt a categorical view in which programs and their properties form a category, and robust analyses are characterized as structure-preserving functors. A diverse range of robustness properties---e.g., invariance under variable renaming and monotonicity---arise from instantiating the category's arrows accordingly.
Beyond formulating the meaning of robustness, this paper provides methods for achieving it. The first is a general recipe for designing robust analyses, by lifting a sound and robust analysis from a restricted (sub-Turing) model of computation to a sound and robust analysis for general programs. This recipe demystifies the design of several existing loop summarization and termination analyses by showing they are instantiations of this general recipe, and furthermore elucidates their robustness properties. The second is a characterization of a sense in which an algebraic program analysis is robust, provided that it is comprised of robust operators. In particular, we show that such analyses behave predictably under common refactoring patterns, such as variable renaming and loop unrolling.

Publisher's Version Article: pldi26main-p410-p doi:10.1145/3808307

SAIL: Sound Abstract Interpreters with LLMs
Qiuhan Gu, Avaljot Singh, and Gagandeep Singh
(University of Illinois Urbana-Champaign, USA)
How to construct globally sound abstract interpreters to safely approximate program behaviors remains a bottleneck in abstract interpretation. In this paper, we show the potential of using state-of-the-art LLMs to automate this tedious process. Focusing on the neural network verification area, we synthesize non-trivial sound abstract transformers across diverse abstract domains using LLMs to search within infinite space from scratch. We formalize the synthesis task as a constrained optimization problem, for which we design a novel mathematically grounded cost function that measures the degree of unsoundness of each generated candidate transformer, while enforcing hard syntactic and semantic validity constraints. Building on this formulation, we introduce SAIL, a novel unified framework that combines model generation, syntactic and semantic validation, and cost-function-based refinement to synthesize globally sound abstract transformers. Evaluation results show that SAIL not only matches the performance of manually designed transformers, but also is able to synthesize sound and high-precision transformers that do not exist in the literature for complex non-linear operators.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p429-p doi:10.1145/3808308

Intrinsically Correct Algorithms and Recursive Coalgebras
Cass Alexandru, Henning Urbat, and Thorsten Wißmann
(RPTU Kaiserslautern-Landau, Germany; Radboud University Nijmegen, Netherlands; Friedrich-Alexander University Erlangen-Nürnberg, Germany)
Recursive coalgebras provide an elegant categorical tool for modelling recursive algorithms and analysing their termination and correctness. By considering coalgebras over categories of suitably indexed families, the correctness of the corresponding algorithms follows intrinsically just from the type of the computed maps. However, proving recursivity of the underlying coalgebras is non-trivial, and proofs are typically ad hoc. This layer of complexity impedes the formalization of coalgebraically defined recursive algorithms in proof assistants. We introduce a framework for constructing coalgebras which are intrinsically recursive in the sense that the type of the coalgebra guarantees recursivity from the outset. Our approach is based on the novel concept of a well-founded functor on a category of families indexed by a well-founded relation. We show as our main result that every coalgebra for a well-founded functor is recursive, and demonstrate that well-known techniques for proving recursivity and termination such as ranking functions are subsumed by this abstract setup. We present a number of case studies, including Quicksort, the Euclidian algorithm, and CYK parsing. Both the main theoretical result and selected case studies have been formalized in Cubical Agda.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p434-p doi:10.1145/3808309

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)
Garbage collection (GC) remains a desirable yet elusive goal in unmanaged languages like C/C++ and Rust, where concurrent memory reclamation must be achieved without compiler or runtime support. Existing techniques face fundamental trade-offs among efficiency, safety, and ease of integration: tracing collectors like BDWGC incur costly stop-the-world pauses and unsafe conservative scanning, while reference counting schemes like CIRC are safe but introduce high overhead and require manual handling of cyclic data.
We present a safe, efficient, and easy-to-integrate concurrent GC library, revisiting partial tracing (PT), a concept initially conceived by Bacon et al. 22 years ago. PT is a hybrid approach that maintains reference counts for roots, ensuring safety through precise root identification, and traces from objects with non-zero counts, offering ease of integration by handling cyclic garbage. Although PT has historically been considered inefficient due to the high cost of root mutation, we overcome this limitation in two design steps. First, Concurrent Partial Tracing (CPT) introduces phase consensus, enabling concurrent phase coordination without mutator suspension and eliminating most reference-count updates during traversal. Second, Concurrent Deferred Partial Tracing (CDPT) further reduces overhead by replacing atomic root updates with a lightweight, hazard pointer (HP)-based mechanism safeguarded by a phase barrier. We show that CDPT outperforms automatic collectors like BDWGC and CIRC while being comparable to manual schemes like RCU, through both micro-benchmarks on concurrent data structures and a macro-benchmark on Moka, a production cache library.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p438-p doi:10.1145/3808310

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; AWS, USA)
Differential privacy is the standard method for privacy-preserving data analysis. The importance of having strong guarantees on the reliability of implementations of differentially private algorithms is widely recognized and has sparked fruitful research on formal methods. However, the design patterns and language features used in modern DP libraries as well as the classes of guarantees that the library designers wish to establish often fall outside of the scope of previous verification approaches.
We introduce a program logic suitable for verifying differentially private implementations written in complex, general-purpose programming languages. Our logic has first-class support for reasoning about privacy budgets as a separation logic resource. The expressiveness of the logic and the target language allow our approach to handle common programming patterns used in the implementation of libraries for differential privacy, such as privacy filters and caching. While previous work has focused on developing guarantees for programs written in domain-specific languages or for privacy mechanisms in isolation, our logic can reason modularly about primitives, higher-order combinators, and interactive algorithms.
We demonstrate the applicability of our approach by implementing a verified library of differential privacy mechanisms, including an online version of the Sparse Vector Technique, as well as a privacy filter inspired by the popular Python library OpenDP, which crucially relies on our ability to handle the combination of randomization, local state, and higher-order functions. We demonstrate that our specifications are general and reusable by instantiating them to verify clients of our library. All of our results have been foundationally verified in the Rocq Prover.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p444-p doi:10.1145/3808311

Optimal Predicate Pushdown Synthesis
Robert Zhang, Eric Hayden Campbell, Dixin Tang, and Işıl Dillig
(University of Texas at Austin, USA)
Predicate pushdown is a long-standing performance optimization that filters data as early as possible in a computational workflow. In modern data pipelines, this transformation is especially important because much of the computation occurs inside user-defined functions (UDFs) written in general-purpose languages such as Python and Scala. These UDFs capture rich domain logic and complex aggregations and are among the most expensive operations in a pipeline. Moving filters ahead of such UDFs can yield substantial performance gains, but doing so requires semantic reasoning. This paper introduces a general semantic foundation for predicate pushdown over stateful fold-based computations.
We view pushdown as a correspondence between two programs that process different subsets of input data, with correctness witnessed by a bisimulation invariant relating their internal states. Building on this foundation, we develop a sound and relatively complete framework for verification, alongside a synthesis algorithm that automatically constructs optimal pushdown decompositions by finding the strongest admissible pre-filters and weakest residual post-filters. We implement this approach in a tool called Pusharoo and evaluate it on 150 real-world pandas and Spark data-processing pipelines. Our evaluation shows that Pusharoo is significantly more expressive than prior work, producing optimal pushdown transformations with a median synthesis time of 1.6 seconds per benchmark. Furthermore, our experiments demonstrate that the discovered pushdown optimizations speed up end-to-end execution by an average of 2.4× and up to two orders of magnitude.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p463-p doi:10.1145/3808312

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)
Sparse matrix-vector multiplication (SpMV) is a crucial operation in scientific computing, graph analytics, and machine/deep learning. Its performance is highly sensitive to matrix sparsity patterns, necessitating tailored program designs. This paper introduces SparseZETA, an intelligent auto-tuner that generates high-performance, machine-designed SpMV programs by directly mimicking and composing human-expert actions. To efficiently navigate the vast design space, SparseZETA reformulates auto-tuning as a behavior-cloning problem: rather than costly exploration, it directly synthesizes programs by sequentially predicting actions in a one-pass decision-making process, guided by the real-time state of the evolving, partially constructed program designs. A novel self-training mechanism further accelerates the collection of training data for the prediction models. On NVIDIA A100 (and RTX 2080 Ti) GPUs, SparseZETA achieves average speedups of 1.27×–15.66× (1.44×–19.07×) over existing auto-tuners, human-designed programs, and a sparse compiler. SparseZETA substantially reduces the human effort required to design SpMV programs, including sparse format creation and kernel implementation, cutting the design time from days or even months to an average of 82.52ms per matrix via lightweight inference on only one CPU.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p473-p doi:10.1145/3808313

Hybrid Path-Sums for Hybrid Quantum Programs
Christophe Chareton, Jad Issa, Mathieu Nguyen, Nicolas Blanco, and Sébastien Bardin
(CEA List - Université Paris-Saclay, France; Université de Lorraine - CNRS - Inria - LORIA, France)
As quantum computing becomes an emerging reality, designing efficient quantum programming capabilities is becoming more and more important. Particularly, the debugging and validation of quantum programs is of paramount importance, as these programs are by definition hard to test. Static analysis and formal verification methods for quantum programs started to emerge a few years now, yet they often miss hybrid quantum/classical reasoning facilities with, e.g., generic quantum control, classical control and classical computation instructions. In this paper, we lay out the foundations of a framework for the automated formal verification of (full) hybrid quantum programs featuring both classical and quantum control, measurement and hybrid data structures. In particular, we propose: (1) a novel symbolic representation for describing and manipulating sets of hybrid quantum/classical states called Hybrid Path-Sums (HPS); (2) a set of rewriting rules providing a rich mechanism for simplifying and reasoning on these symbolic hybrid states, and (3) a core assertion language to specify equivalence of hybrid quantum programs, the satisfaction of properties on (parts of) hybrid states, and the extraction of probabilistic statements about the program behavior. We prove the correctness of the novel symbolic representation, of its rewriting system and of the specification system. Finally, we propose a full implementation of this framework as a dedicated symbolic execution engine for hybrid programs. We present an evaluation of a set of representative hybrid case-studies from the literature, showcasing the advantage of our approach and its efficiency compared to state-of-the-art solutions.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p478-p doi:10.1145/3808314

Fixed Parameter Tractable Linearizability Monitoring
Zheng Han Lee and Umang Mathur
(National University of Singapore, Singapore)
We study the linearizability monitoring problem, which asks whether a given concurrent history of a data structure is equivalent to some sequential execution of the same data structure. In general, this problem is NP-hard, even for simple objects such as registers. Recent work has identified tractable cases for restricted classes of histories, notably unambiguous and differentiated histories.
We revisit the tractability boundary from a fine-grained, parameterized perspective. We show that for a broad class of data structures — including stacks, queues, priority queues, and maps—linearizability monitoring is fixed-parameter tractable when parameterized by the number of processes. Concretely, we give an algorithm running in time O(c^k · poly(n)), where n is the history size, k is the number of processes, and c is a constant, yielding efficient performance when k is small. Our approach reduces linearizability monitoring to a language reachability problem on graphs, which asks whether a labeled graph admits a path whose label sequence belongs to a fixed language L. We identify classes of languages that capture the sequential specifications of the above data structures and show that language reachability is efficiently solvable on the graph structures induced by concurrent histories.
Our results complement prior hardness results and existing tractable subclasses, and provide a unified algorithmic framework. We implement our approach and demonstrate significant runtime improvements over existing algorithms, which exhibit exponential worst-case behavior.

Publisher's Version Published Artifact Artifacts Available Article: pldi26main-p482-p doi:10.1145/3808315

Incremental Computation 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)
Inference in probabilistic programs generally requires evaluating many possible program executions to find those of high posterior density. To scale inference to large datasets, it is crucial that expensive intermediate results are shared across these many evaluations, rather than recomputed from scratch. This paper presents a new approach to realizing this sharing, based on incremental computation, a technique for efficiently recomputing (deterministic) program outputs when program inputs change. First, we show how expressive probabilistic programs can be compiled to deterministic ones that compute their density functions. Then, building on the incremental λ-calculus, we develop a general technique for compositionally incrementalizing expressive functional programs, and apply it to these densities. The resulting incremental densities can be used to accelerate a broad range of Monte Carlo inference algorithms, including for nonparametric models not well supported by existing systems. Furthermore, our decomposition of incremental density computation into separate density and incrementalization steps allows for modular reasoning about correctness—a key pain point in existing systems, where ad-hoc incrementalization features are a known source of soundness bugs. We develop denotational logical relations arguments for the correctness of each step independently, and implement the approach in a Julia prototype, finding that it leads to asymptotic runtime improvements in the size of the dataset on a range of models and inference algorithms.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p491-p doi:10.1145/3808316

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)
The CCR framework unifies refinement and separation logic to provide ownership-based modular reasoning and transitive incremental reasoning in open settings that involve unverified code. However, when reasoning about function invocations, the reasoning principles available to clients remain confined to pre- and postconditions, which struggle to capture effectful behaviors such as I/O actions or interactions with arbitrary unverified code. This limitation becomes particularly acute in hybrid verification, where a mixture of different verification techniques is applied and some code is never formally verified but instead tested or model-checked.
To overcome this limitation, we introduce imaginary specifications—a novel notion that freely mixes executable code with ownership assertions—and reasoning principles for their use. Through key technical developments, we present CRIS (Contextual Refinement with Imaginary Specifications), a framework that generalizes CCR with support for imaginary specifications. We demonstrate CRIS’s expressiveness and reasoning power through examples involving hybrid verification with unverified code exhibiting arbitrary side effects such as I/O or divergence, with complete mechanization in Rocq.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p498-p doi:10.1145/3808317

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)
We introduce weighted NetKAT, a domain-specific language for modeling and verifying quantitative network properties. The language is parametric on a semiring, enabling the treatment of a wide range of quantities in a uniform way. We provide a denotational semantics and an equivalent operational semantics, the latter based on a novel model of weighted NetKAT automata (WNKA) capturing the stateful behavior of our language. With WNKA, we obtain a class of generic decision procedures for reasoning about quantitative safety and reachability in a fully automatic way, even in the presence of possibly unbounded iteration. We demonstrate the applicability of our framework in a case study using Internet2's Abilene network as the underlying topology.

Publisher's Version Article: pldi26main-p501-p doi:10.1145/3808318

Implementability of Global Distributed Protocols Modulo Network Architectures
Elaine Li and Thomas Wies
(New York University, USA)
Global protocols specify distributed, message-passing protocols from a birds-eye view, and are used as a specification for synthesizing local implementations. Implementability asks whether a given global protocol admits a distributed implementation. We present the first comprehensive investigation of global protocol implementability modulo network architectures. We propose a set of network-parametric Coherence Conditions, and exhibit sufficient assumptions under which it precisely characterizes implementability. We further reduce these assumptions to a minimal set of operational axioms describing insert and remove behavior of individual message buffers. Our reduction immediately establishes that five commonly studied asynchronous network architectures, namely peer-to-peer FIFO, mailbox, senderbox, monobox and bag, are instances of our network-parametric result. We use our characterization to derive optimal complexity results for implementability modulo networks, relationships between classes of implementable global protocols, and symbolic algorithms for deciding implementability modulo networks. We implement the latter in the first network-parametric tool Sprout(A), and show that it achieves network generality without sacrificing performance and modularity.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p510-p doi:10.1145/3808319

Enumerating Ill-Typed Programs for Testing Type Analyzers
Thodoris Sotiropoulos and Zhendong Su
(ETH Zurich, Switzerland)
We propose error enumeration, a method that aims to discover soundness defects in type analyzers by generating ill-typed programs by construction. Given a well-typed program P, it systematically injects type mismatches at all possible program locations to explore ill-typed programs that differ from P by replacing one expression with incompatible ones. The core contributions of our work are: (1) soundly injecting type mismatches even in the presence of type inference and refinements, and (2) enabling practical exploration of large seed programs by pruning the search space. Incomplete type information complicates the injection of type mismatches, as type inference can silently ”repair” the injected error by adjusting inferred types in the surrounding context so that the program still type-checks. We address this by introducing a lightweight, usage-based reasoning technique that recovers missing types of program elements by leveraging the existing type annotations at each element’s use site. This enables the injection of errors that guarantee type incompatibilities at the use sites of variables and other expressions. Finally, to prune the search space, we enumerate only those errors that ultimately lead to comparisons between types with distinct shape characteristics.
We evaluated our implementation, Eris, on (1) three type analyzers integrated into the compilers of Kotlin, Scala, and Groovy, and (2) the Checker Framework, widely used to identify null-related errors in Java programs. Eris has uncovered 64 bugs caused by ill-typed programs: 51 leading to unsoundness, and 13 to compile-time crashes. Further investigation reveals that the majority of the soundness bugs discovered by Eris are triggered under highly complex conditions, where error injection requires (1) specific combinations of actual vs. expected type pairs at deeply-nested program locations, or (2) reasoning about control flow and missing type information, capabilities that lie beyond the scope of existing work.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable ACM SIGPLAN Distinguished Paper Award Article: pldi26main-p517-p doi:10.1145/3808320

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)
Gradient estimation—the task of computing the gradient of the expected value of a probabilistic program—has diverse applications in scientific computing, but is notoriously difficult because of issues such as high-dimensional integration, discrete random choices, and complex stochastic dependencies. This article introduces gradient inference, a new approach to developing sound and efficient gradient estimators for probabilistic programs. Gradient inference rests on a formal reduction from a gradient estimation problem to a closely related probabilistic inference problem, whose solution can be differentiated to obtain a gradient estimator. This inference problem is obtained by applying two powerful statistical operations—coupling and factorization—to the input probabilistic program. Our reduction lets us leverage the rich toolkit of probabilistic inference algorithms to design novel gradient estimators that extend and improve upon existing methods.
We introduce GradInf, a probabilistic programming system that facilitates the sound and automated implementation of gradient inference. GradInf is centered around programmable source-to-source transformations for coupling and factorizing higher-order probabilistic programs, whose soundness is proven in terms of a denotational semantics. Key to our development is the use of information-flow typing to allow random choices in a probabilistic program to be factored out and partially evaluated, which improves our ability to deploy sophisticated probabilistic inference algorithms. The resulting system offers practitioners a principled framework for designing gradient estimators. We apply GradInf to several challenging case studies, showing that it can express prominent gradient estimators from the literature and enables the construction of new state-of-the-art estimators that outperform the best existing baselines.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p518-p doi:10.1145/3808321

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)
Inductive types are a fundamental abstraction mechanism in type theory and proof assistants, supporting the definition of data structures and rich specifications. Nested inductive types extend this mechanism by allowing constructors to use parametric types instantiated with the type being defined (lists or trees of the type to be defined). They are widely used in large verification projects – including CompCert, Iris, Verinum, and MetaRocq – to express complex, structured specifications. Despite this widespread use, the treatment of nested inductive types in both and is unsatisfactory. rejects many practical definitions while accepts definitions for which no usable elimination principle can be defined. Neither system provides reliable automatic generation of elimination principles. As a result, developers must define custom eliminators by hand, leading to fragility, duplication, and significant proof engineering overhead. This paper introduces a novel validity criterion for nested inductive types that guarantees that they can be elaborated into well-formed mutual inductive types. Under this criterion, the elimination principle for the original nested definition is provably equivalent to that of its elaborated mutual form. Our condition strictly generalizes Lean’s current check while ruling out exactly the problematic cases accepted in . Using this foundation, we give a systematic method for automatically generating correct elimination principles for nested inductive types, and we provide an implementation integrated into , along with an implementation plan for .

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p530-p doi:10.1145/3808322

Typestate via Revocable Capabilities
Songlin Jia, Craig Liu, Siyuan He, Haotian Deng, Yuyan Bao, and Tiark Rompf
(Purdue University, USA; Augusta University, USA)
Managing stateful resources safely and expressively is a longstanding challenge in programming languages, especially in the presence of aliasing. For example, scope-based constructs like Java’s synchronized blocks offer ease of reasoning, but they restrict expressiveness and parallelism. Conversely, imperative, flow-sensitive approaches enable fine-grained control, but they require sophisticated typestate analyses and often burden programmers with explicit state tracking.
In this work, we present a novel approach that unifies the ease of scoped reasoning with the expressiveness of imperative typestate management. Our design extends traditional flow-insensitive capability mechanisms to a flow-sensitive setting. In particular, we decouple capability lifetimes from lexical scopes, allowing functions to receive, revoke, or return capabilities in a flow-sensitive manner, building on existing mechanisms for the safety and ergonomics of scoped capability programming.
We implement our approach as an extension to the Scala 3 compiler, leveraging path-dependent types and implicit resolution to enable concise, statically safe, and expressive typestate programming. Our prototype generically supports a wide range of patterns, including file operations, advanced locking protocols, DOM construction, and session types, showing that expressive and safe typestate management can be achieved with minimal extensions to an existing language with capability support.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p532-p doi:10.1145/3808323

Persistent Iterators with Value Semantics
Yihe Li and Gregory J. Duck
(National University of Singapore, Singapore)
Iterators are a fundamental programming abstraction for traversing and modifying elements in containers in mainstream imperative languages such as C++. Iterators provide a uniform access mechanism that hides low-level implementation details of the underlying data structure. However, iterators over mutable containers suffer from well-known hazards including invalidation, aliasing, data races, and subtle side effects. Immutable data structures, as used in functional programming languages, avoid the pitfalls of mutation but rely on a very different programming model based on recursion and higher-order combinators (map, foldl, traverse, etc.) rather than iteration. However, these combinators are not always well-suited to expressing certain algorithms, and recursion can expose implementation details of the underlying data structure.
In this paper, we propose persistent iterators---a new abstraction that reconciles the familiar iterator-based programming style of imperative languages with the semantics of persistent data structures. A persistent iterator snapshots the version of its underlying container at creation, ensuring safety against invalidation and aliasing. Iterator operations (++, erase, etc.) operate on the iterator-local copy of the container, giving true value semantics: variables can be rebound to new persistent values while previous versions remain accessible. We implement our approach in the form of LibFpp---a C++ container library providing persistent vectors, maps, sets, strings, and other abstractions as persistent counterparts to the Standard Template Library (STL). Our evaluation shows that LibFpp retains the expressiveness of iterator-based programming, eliminates iterator-invalidation, and achieves asymptotic complexities comparable to STL implementations---albeit with the higher constant-factor overheads of persistence. Our design targets use cases where persistence and safety are desired, while allowing developers to retain familiar iterator-based programming patterns.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p537-p doi:10.1145/3808324

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)
Verus is a verification tool for the Rust programming language that has already been put to use in several significant systems verification efforts. Verus offers a distinctive approach among Rust verification systems in that, in addition to offering fast SMT-based automation, it supports verification of both safe and unsafe Rust code in a single, unified framework. It achieves this by providing users with a range of proof-oriented types—types introduced specifically by Verus to aid in verification—on top of which one can then build verified implementations of Rust APIs that would otherwise require the use of unsafe Rust features.
In this paper, we develop VerusBelt, the first semantic soundness proof for a significant subset of Verus. In addition to modeling the full range of Verus's core proof-oriented types—including cells, invariants, resource algebras, and storage protocols—VerusBelt accounts (for the first time) for full-fledged Rust lifetimes, concurrency and thread safety, and mutable borrows. A central challenge involves building a model of shared borrows that is generic enough to support storage protocols—we tackle this by marrying RustBelt's lifetime logic with the Leaf library for temporary resource sharing in Iris. All our proofs are mechanized in Iris/Rocq.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable ACM SIGPLAN Distinguished Paper Award Article: pldi26main-p559-p doi:10.1145/3808325

Restart and Refine: Scalable IFDS Taint Analysis across Memory Budgets
Yujiang Gui, Yonggang Tao, and Jingling Xue
(UNSW, Australia)
Taint analysis, widely used for bug and vulnerability detection, is typically formulated as a flow- and context-sensitive IFDS analysis. To achieve field sensitivity, IFDS models heap locations as k-limited access paths but suffers from cubic time and quadratic space complexity, leading to prohibitive costs under realistic memory budgets and frequent out-of-memory failures or timeouts. Existing improvements target scalability or precision under abundant memory but remain fragile under constrained resources.
We present ReFine, an iterative restart-and-refinement framework that enables scalable IFDS taint analysis across diverse memory budgets. When memory is exhausted, ReFine reuses partial results from terminated runs as sound under-approximations to guide subsequent iterations. Each restart occurs at a partial-analysis point, where results are abstracted and refined by leveraging that taint propagation is monotonic under field extension—allowing longer access paths to be safely summarized by their prefixes. We formalize this process as a fixpoint computation over product semilattices and prove soundness, correctness, and termination.
Evaluated on 31 real-world Android apps against a state-of-the-art IFDS taint analysis, ReFine wraps it in a restart-and-refinement framework, analyzing 5.0x more apps under 16 GB and 2.4x more under 800 GB, with up to 52.5x speedup. By turning partial analyses into progressive refinement, ReFine delivers sound, precise, and highly scalable IFDS taint analysis across diverse memory budgets.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p561-p doi:10.1145/3808326

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)
Redundancy elimination is a key optimization direction, and loop nests are the main optimization target in modern compilers. Previous work on redundancy elimination of array computations in loop nests either targets specific computation patterns or fails to recognize redundancies with complex structures. This paper proposes RACE (Redundant Array Computation Elimination), a hash-based technique that utilizes a novel two-level scheme to identify the data reuse between array references and the computation redundancies between expressions, enabling hierarchical redundancy detection beyond pattern-specific methods. It traverses the expression trees in loop nests to detect redundancies hierarchically in linear time and generates efficient code with optimized auxiliary arrays that store redundant computation results. Furthermore, RACE supports the expression reassociation with various aggressive strategies to improve the redundancy opportunities. Experimental results demonstrate the effectiveness of RACE.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p566-p doi:10.1145/3808327

Hyper Separation Logic
Trayan Gospodinov, Peter Müller, and Thibault Dardinier
(INSAIT at Sofia University St. Kliment Ohridski, Bulgaria; ETH Zurich, Switzerland)
Many important functional and security properties—including non-interference, determinism, and generalized non-interference (GNI)—are hyperproperties, i.e., properties relating multiple executions of a program. Existing separation logics allow one to reason about specific classes of hyperproperties, e.g., ∀∀-hyperproperties such as non-interference and ∃∃-properties such as non-determinism. However, they do not support quantifier alternation, which is for instance needed to express GNI. The only existing logic that can reason about such properties is Hyper Hoare Logic, but it does not support heap-manipulating programs and, thus, is not applicable to common imperative programs.
This paper introduces Hyper Separation Logic (HSL), the first program logic that supports modular reasoning about hyperproperties with arbitrary quantifier alternation over programs that manipulate the heap. HSL generalizes Hyper Hoare Logic with a novel hyper separating conjunction that lifts the standard separating conjunction to sets of states, enabling a generalized frame rule for hyperproperties. We prove HSL sound in Isabelle/HOL and demonstrate its expressiveness for hyperproperties that lie beyond the reach of existing separation logics.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p595-p doi:10.1145/3808328

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)
Among the biggest challenges in property-based testing (PBT) is the constrained random generation problem: given a predicate on program values, randomly sample from the set of all values, and only values, satisfying that predicate. Efficient solutions to this problem are critical, since the executable specifications used by PBT often have preconditions that input values must satisfy in order to be valid test cases, and satisfying values are often sparsely distributed.
We propose a novel approach to this problem using deductive program synthesis. We present a set of synthesis rules, based on a denotational semantics of generators, that give rise to an automatic procedure for synthesizing correct generators. Our system handles recursive predicates by rewriting them as catamorphisms and then matching with appropriate anamorphisms; this is theoretically simpler than other approaches to synthesis for recursive functions, yet still extremely expressive.
Our implementation, Palamedes, is an extensible library for the Lean theorem prover. The synthesis algorithm itself is built out of standard proof-search tactics, reducing implementation burden and allowing the algorithm to benefit from further advances in Lean proof automation.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p622-p doi:10.1145/3808329

An Efficient Algorithm for Streaming BPE Tokenization
Konstantinos Mamouras, Angela W. Li, and Yudi Yang
(Rice University, USA)
Tokenization is an essential text preprocessing step in almost all large language models (LLMs), and byte-pair encoding (BPE) is a popular tokenization method used by models such as GPT, GPT-2, and RoBERTa. Since LLMs have many applications that require the fast processing of large amounts of data (e.g., real-time document summarization and analysis), offline tokenization algorithms may have high latency or prohibitive memory requirements. In this paper, we study BPE tokenization with a focus on providing a streaming implementation. A BPE tokenizer is specified with an ordered list of token merge rules, where each rule describes the merging of two adjacent tokens. We introduce the concept of delay for a list of BPE merge rules, which corresponds to the amount of lookahead needed before tokens can be finalized. We view BPE tokenization as a sequence-to-sequence transduction and show how to obtain a bound on delay. This bound enables streaming tokenization with a low memory footprint. We propose a novel streaming algorithm that uses a small amount of memory (independent of the input text) and has linear time complexity in the length of the input text. Our experimental evaluation shows that our algorithm performs well in comparison to existing BPE tokenizers.

Publisher's Version Artifacts Functional Article: pldi26main-p647-p doi:10.1145/3808330

Uniformity Analysis in the WebGPU Shading Language
James Lee-Jones, John Wickerson, and Alastair F. Donaldson
(Imperial College London, UK)
The WebGPU programming model brings general-purpose GPU programming to the web, allowing untrusted JavaScript to issue parallel workloads to client GPUs. To ensure reliability, WebGPU mandates uniformity analysis—a static check that rejects programs that could cause barrier divergence, a GPU control-flow error that can hang execution and require OS-level recovery. While traditional GPU models treat barrier divergence as undefined behaviour, WebGPU’s need for safety and reliability makes this unacceptable. We present the first comprehensive formal and practical study of uniformity analysis in WebGPU, identifying four key issues and making corresponding contributions: (1) Lack of definition: The analysis currently defines non-uniform programs only as those it rejects, without an independent notion of barrier divergence. We provide an operational semantics for TinyWGSL, a core calculus of the WebGPU Shading Language (WGSL), developed in consultation with WGSL specification editors and implementers. This semantics rigorously defines barrier divergence in the context of WGSL for the first time. (2) Complex specification: The current description of uniformity analysis in WGSL is lengthy and imprecise. We reformulate it via concise formal rules for TinyWGSL and argue their soundness with respect to our semantics. (3) Lack of soundness and precision: Using our semantics, we expose soundness and precision flaws in the analysis as presented in the WGSL specification. In response, we have proposed four significant changes to the specification (all accepted). (4) Testing difficulty: The complex, semi-formal definition of uniformity in the WGSL specification makes it hard to test implementations. We mechanise uniformity analysis in Alloy and use Alloy’s test generation to stress-test the Chromium implementation, revealing specification–implementation discrepancies and a bug in the Chromium implementation. Overall, our work resolves an important GPU programming problem (rigorously defining barrier divergence), brings an interesting new analysis to the attention of the PL community, and demonstrates the impact of applying formal PL techniques to an important industrial language specification.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p659-p doi:10.1145/3808331

Expecto: Extracting Formal Specifications from Natural Language Description for Trustworthy Oracles
Dongjae Lee and Kihong Heo
(KAIST, Republic of Korea)
Specification-Driven Development (SDD) has emerged as a promising paradigm in software development. This trend is fueled by recent advances in leveraging large language models (LLMs) to generate code from user intents expressed in natural language. However, the reliance on natural language specifications introduces ambiguity and challenges in ensuring correctness. To address these problems, we present Expecto, a system that automatically extracts trustworthy formal specifications from natural language intents. Expecto employs a neuro-symbolic approach, combining the strengths of LLMs and program synthesis techniques. Our key idea is to adopt a top-down, modular specification synthesis algorithm that breaks down the complex task of specification extraction into manageable units. The specifications are written in a domain-specific language (DSL) designed to succinctly express formal specifications of functional requirements. This modular synthesis with a concise DSL reduces the reasoning complexity for LLMs and enhances the accuracy of the extracted specifications. Our results demonstrate that Expecto significantly improves the accuracy and reliability of extracted specifications compared to a monolithic, purely LLM-based approach. Furthermore, when applied to real-world buggy programs in Defects4J, Expecto successfully generates formal specifications that detect more bugs than the baselines.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p660-p doi:10.1145/3808332

Synthesizing Backward Error Bounds, Backward
Laura Zielinski and Justin Hsu
(Cornell University, USA)
Backward stability is a desirable property for a well-designed numerical algorithm: given an input, a backward stable floating-point program produces the exact output for a nearby input. While automated tools for bounding the forward error of a numerical program are well-established, few existing tools target backward error analysis. We present a formal framework that enables sound, automated backward error analysis for a broad class of numerical programs. First, we propose a novel generalization of the definition of backward stability that is both compositional and flexible, satisfied by a wide range of floating-point operations. Second, based on this generalization, we develop the category Shel where morphisms model stable numerical programs, and show that structures in Shel support a rich variety of backward error analyses. Third, we implement a tool, eggshel, that automatically searches within a syntactic subcategory of Shel to prove backward stability for a given program. Our algorithm handles many programs with variable reuse, a known challenge in backward error analysis. We prove soundness of our algorithm and use our tool to synthesize backward error bounds for a suite of programs that were previously beyond the reach of automated analysis.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable ACM SIGPLAN Distinguished Paper Award Article: pldi26main-p665-p doi:10.1145/3808333

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)
PriML, a language developed in recent work on responsive parallelism, extends traditional fine-grained parallel languages such as Cilk by allowing programmers to annotate threads with priorities. Programmers thus get the substantial throughput benefits of lightweight threads scheduled by a user-level runtime, while retaining the ability to use threads for responsive applications typically programmed with lower-level threading systems. PriML’s type system guarantees the absence of priority inversions, costly performance errors in which high-priority threads are delayed by low-priority threads, enabling formal bounds on throughput and responsiveness, but at the cost of expressiveness: threads may not change priority once spawned and the priority of a thread is specified as a priority literal in the code (i.e., priorities are not first-class). This work relaxes the two assumptions above by tracking sets of priorities using techniques drawn from the literature on refinement types. We extend the graph-based cost models of responsive parallelism to incorporate first-class and changing priorities, and prove bounds on the throughput and responsiveness of well-typed programs in our extended language. We implement our type system extensions in the PriML compiler, and demonstrate the benefits of the extension using a concurrent web server as a case study.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p701-p doi:10.1145/3808334

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)
Reasoning about programs in the presence of mutation and aliasing is notoriously difficult. Rust has popularized lifetime-based ownership tracking in systems programming, but its “shared XOR mutable” model is fundamentally at odds with higher-level functional programming. Reachability types offer an alternative: they enable safe sharing and escape of mutable data by tracking which resources each expression can reach.
To track internal reachability within complex object graphs, reachability types adopt self-references that let components refer to enclosing resources from inside, just like this pointers in OO languages. While natural for declaratively typing escaping data, self-references complicate subtyping and furthermore type inference: variance restricts where self-references may appear, yet useful type conversions must allow them to vary in controlled ways, which in turn imposes constraints on inference. As an undesirable result, prior works require programmers to insert term-level coercions for even just avoidance—avoiding ill-scoped names in types.
With all prior works being declarative, we investigate algorithmic reachability types in this work. We introduce a refined subtyping relation that permits more flexible usages of self-references. We further develop a sound and decidable bidirectional typing algorithm, implemented and verified in Lean. The algorithm automatically avoids ill-scoped names in types, and infers qualifiers via a lightweight unification mechanism. As a step towards practical reachability programming, we show that the system is capable of tracking diverse reachability patterns without explicit coercions in complex Church-encoded datatypes.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p703-p doi:10.1145/3808335

Syntactic Implicit Parameters with Static Overloading
Daan Leijen and Tim Whiting
(Microsoft Research, USA; Brigham Young University, USA)
Implicits provide a powerful mechanism for term-based inference, where "obvious" arguments can be omitted and inferred by the type checker. This can greatly reduce the programmer's burden and improve the clarity of expression. As such, many languages support a form of implicits in practice, such as type classes in Haskell or Lean, or implicits in Scala. Unfortunately, many of these systems have become increasingly complex and often require significant implementation effort.
In this paper we take a fresh look at the design space with an arguably simpler approach based on two orthogonal features: _syntactic implicit parameters_ and _static overloading_. Each of these features is limited in scope and has a straightforward implementation. Taken together though, they are surprisingly expressive and we believe they can cover many of the common usage scenarios of implicits in practice.
We formalize our system and provide various examples, and prove our elaboration is coherent. We also give an inference algorithm and show it is sound and complete. Our system is fully implemented in the Koka language, and we describe our experience with these features at scale, and discuss further extensions.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p717-p doi:10.1145/3808336

A Verified Parallel Scheduler for OCaml 5
Clément Allain and Gabriel Scherer
(Inria, France; Université Paris Cité, France)
We present the implementation and mechanized verification of a realistic parallel scheduler for OCaml 5 using the Iris-based Zoo framework. Similarly to Domainslib, it relies on a work-stealing strategy to perform load balancing but also supports other scheduling strategies thanks to its flexible interface. e provide basic benchmarks demonstrating that its performance is on par with other schedulers from the OCaml ecosystem.
As part of this effort, we verify the Chase-Lev work-stealing deque, as implemented in the Saturn library. We show that it features a subtle external and future-dependent linearization point. To deal with it, we introduce new abstractions for reasoning about prophecy variables in Iris.

Publisher's Version Published Artifact Artifacts Available Article: pldi26main-p742-p doi:10.1145/3808337

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)
Recent advances in foundation models have motivated hybrid programming that integrates natural language descriptions, formal specifications, and executable code. A critical challenge in such systems lies in achieving semantic alignment across heterogeneous representations at different abstraction levels. This challenge is particularly pressing in programmatic reinforcement learning (PRL) for robotics, where long-horizon, sparse-reward tasks demand tight coordination between symbolic reasoning and continuous control. Existing approaches either rely on manually engineered symbolic representations or on LLM-generated plans that might be untrustworthy or infeasible to execute, leaving such fundamental gaps unaddressed. We present a closed-loop, counterexample-guided synthesis framework that unifies LLM-based planning, formal verification, and differentiable behavior tree (BT) synthesis for neuro-symbolic policy learning. The framework first converts natural language task descriptions into PDDL, then generates valid high-level plans via a Guess-Check-Critique loop that interleaves LLM generation with SMT-based verification. We automatically compile symbolic abstractions in verified plans into parameterized termination conditions, and co-optimize them with low-level policies to enforce semantic consistency. The learned sub-policies are composed into an integrated BT and fine‑tuned to ensure task-level executability. Furthermore, we perform closed-loop iterations of abstractions and compilations using feedback from verification and learning, while incrementally building a reusable skill library for efficient knowledge transfer. Experiments on challenging long-horizon robotic tasks show that our method exceeds state-of-the-art methods while providing interpretability and generalization.

Publisher's Version Published Artifact Artifacts Available Article: pldi26main-p772-p doi:10.1145/3808338

SuperCollider: Scalable and Effective Data Race Detection for CUDA
Mark Stephenson, Sana Damani, Mohamed Tarek Ibn Ziad, Anis Ladram, and Michael Garland
(NVIDIA, USA)
Data races, which occur when two or more threads incorrectly access the same memory location without appropriate synchronization, cause CUDA programmers considerable pain. Even experts struggle to reason about extreme parallelism, multiple memory spaces and scopes, and diverse synchronization mechanisms. Races can manifest as subtle data corruption, deadlock, or livelock, which are difficult to reproduce in a debugging environment. To date, there is no generally reliable tool for identifying races in GPU programs at scale. State-of-the-art dynamic GPU race detectors attempt to detect data races by faithfully tracking the memory operations, barriers, and memory fences executed by tens of thousands of threads. While this complexity enables the detection of subtle races, it comes with a cost: existing tools incur substantial memory-footprint overheads (e.g., greater than 9x) and/or runtime overheads (e.g., 1000x), and tend to report false positives. This paper introduces SuperCollider, a simple race detector for CUDA that tracks only thread-level state, is agnostic to synchronization protocols, introduces no memory-footprint overhead, seamlessly handles shared, global, and tensor memory spaces, does not produce false positives, and is relatively fast. Although SuperCollider cannot detect all races, we demonstrate that it effectively catches many data races in professionally authored CUDA programs, including races that prior art cannot. Our approach exposed over 90 data races across libraries and CUDA benchmarks, and even found a race in the CUDA Programming Guide. Unlike prior art, SuperCollider can operate at the extreme scales required by modern GPU workloads.

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: pldi26main-p774-p doi:10.1145/3808339

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)
Tools for verifying leakage descriptions of hardware aim to ensure that a given hardware design doesn’t leak secrets via its microarchitecture, when executing programs with appropriate countermeasures. However, existing techniques for proving correctness of leakage descriptions are based on non-constructive proofs via non-interference. As a result, they often rely on expensive solvers that offer little help when verification fails or require handwritten invariants, which are difficult to come up with and even harder to debug. In this paper, we present a new approach to leakage verification which we call simulation-based leakage proofs. To show that a leakage description correctly captures a hardware design using a simulation-based proof, the user constructs a simulator—another hardware design that must faithfully replicate all attacker-observable behavior from explicitly leaked secrets. Simulation-based proofs therefore offer a constructive alternative to classic non-interference proofs, exposing a proof object—the simulator, witnessing the correctness claim. As simulators are just programs, we can write, execute and debug them like any other program, making them easy to use. We also show that they can be checked locally, which makes proof checking fast. We implement simulation-based leakage proofs in Pantomime, a tool that supports writing processors and their leakage proofs in Haskell; we report on using Pantomime to write and verify AIMCore, a 5-stage in-order processor, its leakage description, and simulator, as well as a side-channel hardened version of the core. We show that Pantomime verifies them efficiently (it checks AIMCore in under 40s), and use AIMCore’s leakage description to check for leakages in crypto libraries which uncovered two new vulnerabilities in wolfSSL that have both been assigned CVE’s.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p785-p doi:10.1145/3808340

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)
We propose an incremental approach for safety proofs that decomposes a proof with a complex inductive invariant into a sequence of simpler proof steps. Our proof system combines rules for (i) forward reasoning using inductive invariants, (ii) backward reasoning using inductive invariants of a time-reversed system, and (iii) prophecy steps that add witnesses for existentially quantified properties. We prove each rule sound and give a construction that recovers a single safe inductive invariant from an incremental proof. The construction of the invariant demonstrates the increased complexity of a single inductive invariant compared to the invariant formulas used in an incremental proof, which may have simpler Boolean structures and fewer quantifiers and quantifier alternations. Under natural restrictions on the available invariant formulas, each proof rule strictly increases proof power. That is, each rule allows to prove more safety problems with the same set of formulas. Thus, the incremental approach is able to reduce the search space of invariant formulas needed to prove safety of a given system. A case study on Paxos, several of its variants, and Raft demonstrates that forward-backward steps can remove complex Boolean structure while prophecy eliminates quantifiers and quantifier alternations.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p807-p doi:10.1145/3808341

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)
This work introduces StageSAT, a new approach to solving floating-point satisfiability that bridges SMT solving with numerical optimization. StageSAT reframes a floating-point formula as a series of optimization problems in three stages, each with increasing precision. It begins with a fast, projection-aided descent objective to efficiently guide the search toward a feasible region, then proceeds to bit-level accuracy with units-in-the-last-place (ULP)² optimization and a final n-ULP lattice refinement to ensure correctness. By construction, the final two stages use a representing function that evaluates to zero if and only if a candidate satisfies all constraints. Thus, whenever optimization drives the bit-precise objective to zero, the resulting assignment is a valid solution, providing a built-in guarantee of soundness (no spurious SAT results). To further improve the search, StageSAT introduces a partial monotone descent property on linear constraints via an orthogonal projection technique, which prevents the optimizer from stalling on flat or misleading objective landscapes. Critically, this solver requires no heavy bit-level reasoning or specialized abstractions of floating-point arithmetic; it treats complex arithmetic as a black box, using runtime evaluations to navigate the input space.
We implement StageSAT and evaluate it on extensive benchmarks, including the SMT-COMP’25 floating-point suites and difficult cases from prior work. In our experiments, StageSAT proved both more scalable and more accurate than state-of-the-art optimization-based alternatives. It solved strictly more formulas than any competing solver under the same time budget – in fact, StageSAT found most of the satisfiable instances in our benchmarks and never produced a spurious model for an unsatisfiable formula. This amounts to 99.4% recall on satisfiable cases with 0% false SAT in our benchmarks, exceeding the reliability of prior optimization-based solvers we tested. StageSAT also delivered significant speedups (often 5–10× faster) over traditional bit-precise SMT solvers and earlier numeric solvers. These results demonstrate that our staged optimization strategy can significantly improve both the performance and correctness of floating-point satisfiability solving.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p828-p doi:10.1145/3808342

Categorical Semantics of Probabilistic Symbolic Execution
John M. Li, Jack Czenszak, and Steven Holtzen
(Northeastern University, USA; Yale University, USA)
Symbolic execution has emerged as a powerful technique for scaling exact probabilistic inference to languages with more expressive features. But, this expressivity comes at a price: probabilistic programming languages based on symbolic execution are difficult to debug, optimize, and prove correct due to the many intricacies inherent to high-performance symbolic execution strategies. We aim to make it easier to work with probabilistic symbolic executors by developing symbolic sets, a new semantic domain that cleanly captures the notion of computation underlying symbolic execution. Just as a symbolic executor replaces ordinary execution with a lifted semantics, symbolic set theory replaces ordinary set theory with a lifted mathematics: the category of symbolic sets is a Grothendieck topos, which allows type theory to be used as a metalanguage for working with symbolic sets and functions. We prove a metatheorem that shows how a large class of definitional interpreters written in the internal language of symbolic sets are automatically correct for their ordinary set-theoretic interpretations. Using this metatheorem, we give the first full correctness argument for a symbolic probabilistic language with higher-order functions, type-directed state merging, pattern matching, and structural recursion.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable ACM SIGPLAN Distinguished Paper Award Article: pldi26main-p831-p doi:10.1145/3808343

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)
Proof search powers our most advanced programming tools, from type systems, to search tactics for interactive theorem provers, to Datalog-backed program analyses. Although proof search tooling is powerful and now pervasive, debugging it is hard, even for experts. When proof search cannot prove the goal, the programmer’s best source of information is a massive AND–OR graph representing the tool’s internal state during the proof search process. The difficulty of understanding and debugging this vast trace of internal state locks programmers out of exactly the high-assurance automated reasoning tools we want them to adopt.
We propose a new formulation of proof search debugging, which: (i) views AND–OR graphs as a partial representations of the underlying proof system, (ii) treats debugging as a process of applying modifications to this proof system, and (iii) uses a debugging tool to solicit these modifications until the resulting proof system proves the original goal. This approach unifies decades of ad-hoc strategies in a single general-purpose framework and is applicable to the diverse range of programming tools that use proof search. Our framework can express existing “why-not” debugging strategies as well as new strategies, and we evaluate such strategies on 284 AND–OR graphs. We find that a strategy that enforces a property called Strong Soundness reduces the number of decisions by 1.4×–3.2× compared to an unsound baseline, and a new property we call Strong Completeness Modulo Observability enables pruning to further reduce decisions by 1.0×–2.8× for an overall reduction of 2.0×–3.8×.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p879-p doi:10.1145/3808344

Compiling to Recurrent Neurons
Joey Velez-Ginorio, Nada Amin, Konrad Kording, and Steve Zdancewic
(University of Pennsylvania, USA; Harvard University, USA)
Discrete structures are currently second-class in differentiable programming. Since functions over discrete structures lack overt derivatives, differentiable programs do not differentiate through them and limit where they can be used. For example, when programming a neural network, conditionals and iteration cannot be used everywhere; they can break the derivatives necessary for gradient-based learning to work. This limits the class of differentiable algorithms we can directly express, imposing restraints on how we build neural networks and differentiable programs more generally. However, these restraints are not fundamental. Recent work shows conditionals can be first-class, by compiling them into differentiable form as linear neurons. Similarly, this work shows iteration can be first-class---by compiling to linear recurrent neurons. We present a minimal typed, higher-order and linear programming language with iteration called Cajal(N). We prove its programs compile correctly to recurrent neurons, allowing discrete algorithms to be expressed in a differentiable form compatible with gradient-based learning. With our implementation, we conduct two experiments where we link these recurrent neurons against a neural network solving an iterative image transformation task. This determines part of its function prior to learning. As a result, the network learns faster and with greater data-efficiency relative to a neural network programmed without first-class iteration. A key lesson is that recurrent neurons enable a rich interplay between learning and the discrete structures of ordinary programming.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p881-p doi:10.1145/3808345

Evolving Abstract Transformers for Gradient-Guided, Adaptable Abstract Interpretation
Shaurya Gomber, Debangshu Banerjee, and Gagandeep Singh
(University of Illinois Urbana-Champaign, USA)
Current numerical abstract interpretation relies on fixed, hand-crafted, instruction-specific transformers tailored to each domain, giving rise to three significant limitations. First, extensibility is limited because transformers cannot be reused across domains and new transformers need to be designed for each new domain or operator. Second, precise compositional reasoning over instruction sequences is difficult as transformers are defined only at the instruction level. Third, all downstream tasks are forced to use the same fixed transformer, irrespective of their precision, efficiency, or task-specific requirements. To address these limitations, we propose the Evolving Abstract Transformer, a general transformer that replaces the fixed single-output design of traditional transformers with an adaptable search over a parametric space of sound outputs. This is achieved through two underlying algorithms we develop. First, the Universal Parametric Output Space Encoder (UPOSE) constructs a compact parametric space of sound outputs for any polyhedral numerical domain and any operator in the Quadratic-Bounded Guarded Operators (QGO) class which includes both individual instructions and structured sequences. Next, the Adaptive Gradient Guidance (AGG) algorithm leverages the differentiable structure of the space generated by UPOSE and uses gradient-based updates to efficiently search it according to downstream analysis objectives and available runtime, continually evolving the output as more time is provided. We implement these ideas in the AbsEvolve framework and evaluate their effectiveness across three numerical abstract domains: Zones, Octagons, and Polyhedra. Our results demonstrate that the evolving transformer works across domains and handles diverse instructions and sequences, allowing efficient adaptability in the precision–efficiency tradeoff by adjusting the number of gradient steps in the search, while also reaching the most precise invariants up to 3.2× faster than existing baselines.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p887-p doi:10.1145/3808346

TreeCoder: Systematic Exploration and Optimisation of Decoding and Constraints for LLM Code Generation
Henrijs Princis, Arindam Sharma, and Cristina David
(University of Bristol, UK)
Large language models (LLMs) have shown remarkable ability to generate code, yet their outputs often violate syntactic or semantic constraints when guided only through natural language prompts. We introduce TreeCoder, the most general and flexible framework to date for exploring decoding strategies, constraints, and hyperparameters in LLMs, and use it in code generation to enforce correctness and structure during decoding rather than relying on prompt engineering. TreeCoder represents decoding as a tree search over candidate programs, where both decoding strategies and constraint functions–such as style, syntax, execution–are treated as first-class, optimisable components. This design enables systematic exploration and automatic tuning of decoding configurations using standard optimisation techniques. Experiments on Python, SQL and Rust show that TreeCoder consistently improves accuracy across open-source models such as CodeLlama, Mistral, DeepSeek and Qwen, often significantly outperforming their unconstrained baselines.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p906-p doi:10.1145/3808347

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)
Many quantitative properties of probabilistic programs can be characterized as least fixed points, but verifying their lower bounds remains a challenging problem. We present a new approach to lower-bound verification that exploits and extends the connection between the uniqueness of fixed points and program termination. The core technical tool is a generalization of ranking supermartingales, which serves as witnesses of the uniqueness of fixed points. Our method provides a simple and unified reasoning principle applicable to a wide range of quantitative properties, including termination probability, the weakest preexpectation, expected runtime, higher moments of runtime, and conditional weakest preexpectation. We provide a template-based algorithm for automated verification of lower bounds and demonstrate the effectiveness of the proposed method via experiments.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p950-p doi:10.1145/3808348

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)
Weak monadic second-order logic (wMSO) is a foundational tool for specifying regular properties. Traditional decision procedures for this logic typically translate wMSO formulas into finite automata. Although the logic is decidable, this approach incurs non-elementary complexity in the worst-case. Nearly thirty years ago, the state-of-the-art MONA tool showed that, despite these theoretical limits, wMSO can be decided efficiently in practice through carefully optimized automata constructions. We revisit wMSO from an algebraic perspective by introducing Extended Regular Expressions with Quantifiers (EREQ). Instead of relying on automata determinization, EREQ employs symbolic derivatives to perform incremental quantifier elimination, providing a compositional and symbolic alternative to classical automata-based approaches.
We present a linear-time translation of wMSO into EREQ and a derivative-based decision procedure for EREQ. We prove the correctness of the translation and of the derivative construction in the Lean proof assistant. We implement our approach in Rust and evaluate it on a set of established MONA benchmarks, demonstrating competitive performance with state-of-the-art tools. Our results demonstrate the potential of derivative-based methods, opening new avenues for efficient decision procedures in EREQ.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p993-p doi:10.1145/3808349

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)
Modern processors integrate heterogeneous devices to expose unified shared memory. Yet, the de-facto design pattern used to compose their disparate coherence protocols lacks a formal foundation. This leaves the door open for subtle consistency bugs, in a critical gap between practice and correctness. This paper provides the first formal, machine-checked proof that a de-facto design pattern, which we call the Principle of Synchronous Propagation, is correct. Leveraging a new unifying abstraction for coherence protocols, our central theorem (machine checked in Lean) proves that Synchronous Propagation is sufficient to guarantee the Compound Memory Consistency Model for a wide class of protocols. Our work provides long-needed assurance for current designs and delivers a reusable, compositional framework for verifying future heterogeneous systems.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p1012-p doi:10.1145/3808350

Abstract Interpretation with Confidence: Quantifying the Precision of Dataflow Analysis with Probabilities
Yuanfeng Shi, Ziyue Jin, and Xin Zhang
(Peking University, China)
Abstract interpretation has served as a foundational framework for static program analysis, enabling the over approximation of program semantics to be sound (i.e., no false negatives) but often at the cost of false alarms due to incompleteness. Although prior efforts to address false alarms have incorporated probabilistic techniques to compute confidence values for alarms, these methods are largely guided by empirical intuitions and lack a theoretical foundation. This paper bridges this gap by proposing a principled framework to quantify the confidence in results produced by a dataflow analysis based on abstract interpretation. Specifically, we define the problem as calculating the probability of the abstract interpreter being locally complete for a sampled program from the distribution of programs consistent with such abstract interpretation. By proposing a compositional denotational semantics ⟨⟨· ⟩⟩, we derive the distribution of program outputs to compute those confidence probabilities. Moreover, to ensure tractability, we propose another denotational semantics ⟨⟨· ⟩⟩^lc that under-approximates ⟨⟨· ⟩⟩. The paper proves both the correctness of the two semantics, and therefore establishes a theoretical foundation for quantifying the precision of static program analysis with probabilities.

Publisher's Version Article: pldi26main-p1066-p doi:10.1145/3808351

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)
Immutability is common in the programming mainstream: deep immutability is the default in functional languages while imperative languages typically provide opt-in support for shallow immutability, usually enforced through static checking.
Python is a dynamic imperative language where mutability is inherent: not only are most objects mutable, but programs themselves---modules, classes, functions---are represented by mutable objects at run-time, and libraries routinely rely on this mutability. This makes adding immutability to Python a significant challenge.
This paper presents the design and implementation of deep immutability for Python. Our primary motivation is to permit multiple sub-interpreters to directly share object references, which currently requires costly serialisation. Sharing via immutability introduces a soundness challenge, as a violation could corrupt the interpreter's state.
We identify numerous challenges that stem from decades of design decisions that did not anticipate immutability, and show how they can be overcome through two complementary techniques: detachment, which severs run-time links that would cause immutability to propagate too widely, and freezability, which gives objects run-time control over whether and how they may become immutable. Together, these principles form a general design pattern for deep immutability in dynamic languages. We validate our design with an implementation on CPython 3.15 that is backwards-compatible with existing programs and enables direct, zero-copy sharing of immutable objects across sub-interpreters.

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p1129-p doi:10.1145/3808352

Corrigendum: Falcon: A Scalable Analytical Cache Model
Arjun Pitchanathan, Kunwar Grover, and Tobias Grosser
(University of Edinburgh, UK; Advanced Micro Devices, UK; University of Cambridge, UK)
This is a corrigendum for the article "Falcon: A Scalable Analytical Cache Model" published in Proc. ACM Program. Lang. 8, PLDI, Article 222 (Jun 2024). We make corrections to the experimental evaluation and provide updated data.

Publisher's Version Article: pldi24main-p644-p-CR doi:10.1145/3820287