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

Title Page


Article: oopslab26foreword-fm000-p doi:

Sponsors


Article: oopslab26foreword-fm003-p doi:

Editorial Message
Anders Møller and Işıl Dillig
(Aarhus University, Denmark; University of Texas at Austin, USA)


Article Search Article: oopslab26editorial-fm001-p doi:10.1145/3839445

Probabilistic Floating-Point Round-Off Analysis via Concentration Inequalities
Yichen Tao, Hongfei Fu, Jiawei Chen, and Jean-Baptiste Jeannin
(University of Michigan, USA; Shanghai University of Finance and Economics, China)
Floating-point round-off errors are ubiquitous in numerically intensive programs arising in fields such as scientific computing and optimization. As floating-point errors potentially lead to unexpected and catastrophic program failures, one must derive guaranteed round-off thresholds to ensure the correctness of these programs. However, deterministic round-off thresholds tend to be too conservative to be usable in practice, since they often involve large round-off errors that occur with small probability. Probabilistic thresholds relax deterministic ones by specifying that the probability of the round-off error exceeding a threshold is below a given confidence.
In this work, we propose a novel approach to probabilistic round-off analysis, by applying concentration inequalities over the Taylor expansion from FPTaylor (TOPLAS 2018). A major obstacle in applying concentration inequalities is that the Taylor expansion involves absolute value operators that make the calculation of the expected values of the first order partial differential terms difficult. Our first step to overcome this obstacle is a sound over-approximation that removes the absolute value operators in polynomial expressions. Then, we show how to handle fractional expressions by a transformation into polynomial case. Finally, we show how to improve our approach with range partitioning. Our approach is scalable since the key computational part is the calculation of expected values of polynomial expressions with independent variables, for which the linear and independence properties of expectation boost the computation. Experimental results show that our approach is orders of magnitude more time efficient, while producing thresholds with comparable precision against the state of the art.

Article Search Article: oopslab26main-p169-p doi:10.1145/3839447

Experimental Evaluation Methodology for the Era of No Steady Performance
Jaromír Antoch, Walter Binder, Lubomír Bulej, François Farquet, Vojtěch Horký, Aleksandar Prokopec, Andrea Rosà, and Petr Tůma
(Charles University, Czech Republic; USI Lugano, Switzerland; Oracle Labs, Switzerland)
Recent studies of virtual machine warm up have pointed out that even small deterministic microbenchmarks executed in tightly controlled circumstances often do not reach a steady state of peak performance. This impacts performance evaluation methodologies that focus on performance after warm up, because the lack of a steady state may violate common assumptions made when computing metrics such as the average performance or the confidence interval for that average.
Our work examines the reported lack of steady state in the context of comparatively larger virtual machine workloads. We document and analyze similar lack of steady state and argue that it should be considered an inherent property of these workloads rather than a fault. We introduce an updated performance evaluation methodology for workloads whose execution exhibits segments of steady state performance separated by sudden performance changes. Using the Renaissance benchmark suite for the Java Virtual Machine, we show that the methodology can produce confidence intervals that miss the true performance over 20 % less often than the existing methodologies.

Article Search Artifacts Available Article: oopslab26main-p193-p doi:10.1145/3839448

Formalizing the Linux eBPF Core ISA: A Mechanized Operational Semantics and Its Real-World Applications
Shenghao Yuan, Yazhou Tang, Tianci Cao, Frédéric Besson, Jean-Pierre Talpin, and Mingshuai Chen
(Zhejiang University, China; Inria Rennes, France; Inria, France)
This paper presents a mechanized formal semantics for the Linux eBPF instruction set architecture (ISA). We develop a small-step semantics in Rocq that faithfully formalizes all 153 sequential in-kernel instructions of the eBPF ISA. The semantics is fully executable and has been validated against the official Linux eBPF test suite. This extensive testing revealed inconsistencies in our original formalization. Using this semantics, we have designed, implemented, and verified the soundness of the bit-level abstract domain employed by the Linux eBPF verifier. Our semantics also complements the existing Linux eBPF documentation by providing a rigorous formal specification. During the formalization process, we have discovered previously unknown bugs in the Linux eBPF implementation, and developed new verifier optimizations; the corresponding kernel patches have been upstreamed.

Article Search Article: oopslab26main-p24-p doi:10.1145/3839449

Synthesis of Compact and Expressive Quantum-Circuit Optimizations
Wei Qiang and Ronghui Gu
(Columbia University, USA; Certik, New York, USA)
Today’s quantum devices are noisy, so reducing circuit size is critical for reliable execution. Existing rule-based optimizers often rely on large rule sets that are difficult to manage and still miss long-distance transformations. We present QSymb, a framework for synthesizing compact and expressive quantum-circuit rewrite rules with formal guarantees. We formalize symbolic rewrite rules in which a symbolic gate represents infinitely many subcircuits. We then define canonical symbolic rules of the form L;S = S;R and prove that they constitute a compact generative core from which general symbolic rules can be derived. On top of this formal foundation, given a gate set, QSymb synthesizes (1) a small, non-derivable concrete rule set that is complete up to chosen size and qubit bounds, and (2) a small but expressive canonical symbolic rule set that captures transformations beyond finite or monomial-only patterns. We further present rule anchoring to derive optimization-effective rules from canonical symbolic rules. Together, these results provide both expressiveness and guarantees: soundness of synthesized rules via validation, non-derivability, and bounded completeness. On the IBM-Eagle gate set, QSymb strictly outperforms state-of-the-art rewrite-based optimizers (Qiskit, Guoq, Quartz, TKET, and Queso) in two-qubit-gate reduction on 90%, 67%, 82%, 85%, and 83% of standard quantum algorithm benchmarks, respectively; on Nam gate set, the corresponding rates are 88%, 74%, 81%, 86%, and 82.9%. It achieves final average two-qubit-gate reductions of 27.44% and 29.95%, respectively.

Article Search Artifacts Available Article: oopslab26main-p56-p doi:10.1145/3839450

LLM-Assisted Unsatisfiability Proofs for Satisfiability Modulo Theories, Oracles and Natural Language
Gourav Takhar, Sumit Lahiri, Pankaj Kumar Kalita, and Subhajit Roy
(IIT Kanpur, India; Qualcomm, India; IBM Research, India)
Modern software systems routinely invoke components whose source code is unavailable, such as proprietary libraries or cloud-based APIs. Such closed-box functions provide only oracle-style access: they can be executed on concrete inputs, but their internal logic cannot be inspected. Prior work has explored augmenting SMT solvers—the foundational engines behind contemporary automated reasoning—to handle satisfiability queries over first-order formulas containing calls to such closed-box functions. However, these approaches primarily rely on testing-based techniques to search for satisfying models and therefore do not support constructing proofs of unsatisfiability. While model search is sufficient for bug-finding tasks, the inability to generate unsatisfiability proofs fundamentally limits their applicability to formal verification.
In this work, we present the first SMT solver capable of producing proofs of unsatisfiability for first-order theories that include closed-box function calls. Our key insight is to leverage large language models (LLMs) to conjecture auxiliary lemmas—based on natural language documentation of the closed-box functions—that capture properties relevant for reasoning about their behavior. To support this approach, we introduce an extension of the SMT-LIB language that allows the declaration of closed-box functions together with natural language descriptions, usage documentation, examples, and oracle interfaces. We, then, develop NLUnsat, an SMT solver that operates over this extended syntax to find unsatisfiability proofs on SMT-LIB formulas with closed-box functions.
On a benchmark suite of 193 extended SMT-LIB problems involving closed-box functions, NLUnsat equipped with the openai.gpt-oss:20b LLM solves 89% of the instances, and a virtual best solver across five LLMs solves 98% of the instances. We further evaluate NLUnsat in the setting of deductive verification for programs containing closed-box function calls. On a collection of 15 benchmark programs, our verifier, using NLUnsat as its backend solver, successfully proves all verification goals when given access to a pool of two LLMs, openai.gpt-oss:20b and openai.gpt-oss:120b. Finally, we evaluate NLUnsat on satisfiable benchmark instances: none of these instances were incorrectly classified as unsatisfiable, and the solver successfully finds models for 57 out of 107 satisfiable instances.

Article Search Artifacts Available Article: oopslab26main-p70-p doi:10.1145/3839451

T-REX: Teaching Large Language Models to Reason with Verbalized Execution Semantics
Yan Wang, Ling Ding, Jiechen Sun, Tien N. Nguyen, Shaohua Wang, Aashish Yadavally, Xin Xia, and Yanan Zheng
(Central University of Finance and Economics, China; Independent, China; University of Texas at Dallas, USA; University of Central Florida, USA; Zhejiang University, China; Yale University, USA)
Large language models (LLMs) have shown strong performance in static code tasks like code search, summarization, and generation, but remain limited in dynamic code reasoning, which involves inferring how programs behave during execution without actually running them. This limitation stems from LLMs being trained on static code and lacking the necessary runtime context. In this paper, we present T-REX, a novel teacher-student framework for execution prediction that addresses these limitations by grounding LLM training in actual execution and corresponding execution semantics. T-REX uses a large teacher model (Explainer) to generate fine-grained, stepwise natural language rationales explaining how program state transitions from one statement to another during actual execution. These rationales are used to train a smaller student model (Reasoner) to predict next program states, enabling accurate simulation of program behavior with lower computational cost. Our execution-grounded, rationale-driven training aligns with transition-aware execution semantics at the statement level, enhancing prediction accuracy. Our experiments show that T-REX enables Reasoner to outperform much larger GPT-4o and GPT-4o-mini models across multiple dimensions of runtime behavior prediction, while also aiding in static detection of runtime errors as well as in debugging. Finally, we discuss how T-REX can be generalized to static emulation of any dynamic analysis through such a teacher-student distillation, illustrating with the specific case of dynamic program slicing in Python.

Article Search Article: oopslab26main-p116-p doi:10.1145/3839452

Testing Theorems, Fully Automatically
Segev Elazar Mittelman, Harrison Goldstein, and Leonidas Lampropoulos
(University of Maryland, College Park, USA; University at Buffalo, USA)
While the ultimate goal of interactive theorem proving is to prove theorems, it can really help to test them first. Testing theorems, specifically using property-based testing, helps users identify incorrect definitions and theorem statements before they waste time on a proof that could never succeed. Unfortunately, the testing infrastructure provided by modern theorem provers has yet to reach its full potential. Even QuickChick, the state-of-the-art property-based testing framework for Rocq, which offers random generation for data satisfying inductively defined relations, often requires substantial effort and expertise to be used effectively. This is in part because this effectiveness is heavily sensitive to both the order that hypotheses appear within a theorem, and to the order that inductive constraints appear within the inductive relations involved.
In this paper, we present a novel strategy for testing theorems that is highly effective, fully automatic, and robust to equivalent formulations of theorem and definition statements. To do so, we characterize the exponentially large space of possible QuickChick-style properties and generators as solutions to a constrained scheduling problem. To find the best property or generator in this space, we estimate effectiveness by introducing a notion of "density" for inductive relations, which approximates the tendency for a generator to succeed given arbitrary inputs. We implement our algorithm on top of the QuickChick framework for Rocq and evaluate it in a number of case studies from the literature, demonstrating that our push-button automation is on par with and in some cases even more effective at finding bugs than expertly handcrafted tests.

Article Search Artifacts Available Article: oopslab26main-p152-p doi:10.1145/3839453

Seeking Evidence of Further Optimization: Detecting Missed Optimizations through Compiler’s Native Analyses
Yi Zhang, Yu Wang, Ke Wang, and Linzhang Wang
(Nanjing University, China)
Compilers are central to software performance, yet even mature optimization pipelines such as LLVM's and GCC's often miss optimization opportunities. Existing approaches for detecting missed compiler optimizations are constrained by the challenge of reliably determining whether a specific optimization has been applied, leading to a fundamental weakness in their ability to generalize to real-world software.
This paper presents a new perspective for detecting missed compiler optimizations. The key idea is utilizing compiler's native analyses to directly examine the compiler's optimized output and identify code regions that remain further optimizable---evidence that some optimization opportunities were missed. We develop two strategies to realize this idea: one that queries analyses independent of the missed optimization, effectively leveraging their otherwise unused reasoning results, and another that rewrites code into semantics-preserving forms to activate otherwise incompatible analyses.
We conduct an extensive evaluation of our approach on LLVM using all 219 projects from LLVM Opt Benchmark, a suite used by LLVM developers to measure the performance impact of compiler updates on real-world software. Across these programs, our tool discovers 31,616 missed optimization opportunities. By analyzing them, we have identified and reported 25 issues to LLVM developers; 20 have already been patched or confirmed. Applying LLVM official patches to our reported issues consistently yielded runtime speedups of up to 12.96% for affected software and compile-time reductions of up to 7.55%.

Article Search Article: oopslab26main-p182-p doi:10.1145/3839454

Beyond Nominality: Faster Rapid Type Analysis in the Presence of Structural Subtyping
Elton Pinto and Milind Chabbi
(Georgia Institute of Technology, USA; Uber Technologies, USA)
Rapid Type Analysis (RTA) is an important algorithm used in constructing whole-program call graphs. RTA occupies a special middle ground between precision and speed, making it an algorithm of choice for many industry-scale downstream program analysis tasks. RTA’s core subtyping query, which asks whether a concrete type 𝐶 implements an interface 𝐼, is cheap under nominal subtyping: the implements relation is syntactically expressed and hence resolved in constant time.
Under structural subtyping, however, the hierarchy is implicit and must be computed by comparing method sets. RTA discovers types incrementally during its fixed-point iteration, and the naive approach checks each newly discovered concrete type (interface type) against all known interface types (concrete types) so far. The resulting analysis performs a number of “implements” calls equal to the product of the total number of concrete (|𝐶|) and interface (|𝐼|) types (𝑂(|𝐶|×|𝐼|)). For large programs in languages with structural subtyping, such as Go, the RTA algorithm is less effective at rapidly finding these relationships, slowing call graph construction.
We present Kumo, an improvement to the RTA algorithm that addresses its weaknesses in structurally typed languages. With Kumo, we solve the aforementioned problem with two techniques: first, we reduce the work overhead of discovering subtypes using a purpose-built method index technique, and second, we efficiently parallelize the algorithm to achieve high speedups. The method index exploits a necessary condition of structural subtyping—matching types must share at least one method name—to restrict each implements check to a small set of plausible candidates, reducing the check count to near-linear in practice. The parallelization exploits the fixed-point iteration of RTA while guaranteeing correctness via a subtle event ordering; fine-grained synchronization ensures scalability.
We evaluate Kumo on an industrial corpus of 969 Go services at Uber. Relative to Go’s unmodified standard-library RTA, Kumo achieves a median speedup exceeding 116×with peaks reaching 268×, using 64 workers. Kumo is being used in Uber’s CI systems on every code diff, and the speedups translate to reducing the most expensive graph construction step from 40 minutes to under 15 seconds using 64 parallel workers on large programs. While evaluated on Go, the technique applies to any language with structural subtyping.

Article Search Article: oopslab26main-p257-p doi:10.1145/3839455

A Type System for Optimizing Dynamic IFC
Daniel Galán Pascual, François Hublet, Srđan Krstić, Roman Fischer, Colin Pfingstl, and David Basin
(ETH Zurich, Switzerland)
Dynamic information-flow control (IFC) enforces confidentiality policies at runtime by tagging values with security labels and blocking policy-violating outputs by terminating the running system. Pervasive label tracking and enforcement checks incur high runtime costs, which limits practical IFC deployment to performance-insensitive workloads. We present a novel alternative called MinIF, a type-directed program transformation that statically eliminates the overhead of dynamic IFC for existing systems.
The central contribution of MinIF is a flow-sensitive type system that tracks which sensitive inputs influence a value and whether the enforcement mechanism would accept operations on it, even though the enforced policy is unknown to the type system. Using the type system, MinIF statically predicts enforcement outcomes and removes redundant checks along with the label-tracking code that served them, and we prove that the optimized program preserves both the behavior and the enforcement decisions of the original. For IFC systems with introspection, the optimization is fully automatic, as the introspection queries already present in the program supply all the permission information MinIF needs, with no programmer annotations. Unresolved checks surface as warnings, and the absence of warnings gives developers a static guarantee against enforcement-induced system termination.
We evaluate MinIF on Python programs running on the WebTTC dynamic IFC platform. On benchmarks, MinIF eliminates between 13% and 99% of the enforcement overhead, and compute-intensive workloads that time out under enforcement now complete in milliseconds.

Article Search Article: oopslab26main-p292-p doi:10.1145/3839456

Automatically Generating ML Compiler Backends from Tensor Accelerator ISA Descriptions
Devansh Jain, Akash Pardeshi, Marco Frigo, Kaustubh Khulbe, Krut Patel, Saatvik Lochan, Jai Arora, and Charith Mendis
(University of Illinois at Urbana-Champaign, USA; NVIDIA, USA)
Machine learning (ML) compilers play a key role in enabling high-performance implementations of ML workloads. These compilers use existing CPU and GPU backends to generate device-specific code. In recent years, many tensor accelerators (or AI accelerators) have been designed to further accelerate these workloads, with commercial products like AWS Trainium publicly available. However, compared to commodity hardware, a majority of tensor accelerators do not have mature ML compiler backends with robust code generation support. Moreover, tensor accelerator designs are subject to fast iteration cycles, making it difficult to manually develop and maintain ML compiler backends. Therefore, to enable faster integration of novel tensor accelerator designs in ML infrastructure, we need to make the compiler backend construction process more agile.
In this paper, we introduce ACT, a compiler backend generator that automatically generates compiler backends for tensor accelerators, given just the instruction set architecture (ISA) descriptions. These backends are integrated with XLA, a production ML compiler. ACT uses a novel ISA-parameterized compilation algorithm to generate a compiler backend with an equality-saturation-based instruction selection phase and a constraint-programming-based memory allocation phase. We generated compiler backends for 6 accelerator platforms from industry (e.g., AWS Trainium, Intel AMX) and academia (e.g., Gemmini). We showed that these generated backends match or outperform commercial compiler backends and expert-written kernel libraries, while maintaining low compilation overheads. Notably, ACT-generated backend for AWS NKI ISA improved the code generation coverage for AWS Trainium by 2.3x compared with AWS’s production compiler, neuronx-cc.
ACT is part of a larger open-source ecosystem, built around our ISA description language TAIDL, that automatically generates essential software tools, such as test oracles and compiler backends, from ISA descriptions of tensor accelerators. Our tooling has been adopted by multiple academic and industry teams designing novel tensor accelerators. The ecosystem is available at https://github.com/act-compiler/act.

Article Search Artifacts Available Article: oopslab26main-p309-p doi:10.1145/3839457

Compiling Quantum Regular Language States
Armando Bellante, Reinis Irmejs, Marta Florido-Llinàs, María Cea Fernández, Marianna Crupi, Matthew Kiser, and J. Ignacio Cirac
(Max Planck Institute of Quantum Optics, Germany; Munich Center for Quantum Science and Technology, Germany; TU Munich, Germany; IQM Quantum Computers, Germany)
State preparation compilers for quantum computers typically sit at two extremes: general-purpose routines that treat the target as an opaque amplitude vector, and bespoke constructions for a handful of well-known state families. We ask whether a compiler can instead accept simple, structure-aware specifications while providing predictable resource guarantees. We answer this by designing and implementing a quantum state-preparation compiler for regular language states (RLS): uniform superpositions over bitstrings accepted by a regular description, and their complements. Users describe the target state via (i) a finite set of bitstrings, (ii) a regular expression, or (iii) a deterministic finite automaton (DFA), optionally with a complement flag. By translating the input to a DFA, minimizing it, and mapping it to an optimal matrix product state (MPS), the compiler obtains an intermediate representation (IR) that exposes and compresses hidden structure. The efficient DFA representation and minimization offloads expensive linear algebra computation in exchange of simpler automata manipulations. The combination of the regular-language frontend and this IR gives concise specifications not only for RLS but also for their complements that might otherwise require exponentially large state descriptions. This enables state preparation of an RLS or its complement with the same asymptotic resources and compile time, which to our knowledge is not supported by existing compilers. We outline two hardware-aware backends: SeqRLSP, which yields linear-depth, ancilla-free circuits for linear nearest-neighbor architectures via sequential generation, and TreeRLSP, which achieves logarithmic depth on all-to-all connectivity via a tree tensor network. On the theory side, we prove circuit-depth and gate-count bounds that scale with the system size and the maximal Schmidt rank of the target state, and we give compile-time bounds that expose the benefit of the initial DFA representation. We implement the full pipeline and evaluate it on Dicke and W states, random uniform superpositions, and complement states, comparing against general-purpose, sparse-state, and specialized baselines.

Article Search Artifacts Available Article: oopslab26main-p331-p doi:10.1145/3839458

MGQL: An Executable, Small-Step Semantics of GQL
Aditya Thimmaiah, Tong-Nong Lin, and Milos Gligoric
(University of Texas at Austin, USA)


Article Search Article: oopslab26main-p337-p doi:10.1145/3839459

Incremental Program Synthesis from Event Logs
Jinwoo Kim, Victor Nicolet, Joey Dodds, and Loris D'Antoni
(University of California at San Diego, USA; Amazon, USA)
The goal of program synthesis is to enable non-expert users to write programs by providing a specification instead of an implementation. To truly realize this goal, the specification must require no expertise and no effort to generate. We consider the problem of synthesizing automation scripts from only the logs that are automatically collected by many systems. Using our approach, users can automate tasks they usually perform manually, without having to know how to program them.
Because logs are collected automatically, the synthesis approach needs to scale to large sets of logs. We present a new algorithm to solve this task by incrementally extending an API-calling script with behavior exemplified by a sequence of log events, adding one sequence at a time. By minimizing the program modifications at each step, we preserve user intent and synthesize a program as general as possible. We show that our approach, implemented in a tool LogLoom, scales to synthesis tasks with more traces and more complex programs than existing techniques. LogLoom synthesizes scripts that are identical to reference solutions for 60 out of 72 benchmarks, compared to 14 for an existing symbolic approach and 39 for an LLM.

Article Search Article: oopslab26main-p363-p doi:10.1145/3839460

EUFⁿ: A Decidable Extension to the Theory of Equality with Uninterpreted Functions
Yide Du, Zhenbang Chen, Weijiang Hong, and Wei Dong
(National University of Defense Technology, China)
The theory of Equality with Uninterpreted Functions (EUF) is fundamental to constraint solving and program verification. Uninterpreted functions abstract concrete implementations, enabling generalization and simplification of theorems and proofs. However, standard EUF restricts function composition to fixed finite depths (e.g., f^k(x) where k is constant). This work extends EUF to EUFⁿ, supporting parametric composition depth for unary functions (e.g., fⁿ(x) where n is a natural number variable).
An EUFⁿ formula can be viewed as a disjunction of infinitely many EUF formulas, each instantiated by an assignment of natural numbers. Its satisfiability is defined by the satisfiability of at least one such instantiated EUF formula. We establish the decidability of the EUFⁿ satisfiability problem via a conditional congruence graph (CCG) algorithm. This approach generalizes the standard congruence closure procedure by maintaining conditional equivalence relations between terms. The algorithm reduces the satisfiability problem to deciding existential sentences in Presburger arithmetic with divisibility, which is a decidable problem, thereby yielding a decision procedure for the quantifier-free fragment of EUFⁿ with a 2NEXPTIME complexity upper bound.
The enhanced expressiveness of EUFⁿ enables new applications: (1) Encoding a decidable subclass of interleaved Dyck reachability problems where existing over/under-approximations produce false positives/negatives, and (2) Encoding a new decidable subclass of uninterpreted program verification problems.

Article Search Article: oopslab26main-p402-p doi:10.1145/3839461

Sound State Encodings in Translational Separation Logic Verifiers
Hongyi Ling, Thibault Dardinier, Ellen Arlt, and Peter Müller
(ETH Zurich, Switzerland; EPFL, Switzerland; MPI-SWS, Germany)
Automated program verifiers are often organized into a front-end, which encodes an input program into an intermediate verification language (IVL), and a back-end, which proves that the IVL program is correct. Soundness of such translational verifiers requires that the back-end verification is sound and that correctness of the IVL program implies correctness of the input program. Existing formalizations for translational verifiers based on separation logic target the former, but support the latter only under the strong assumption that there exists a separation logic for the input program with the same state model as the IVL. This assumption is unrealistic in practice, especially since the state model also defines the supported separation logic resources.
We present the first formal framework for proving the soundness of translational separation logic verifiers with non-trivial state encodings. To be applicable to various front-ends and IVLs, our framework only assumes the existence of a homomorphic encoding relation between the front-end and IVL state models. At the core of our framework is a novel condition, backward satisfiability, which is crucial to guarantee the soundness of the front-end translation. We formalize our framework for front-end verifiers based on concurrent separation logic and separation logic IVLs, such as Raven, VeriFast, and Viper. We demonstrate its expressiveness by proving soundness for three common state encodings. Our framework and all proofs are formalized in Isabelle/HOL.

Article Search Artifacts Available Article: oopslab26main-p403-p doi:10.1145/3839462

Quantum Monte Carlo Estimation via Probabilistic Programming
Seungmin Jeon, Jaeho Choi, Jonguk Jeon, Kanguk Lee, Kyeongmin Cho, Sukyoung Ryu, and Jeehoon Kang
(KAIST, Republic of Korea; HyperAccel, Republic of Korea; Rebellions, Republic of Korea; FuriosaAI, Republic of Korea)
Monte Carlo methods are fundamental to finance, system verification, and scientific simulation, but converge slowly: achieving an additive error of є requires O(1/є²) samples. Quantum Amplitude Estimation (QAE) offers a quadratic speedup by encoding the target probabilistic model into a quantum circuit. However, constructing such a circuit demands low-level quantum expertise, and existing tools for this task all sacrifice at least one of generality, usability, or efficiency.
To address these, we design QPPL (Quantum Probabilistic Programming Language), a simple imperative language, and a compiler that translates probabilistic programs into quantum circuits. The key insight is that the circuit construction amounts to specifying a probability distribution, precisely the task that probabilistic programming addresses. QPPL achieves generality by supporting joint distributions, conditional updates, dynamic probabilities, and real-valued expectations in a single language; usability by offering a sequential, imperative syntax with named variables and direct arithmetic that hides all quantum details; and efficiency by modularly compiling each construct into reversible circuit primitives, achieving scalable circuit synthesis. We prove that the compilation is semantics-preserving. On benchmarks spanning finance and probabilistic model checking, QPPL is the only tool that covers all benchmarks, while producing circuits with up to 8.8× fewer gates and 26× shallower depth than existing tools.

Article Search Artifacts Available Article: oopslab26main-p411-p doi:10.1145/3839463

Revisiting Path Coverage Tracing from a Node-Centric View
Heqing Huang and Zhendong Su
(City University of Hong Kong, China; ETH Zurich, Switzerland)
Path coverage tracing is one of the fundamental components for supporting a wide range of dynamic program analyses, such as testing, debugging, profiling, and many others. Since one needs to insert code into a program to trace its coverage, runtime overhead becomes the main bottleneck for scalability. As finding the minimum number of instrumentation points is NP-hard, extensive work has focused on reducing the number of instrumented edges under diverse assumptions, and thus suffers from the trade-off between precision and efficiency. Departing from this edge-centric view, we introduce, in this work, a novel perspective, namely the node-centric view, where we aim to find the minimum number of blocks, rather than edges as in existing work, that can differentiate all edges and paths in the program. This new perspective allows us to design a linear-time algorithm that is provably correct and optimal—it finds the minimum set of blocks for correctly differentiating edge/path coverage for arbitrary control-flow graphs. Our key insight is that optimal node-level instrumentation only needs to distinguish undifferentiated paths at the block where they converge, enabling our algorithm to have linear-time complexity regarding the number of basic blocks. We implement our algorithm as InsOpt and compare it against state-of-the-art edge-coverage instru- mentation techniques on the real-world vulnerability-detection benchmark, Magma. Our evaluation results demonstrate significant improvements: InsOpt needs 2.8x less instrumentation with only 17% basic blocks instrumented. This reduced instrumentation yields a 1.6x speedup and a substantial 2.4x reduction in runtime overhead. Moreover, we also demonstrate substantial potential for InsOpt across other applications. Specifically, our integration of InsOpt with AFL++, a state-of-the-art fuzzer, shows a 5.0x speedup in vulnerability detection and a 1.5x performance improvement. Notably, this efficiency gain further benefits InsOpt in detecting five previously unknown bugs in frequently evaluated projects by other state-of-the-art tools.

Article Search Artifacts Available Article: oopslab26main-p456-p doi:10.1145/3839464

A Formal Account of the Wasm 3.0 Concurrency Model
Azalea Raad, Michalis Kokologiannakis, Viktor Vafeiadis, and Conrad Watt
(Imperial College London, UK; ETH Zurich, Switzerland; MPI-SWS, Germany; Nanyang Technological University, Singapore)


Article Search Article: oopslab26main-p501-p doi:10.1145/3839465

Implementing Set-Theoretic Types
Mickaël Laurent and Kim Nguyễn
(Charles University, Czech Republic; Université Paris-Saclay, France)
Set-theoretic types provide a rich type algebra that supports unrestricted unions, intersections, and negations, together with a decidable type constraint-solving algorithm known as tallying. These types are particularly well suited for typing dynamic languages, where functions often exhibit both generic and overloaded behavior. However, the complexity of their implementation has hindered their widespread adoption. In this paper, we introduce a modular representation for set-theoretic types and revisit the algorithms for subtyping and tallying. We compare our approach with the historical CDuce implementation and evaluate the performance impact of some optimizations and design choices.

Article Search Artifacts Available Article: oopslab26main-p532-p doi:10.1145/3839466

Commit-Window Observation Contracts for Reactive Entity-Component Systems
Tomoyuki Aotani and Tetsuo Kamina
(Sanyo-Onoda City University, Japan; Oita University, Japan)
Modern entity-component systems (ECS) runtimes expose structural events (OnAdd, OnSet, and OnRemove), change filters, and continuous queries (CQ) so that systems rerun only where data changed; yet the correctness of the underlying optimizations—coalescing notifications, reordering write-disjoint updates within a commit window, caching CQ membership, iterating to quiescence—has lacked a semantics that states the required commit-window observation contract.
We present RxTCoreECS, a calculus that formalizes this contract for reactive ECS by integrating a Core-ECS store-and-scan baseline with a reactive transactional layer. Its key design point is an explicit two-tier notification model: (i) an eventful commit that emits a sequential per-operation trace, and (ii) a net-effect commit that emits a per-cell delta (at most one event per cell per commit window). The target contract is intentionally windowed: observers are order-insensitive within a commit window, and Changed is a dirty-by-write post-membership filter rather than a semantic-equality test. We define a window-local observational equivalence, relative to the incoming queue prefix, that quotients event order only within one commit window, prove schedule independence under write-disjointness, and connect the two layers by a coalescing refinement and a forward simulation theorem. We add a CQ-cache model with correctness lemmas for Added/Removed/Changed deltas, an explicit version/filter alignment theorem exposing the once-per-window bump policy for touched entities and cells, and a fuel-bounded quiescence loop. We prove a reusable all-dirty scan-closure schema under explicit round-refinement and stability obligations. All formal definitions and named results in the paper are mechanized and checked in Rocq.

Article Search Article: oopslab26main-p538-p doi:10.1145/3839467

Towards Concise Binding Semantics of Late-Bound OOP Systems
Joel Jakubovic
(Charles University, Czech Republic)
Smalltalk and Self are two paradigmatic examples of class-based and prototype-based late-bound object-oriented programming, respectively. Many of their similarities and differences can be grounded in how they bind message names to concrete values, but the details can be subtle and are not available in a concise form. The Id object model abstracts over specific binding semantics, even permitting the flexibility of late-bound message sending as part of binding semantics, so it is worth using as a common basis on which to compare them. In this paper, we present the method-binding semantics of Smalltalk and Self as different “special cases” within the Id object model.

Article Search Article: oopslab26main-p555-p doi:10.1145/3839468

Prosecutor: Bayesian Counterfactual Fault Localization
Sara Baradaran, Yifei Huang, Wei Le, and Mukund Raghothaman
(University of Southern California, USA; Iowa State University, USA)
Bayesian reasoning has emerged as a promising approach to fault localization, where the introduction of errors and their subsequent propagation through faulty executions is treated as a stochastic process. One can then perform Bayesian inference on a probabilistic model encoding the program execution to associate individual statements and values with a posterior probability of being erroneous. In this paper, we propose a new graph representation that effectively models error propagation through failing program executions. This structure, which we call the Error Propagation Graph (EPG), extends prior probabilistic approaches by incorporating richer inter-procedural relationships and accounting for the influence of unexplored control-flow branches that may affect variable values. We also show how EPGs can be constructed efficiently and compactly, and how this structure enables the selection of a set of counterfactual experiments, each involving artificially flipping a suspicious branch predicate at runtime and observing its downstream effect on the test outcome. The results of these experiments provide additional evidence that can be incorporated into the EPG to confirm or refute the model's initial suspiciousness estimates. We have implemented this technique in a tool named Prosecutor and evaluated it on 470 buggy versions of 13 projects from the Defects4J benchmark suite. Our experimental evaluation shows that Prosecutor places 40% of the true fault locations within its top-3 predictions. The technique also significantly outperforms a diverse set of baselines by identifying at least 10%, 11%, 15%, and 19% more buggy statements than each of the baselines in its top-1, top-3, top-5, and top-10 predictions, respectively.

Article Search Artifacts Available Article: oopslab26main-p559-p doi:10.1145/3839469

Equivalence Checking of ML GPU Kernels
Benjamin Driscoll, Kshitij Dubey, Anjiang Wei, Neeraj Kayal, Rahul Sharma, and Alex Aiken
(Stanford University, USA; Microsoft Research, India; Google DeepMind, India)
With the rapid progress of deep learning and large language models (LLMs), companies spend enormous sums executing GPU kernels. These kernels have become prime targets for aggressive optimization. Recent efforts increasingly leverage LLMs to generate GPU kernels, but make no formal guarantees about the generated kernels. We present the first equivalence checker for GPU kernels and use it to formally verify the correctness of machine learning (ML) kernels optimized by hand, by LLM, and by compiler. We show that our equivalence checker is sound and, for a well-defined class of GPU kernels which includes many programs of interest, complete. Our implementation, VOLTA, can verify ML computations such as convolutions, matrix multiplications, and various attention mechanisms.

Article Search Artifacts Available Article: oopslab26main-p562-p doi:10.1145/3839470

Semantics for 2D Rasterization
Bhargav Kulkarni, Henry Whiting, and Pavel Panchekha
(University of Utah, USA)
Rasterization is the process of determining the color of every pixel drawn by an application. Powerful rasterization libraries like Skia, CoreGraphics, and Direct2D put exceptional effort into drawing, blending, and rendering efficiently. Yet applications are still hindered by the inefficient sequences of instructions that they ask these libraries to perform. Even Google Chrome, a highly optimized web browser co-developed with the Skia rasterization library, still produces inefficient instruction sequences even on the top 100 most visited websites. The underlying reason for this inefficiency is that rasterization libraries have complex semantics and opaque and non-obvious execution models.
To address this issue, we introduce μSkia, a formal semantics for the Skia 2D graphics library, and mechanize this semantics in Lean. μSkia covers language and graphics features like canvas state, the layer stack, blending, and color filters, and the semantics itself is split into three strata to separate concerns and enable extensibility. We then identify four patterns of sub-optimal Skia code produced by Google Chrome, and then write replacements for each pattern. μSkia allows us to verify that the replacements are correct, including identifying numerous tricky side conditions. We then develop a high-performance Skia optimizer that applies these patterns to speed up rasterization. On 139 Skia programs gathered from the top 100 websites, this optimizer yields a speedup of 1.12× over Skia's most modern GPU backend, while taking just 0.03 ms for optimization. The speedups persist across a variety of websites, Skia backends, and GPUs. To provide true, end-to-end verification, optimization traces produced by the optimizer are loaded back into the μSkia semantics and translation validated in Lean.

Article Search Artifacts Available Article: oopslab26main-p563-p doi:10.1145/3839471

SPONGE: Adaptive Boundary-Anchored Indexing for Online Value-Flow Queries
Sixiang Peng, Chenyang Sun, Wei Chen, Bowen Zhang, and Charles Zhang
(Hong Kong University of Science and Technology, China)
The application of high-precision value-flow analysis is experiencing a paradigm shift from planned executions to online ad hoc queries driven by human auditors and AI agents. However, existing techniques struggle in this interactive setting: exhaustive offline tabulation is fundamentally intractable, while memoryless online search suffers from redundant exploration and SMT invocations. To bridge this gap, we propose SPONGE, a novel two-phase framework that accelerates ad hoc queries through boundary-anchored indexing. Offline, SPONGE employs an adaptive-depth strategy to selectively precompute feasible value-flow segments at critical procedure boundaries, optimizing SMT allocation based on traversal probability and search space complexity. Online, it utilizes an index-guided push-down search with lazy expansion to dynamically stitch these pre-verified segments, effectively bypassing redundant state exploration and pruning unsatisfiable paths. We evaluated SPONGE on 9 C/C++ projects (up to 3.8 million LoC). Results demonstrate that SPONGE drops the 95th-percentile online query time from nearly 270 s to under 50 s compared to a baseline search. Furthermore, the adaptive strategy reduces offline indexing time by 75% over a uniform approach, amortizing the offline cost in fewer than 300 queries for workloads dominated by complex queries.

Article Search Artifacts Available Article: oopslab26main-p565-p doi:10.1145/3839472

Uncovering Hidden Memory Costs for Garbage Collection
Sudhanshu Agarwal and Saugata Ghose
(University of Illinois at Urbana-Champaign, USA)


Article Search Article: oopslab26main-p590-p doi:10.1145/3839473

Classifying Capabilities
Cao Nguyen Pham, Oliver Bračevac, Yichen Xu, Yaoyu Zhao, and Martin Odersky
(EPFL, Switzerland)
Capture checking in Scala 3 enables lightweight and practical effect and resource tracking by recording capabilities in types. However, the system offers no way to reason about kinds of capabilities. Natural constraints such as “retaining only the control-flow capabilities of this closure” or “excluding all thread-local capabilities from this argument” become inexpressible. Both arise in the Scala 3 standard library: Try re-throws caught exceptions, so it retains only the control-flow capabilities of its body, and Future must not capture thread-local resources. The inability to state these constraints has kept parts of the library outside capture checking.
We introduce capability classifiers: a tree-structured, user-extensible hierarchy of tags that classify capabilities by their semantic role. Projections filter capture sets by classifier, supporting both inclusion (c.only[C]) and exclusion (c.except[C]). The tree structure enables decidable disjointness reasoning: classifiers on separate branches are guaranteed to be disjoint regardless of unknown extensions elsewhere in the hierarchy. We formalize classifiers as an extension of System Capless, a core calculus for capture checking, introducing a classifier kind algebra based on intersection, union, and subtraction of classifier subtrees. We extend the operational semantics to model exception interception and establish type safety, effect safety, and handler coverage via a big-step proof, fully mechanized in Lean 4. Classifiers are implemented in the Scala 3 capture checker, and we demonstrate their use on standard library types and real-world effect exclusion patterns.

Article Search Artifacts Available Article: oopslab26main-p593-p doi:10.1145/3839474

Verifying Economic Security of Smart Contracts via Unintended Return
Yi Rong, Xupeng Li, and Ronghui Gu
(Columbia University, USA; CertiK, USA)
We propose CMod, an economic model for analyzing the economic security of decentralized finance (DeFi) smart contract code. CMod defines the notions of economic value, intended-return conditions, and unintended single-transaction return, and reasons about economic security by proving the absence of unintended single-transaction return. Based on CMod, we co-design CSol, an automated verification tool for Solidity that reasons about path properties in multi-contract environments via bounded symbolic execution. CSol incorporates three categories of optimizations: CMod-oriented path pruning and inductive verification, proof-goal simplification, and solver acceleration. Our evaluation shows that CMod and CSol can be applied to real-world contract code and characterize economically exploitable vulnerabilities. CSol verifies 245 real-world contracts, identifies 6 live scam contracts, detects 16 of 18 real-world exploits and 92 of 104 audit-stage findings, and exposes one misidentification in an existing tool's benchmark.

Article Search Article: oopslab26main-p625-p doi:10.1145/3839475

SmartFuzz: Leveraging Large Language Models and Feature Composition to Generate High-Quality Seeds for Database Fuzzing
Li Lin, Jintai Hong, Yanlin Zhuang, and Rongxin Wu
(Xiamen University, China)
Mutation-based fuzzing is one of the most effective techniques for uncovering bugs in Database Management Systems (DBMSs). However, its effectiveness critically depends on the quality of the initial seed queries. High-quality seeds should be syntactically and semantically valid, incorporate diverse SQL features, and encode behaviors that drive execution into bug-prone states. In practice, existing DBMS fuzzers primarily rely on SQL queries extracted from unit tests or regression suites as initial seeds, which are often limited in diversity and scale, leaving many DBMS features and execution paths unexplored. To address this limitation, we propose SmartFuzz, an automated framework for synthesizing high-quality initial SQL seeds for mutation-based DBMS fuzzing using Large Language Models (LLMs). The key insight behind SmartFuzz is that two underutilized sources---official DBMS documentation and historical crash-triggering inputs---capture complementary knowledge about DBMS feature usage and bug-relevant behaviors. SmartFuzz extracts structured features from these sources and leverages LLMs to synthesize executable, feature-rich SQL seeds that are biased toward bug-prone execution states. We integrate SmartFuzz into existing mutation-based DBMS fuzzing pipelines and evaluate it on 4 widely used DBMSs. The results demonstrate that SmartFuzz significantly improves bug discovery and code coverage compared to state-of-the-art mutation-based fuzzers. In total, SmartFuzz detects 61 previously unknown bugs, of which 60 have been confirmed and fixed by developers.

Article Search Article: oopslab26main-p630-p doi:10.1145/3839476

When Do Staging Annotations Preserve Semantics? Mechanizing the Metatheory of Automatic Let-Insertion in Typed Multi-stage Programming
Jun Tan and Guannan Wei
(Independent, China; Tufts University, USA)


Article Search Article: oopslab26main-p633-p doi:10.1145/3839477

Composing CRDTs Convergent by Construction
Alexander Städing Dominguez, George Zakhour, Pascal Weisenburger, and Guido Salvaneschi
(University of St. Gallen, Switzerland)


Article Search Article: oopslab26main-p636-p doi:10.1145/3839478

Pyriscope: Precise and Low-Overhead Python Control Flow Tracing via Sparse Hardware-Based Events
Xinchen Yao, Wu Daiyou, and Zhiqiang Zuo
(Nanjing University, China)
Capturing the control-flow and/or coverage profiles of Python code becomes a pressing need for Python development community, which is commonly used in a wide spectrum of tasks including program testing/fuzzing, debugging, understanding, and optimizations. Existing tracing approaches either suffer from prohibitively high overhead or only collect approximate information, which cannot satisfy the practical requirements. In this paper, we propose to leverage modern hardware tracing modules to achieve precise and low-overhead control-flow tracing for Python programs. To this goal, we develop Pyriscope on top of CPython runtime by integrating the effective trace pruning and efficient analysis techniques. Evaluation results demonstrate the efficacy of our system. It incurs an average overhead of only 2.99% for rich-informative control-flow tracing, which is orders of magnitude smaller than that of the state of the arts.

Article Search Article: oopslab26main-p649-p doi:10.1145/3839479

Augur: Predicting View Serializability Violations in Relational Data Store Applications
Chujun Geng, Noah Charlton, Spyros Blanas, Michael D. Bond, and Yang Wang
(Ohio State University, USA)
Relational data stores are widely used because they provide persistence, scalability, and fault tolerance with a simple interface. However, most data store applications configure the data store to use weak isolation for scalable performance, permitting sporadic unserializable executions that produce incorrect results or failures. Prior work uses dynamic predictive analysis to infer violations from execution traces, but existing techniques cannot handle relational (i.e., SQL) queries with complex predicates, and they predict executions that do not violate View Serializability, leading to false negatives and false positives.
This paper introduces Augur, the first dynamic predictive program analysis that (1) supports data store applications with complex relational queries and (2) reports only executions that violate View Serializability. The evaluation demonstrates that Augur finds feasible, unserializable executions in OLTP-Bench programs and in the widely used e-commerce application Spree.

Article Search Article: oopslab26main-p659-p doi:10.1145/3839480

CapOpt: Capability-Aware Superoptimization for Secure and Provably Faster Code
Xiaoyang Sun, Dejice Jacob, Huanting Wang, Jeremy Singer, and Zheng Wang
(University of Leeds, UK; University of Glasgow, UK)
Superoptimization is a powerful code optimization technique that generates optimized instruction sequences by exploring the space of instruction-level transformations. However, existing superoptimizers assume that pointers and integers are interchangeable, an assumption that no longer holds in memory-security-enhanced architectures like CHERI, where pointers are represented as metadata-rich capabilities with enforced bounds, permissions, and provenance. This semantic change breaks many traditional optimizations and forces CHERI compilers to adopt conservative strategies that sacrifice performance for safety. We present CapOpt, the first superoptimization framework that explicitly incorporates capability semantics into both its search space and correctness model. CapOpt introduces Provenance-Guided Stratified Synthesis (PGSS), a synthesis strategy that structures the search space around capability-aware abstractions and uses provenance-based reasoning to eliminate unsafe transformations. We also define a capability-aware equivalence model that extends conventional functional correctness to include metadata integrity. We evaluated CapOpt on an ARM-based CHERI hardware platform and the CHERI-RISC-V simulator. Experimental results show that CapOpt improves performance by up to 4.1% over the existing CHERI-LLVM toolchain, while strengthening security by tightening pointer bounds and permissions.

Article Search Article: oopslab26main-p664-p doi:10.1145/3839481

Relight: Simple User-Level Checkpointing and Fast-Forward Replay for Distributed Task-Based Systems
Elliott Slaughter, Rupanshu Soi, Michael Bauer, and Alex Aiken
(SLAC National Accelerator Laboratory, USA; Stanford University, USA; NVIDIA Research, USA)
Checkpointing, or periodic saving of program state to storage, is the de facto standard technique used to mitigate risks of nondeterministic bugs, hardware faults, and job wall-time limits in long-running programs. Traditional approaches require users to manually manage the migration of data to and from storage when capturing checkpoints and when resuming execution. However, for task-based programs, where the user has already factored the computation into tasks and the program data into collections, sufficient information is available to automatically capture and resume from checkpoints with minimal code changes. We present Relight, the first framework for automatic, distributed checkpointing of task-based programs that provides an efficient fast-forward replay for full job recovery. On a set of already-optimized benchmarks, we demonstrate that Relight delivers checkpointing performance and scalability comparable to the original, unmodified codes when running on up to 512 nodes of the Piz Daint supercomputer.

Article Search Artifacts Available Article: oopslab26main-p680-p doi:10.1145/3839482

Symbolic Basic Block Profiling for Machine Learning Kernels
Jingyu Qiu, Rongcui Dong, and Sreepathi Pai
(University of Rochester, USA)
Current basic block profiling techniques obtain the count of executions of each basic block in a program using dynamic instrumentation. These profiling counters create runtime overheads and also require the execution of the program, which, for large input sizes, can take substantial time. We propose symbolic program profiling that generates symbolic formulae for a basic block’s count with inputs as the independent variables. Our technique is limited in applicability to a certain class of programs, namely machine learning (ML) kernels. We implement our technique in the LLVM compiler and evaluate it on 78 ML operators from 50 different ML models. These operators are generated by TVM, a machine learning compiler. Our symbolic profiles deliver exactly the same results as dynamic instrumentation for 73 out of 78 kernels with a median speedup of 15093×.

Article Search Artifacts Available Article: oopslab26main-p705-p doi:10.1145/3839483

Bringing Foundational Verification to Real-World Rust Code
Lennard Gäher, Vincent Lafeychine, Sascha Kehrli, Avraham Shinnar, Wojciech Ozga, Guerney Hunt, and Derek Dreyer
(MPI-SWS, Germany; Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria - LMF, France; IBM Research, USA; IBM Research Zurich, Switzerland)
Rust is a modern systems programming language that, thanks to its strong memory safety guarantees, is well-suited to the domain of safety-critical systems. Since memory safety alone is not ultimately enough for safety-critical systems, there have emerged in recent years a number of tools for deductive verification of functional correctness of Rust programs. One recent tool, RefinedRust, is notable in that it both handles unsafe pointer-manipulating Rust code and produces foundational, machine-checked proofs in the Rocq prover. However, RefinedRust is a prototype tool and lacks support for several of the high-level abstractions that Rust provides, including traits, closures, and iterators. These features are commonly used in real-world Rust code, and are supported by other non-foundational Rust verification tools like Prusti and Creusot.
In this paper, we show how to extend RefinedRust with these features, and in a manner such that they can be used in conjunction with unsafe code. We demonstrate its usefulness by verifying interesting parts of the memory subsystem of the real-world, low-level ACE security monitor, including its page allocator.

Article Search Artifacts Available Article: oopslab26main-p769-p doi:10.1145/3839484

Heap Abstraction via Early-Confluent Object Merging for Pointer Analysis
Jinpeng Wang, Yufei Liang, Zhongsheng Zhan, Tian Tan, and Yue Li
(Nanjing University, China)
Heap abstraction critically affects both the efficiency and precision of pointer analysis for Java programs. By merging heap objects allocated at different program points, heap abstractions can significantly improve analysis efficiency, but often at the cost of precision. Mahjong, a state-of-the-art heap abstraction based on object merging, demonstrates that object merging can substantially improve the efficiency of pointer analysis while preserving precision for type-dependent clients; however, this client-specific guarantee limits its general applicability. In this work, we investigate how to improve the efficiency of pointer analysis through object merging, while preserving precision in a manner independent of any particular client. Our key insight is that, from the perspective of pointer analysis, many heap objects exhibit early flow confluence: they are allocated at different program points and then quickly propagate to the same pointers (variables or fields), after which they continue to flow together through the program. Merging such early-confluent objects has negligible impact on overall analysis precision. In contrast, merging objects that do not flow to the same pointers, or that converge only much later, can introduce substantial precision loss.
Guided by this insight, we propose Valve, a new heap abstraction approach that efficiently identifies and merges early-confluent objects. Valve encodes the flow information needed for early-confluence detection as nondeterministic finite automata (NFAs) and approximates mergeability checking via an NFA-equivalence test, enabling efficient object merging while retaining high precision. We evaluate Valve on the largest benchmarks used in recent literature as well as modern large-scale Java applications, by integrating it with multiple state-of-the-art pointer-analysis techniques and directly comparing it with Mahjong. The results show that Valve achieves substantially higher precision than Mahjong for non-type-dependent clients, while maintaining comparable precision for type-dependent clients. At the same time, Valve delivers comparable or often better analysis efficiency across all evaluated cases. Overall, Valve, as a heap abstraction approach, significantly improves the efficiency of pointer analysis across several state-of-the-art techniques while maintaining high precision (99.61% on average).

Article Search Artifacts Available Article: oopslab26main-p770-p doi:10.1145/3839485

A Language Approach to Fine-Grained Microarchitectural Observation
Guokai Chen, Sergi Soler Arrufat, Clément Pit-Claudel, and Thomas Bourgeat
(EPFL, Switzerland)
Analyzing, understanding, and validating the performance of modern processors present significant challenges. These stem from two primary issues. First, it is difficult to construct “performance tests” that can test precisely scoped hypotheses about microarchitectural behavior. Second, it is difficult to make sense of performance measurements: hardware teams see too many low-level events that they struggle to map back to the tested programs, and software developers and security researchers can only observe coarse-grained performance counters. This paper addresses both challenges with a unified programming language approach that we prototype in a framework named HT.
To overcome the test-construction problem, our insight is that a broad range of microarchitectural effects are triggered by a specific software address layout. We introduce a DSL that enables specifying desired microarchitectural effects of a program through specifying its address layout, separately from its functional behavior. This separation is achieved using an SMT solver to compute a suitable instruction and data layout.
To overcome the observability challenge, we systematically link high-level software patterns down to raw hardware simulation outputs. We introduce flexible event-tracing constructs designed to construct custom, multi-cycle higher-level events from (single-cycle) low-level event logs, effectively acting as the bridge that connects software execution patterns to low-level hardware events.
We demonstrate HT’s utility on XiangShan, a production-grade open-source RISC-V processor, through three case studies: analyzing the performance impact of the Zicond RISC-V extension, reproducing subtle microarchitectural attacks, and characterizing the branch prediction behavior of Lua, an interpreted language.

Article Search Artifacts Available Article: oopslab26main-p772-p doi:10.1145/3839486

Direct Manipulation and Natural Language Programming, Together at Last?
Parker Ziegler, David Minh-Duy Cao, Justin Lubin, and Sarah E. Chasins
(University of California at Berkeley, USA)
Decades of programming languages research has contributed novel approaches to program editing that go beyond modifying text, including direct manipulation programming, structure editing, and automated refactoring tools. However, the rapid growth of natural language programming largely reinforces a view of programs as text and program editing as (unstructured) text transformation. How can we develop unified programming systems that bridge the gap between these approaches, supporting multiple editing paradigms in concert? And how would such systems change the way we program? We take a first step toward answering these questions by introducing a framework that enables program editing via both direct manipulation and natural language, and instantiate this framework in a variant of the cartokit direct manipulation programming system (cartokit_DM+NL). Our key insight is to treat programs as sequences of structured edits and to use an edit language as a shared interface for both direct manipulation and natural language interactions, leveraging constrained decoding to support the latter. Using our instantiation, we conducted a within-subjects study (N=18) to understand how the combination of direct manipulation and natural language as editing modalities changes the programming process compared to each modality alone. Perhaps surprisingly, we found that study participants overwhelmingly chose to edit via direct manipulation when both modalities were available, performing just 6.14% of edits via natural language. Our thematic analysis of study sessions revealed that direct manipulation aided task decomposition, encouraged incremental editing, and helped mitigate known challenges in natural language programming related to understanding model capabilities and interpreting model-generated code. Conversely, natural language editing came into play largely to automate, parameterize, and replay known edits that would otherwise be repeated tediously by hand. Our edit-based framework and study findings lay out a possible pathway for future research on programming systems that blend natural language with alternative editing modalities, building on the foundation of edit languages.

Article Search Artifacts Available Article: oopslab26main-p792-p doi:10.1145/3839487

Abductive Inference of Separation Logic Specifications with Isorecursive User-Defined Predicates and Magic Wands
Nicolas Klose and Peter Müller
(ETH Zurich, Switzerland)
Program verifiers based on separation logic, such as Gillian, VeriFast, and Viper, allow one to prove complex properties of heap-manipulating, concurrent programs. These tools automate a large part of the proof search, but require a substantial amount of annotations such as method pre- and postconditions and loop invariants. Inference techniques such as bi-abduction can alleviate this burden, but existing techniques are too restrictive to be used in expressive program verifiers. In particular, existing bi-abduction techniques do not support the magic wand connective, so that inference for iterative traversals of structures beyond list segments is limited. Moreover, they rely on an equirecursive interpretation of predicates, instead of the isorecursive interpretation used by most SMT-based verifiers.
In this paper, we present a novel abductive inference that addresses these limitations. It infers loop invariants that combine user-defined predicates with magic wands to keep track of the part of a data structure still to be traversed and the remainder of the data structure, such that ownership of the entire structure is retained after the traversal. Moreover, our abduction technique is the first to infer the auxiliary operations required by verifiers to manipulate predicates and wands.
We implemented our inference in Viper; our evaluation shows that our approach can infer over 80% of the specifications required to verify memory safety of a diverse benchmark set.

Article Search Artifacts Available Article: oopslab26main-p797-p doi:10.1145/3839488

Staged Multi-step UTXO Workflows via Recursive Invariants
Shuyang Tang, Sherman S. M. Chow, Hongfei Fu, Zihan Guo, and Guoqiang Li
(Shanghai Jiao Tong University, China; Chinese University of Hong Kong, Hong Kong; Shanghai University of Finance and Economics, China; Sun Yat-sen University, China)
Stateless UTXO-style execution validates transactions using local and referenced data, enabling parallel validation and predictable serialized-size/weight accounting. However, multi-step workflows must thread state across outputs, and a prepared next-step transaction may become stale when another valid spend confirms first. Explicit state threading therefore shifts consistency maintenance, off-chain tracking, and transaction rebuilding onto the protocol boundary, potentially increasing coordination cost, latency, transaction count, and fees. Recursive invariants (RIs), our proposed transaction-level logic and toolchain, address this gap by expressing workflow rules as transaction-level predicates over a transaction's inputs and a declared set of designated outputs. Modeled this way, an accepted spend of a designated output re-checks the same RI one step later, carrying the workflow rule forward without introducing application-level shared mutable state or executable logic attached to outputs. Accordingly, multi-step protocol rules preserve validation-time locality and admit explicit cost accounting, while cross-transaction guarantees arise from repeated one-step checking. Not all successor clauses are checkable when the current transaction is validated, so our small statically typed domain-specific language (DSL) uses three-valued semantics over true, false, unknown to defer future-dependent obligations until they become checkable. Co-designed with this DSL, our framework formalizes UTXO validation and ledger extension, identifies the validation-time-evaluable one-step fragment, and proves the deduction system sound with respect to the three-valued semantics. Here, we mechanize the soundness proof in the Coq/Rocq proof assistant. On the systems side, we implement a prototype RI interpreter and DSL toolchain with explicit byte and fee annotations. Workflows across six practice-motivated case studies exhibit linear cumulative overhead with a small per-step constant, while illustrating how RIs reduce ad hoc transaction constraint engineering and off-chain orchestration.

Article Search Artifacts Available Article: oopslab26main-p815-p doi:10.1145/3839489

Code–Test Co-translation: Towards Practical and Effective Program Migration in the Wild
Xitao Li, Xiaofei Xie, Jiang Wu, Ting Liu, and Haijun Wang
(Xi'an Jiaotong University, China; Singapore Management University, Singapore)
Program migration, which involves translating software systems from one programming language to another, is essential for modernizing legacy systems and improving maintainability. Recent large language models (LLMs) have demonstrated strong performance in code translation; however, existing methods and benchmarks still exhibit key limitations. (1) They primarily focus on simple, self-contained snippets that fail to capture the complexity of real-world programs, and (2) they often assume that target-language test cases are readily available for evaluation and feedback, an unrealistic assumption given the difficulty of manually creating equivalent tests across languages. In this paper, we argue for a more practical setting, termed the Code–Test Co-Translation (CTCT) problem, where both the program and its associated test suite should be jointly translated to preserve semantic and functional consistency. Through an empirical study on real-world programs, we identify two major challenges in CTCT: (1) the difficulty of measuring test-case consistency in the absence of ground truth, and (2) the ineffectiveness of existing iterative translation–repair strategies, which suffer from state degradation and poor initialization traps when handling complex, real-world features.
To address these issues, we propose CoTTrans, a state-quality–aware iterative translation–repair framework guided by a novel Test Case Consistency (TCC) metric. TCC quantifies both syntactic and semantic consistency between source and translated tests, enabling fine-grained feedback that drives LLM-based refinement. CoTTrans further integrates TCC with test pass rates to assess state quality and triggers adaptive backtracking when low-quality states are detected during the translation. Evaluated on the BigCodeBench dataset, CoTTrans improves the translation correctness score from 0.360 to 0.675 on DeepSeek-V3, substantially outperforming existing methods, while TCC demonstrates superior effectiveness in measuring test consistency compared with existing metrics. These results show that CoTTrans enhances translation stability and accuracy, establishing a practical foundation for reliable code–test co-evolution in real-world program migration.

Article Search Artifacts Available Article: oopslab26main-p830-p doi:10.1145/3839490

Transitive, Abstract, and Class Polymorphic Immutability
Aosen Xiong, Yudi Bai, Haifeng Shi, Lian Sun, Mier Ta, and Werner Dietl
(University of Waterloo, Canada)
State mutations can often lead to silent program errors, including broken invariants and security vulnerabilities. Object-oriented languages offer basic mechanisms to prevent mutation; however, enforcing desired guarantees remains challenging. Two such guarantees are transitive immutability, which disallows mutation of all objects reachable from a reference, and abstract immutability, which permits controlled mutation of otherwise immutable objects. Furthermore, introducing readonly references to support subtype polymorphism often complicates the soundness of the type system. The integration of immutability into a class hierarchy introduces challenges, primarily manifesting as duplicated code between mutable and immutable variants.
We present Precise Immutability for Classes and Objects (PICO), a type system that enforces transitive abstract immutability with readonly references. PICO introduces novel viewpoint adaptation rules to achieve transitivity. These rules prevent unsoundness caused by mutable and immutable cross-type aliasing, a long-standing issue for systems combining immutability and assignability. Additionally, PICO formally defines the abstract state, which allows developers to permit mutation for selected parts of the object graph. PICO provides four state-preservation guarantees within a single system by selecting corresponding viewpoint adaptation rules: abstract-, concrete-, readonly-, and transitive-state preservation. Finally, the system supports safe class mutability polymorphism: one class can express both mutable and immutable uses, avoiding duplicate mutable/immutable class variants while also enabling backward-compatible retrofitting of existing hierarchies.
We formalize PICO and prove its type soundness and four state-preservation guarantees in the Rocq proof assistant. We also implement a type checker for Java using the Checker Framework. We evaluate this implementation on the Java Collections Framework in OpenJDK 17 and other benchmarks, covering approximately 26,000 non-comment lines of code. The results demonstrate that PICO effectively enforces immutability guarantees and can successfully retrofit existing libraries without duplicating code.

Article Search Artifacts Available Article: oopslab26main-p835-p doi:10.1145/3839491

Sound Enforcement of Dynamic Release Information Flow Policy
Jeffrey Ching and Danfeng Zhang
(Duke University, USA)
Information flow analysis is the de facto method of assessing confidentiality and integrity issues. However, the widespread adoption of information flow analysis in real-world systems is still lacking, partly due to a fundamental gap between theory and practice: the dynamic nature of security concerns in real-world systems goes beyond the scope of existing techniques that assume a static policy (i.e., data secrecy does not change).
Recognizing the fundamental gap, a substantial amount of research has studied various aspects of it (e.g., enabling declassification, endorsement, and revocation policies). A recent work takes a step further by formalizing a promising end-to-end policy called dynamic release that unifies prior formalizations by allowing information flow restrictions to downgrade and upgrade in arbitrary ways. However, how to soundly enforce the powerful dynamic release policy is still an open question.
In this paper, we present the first type system that enforces dynamic release policy and formally prove its soundness. More specifically, we (1) formalize a core language that enables dynamic release policy, (2) develop a type system that checks dynamic release policy, (3) develop new proof techniques and formally prove that the type system enforces dynamic release policy, and (4) implement a prototype of the type system as an extension to the Rust language, along with case studies on a conference reviewing system and Civitas.

Article Search Artifacts Available Article: oopslab26main-p841-p doi:10.1145/3839492

Refined² Environment Classifiers
Yuito Murase and Atsushi Igarashi
(Kyoto University, Japan)
MetaML-style multi-stage programming (MSP) supports quasi-quotation-based code generation, runtime execution of generated code, and cross-stage persistence (CSP). However, its interaction with computational effects is subtle: mutable state can cause scope extrusion, where generated code escapes the scope of variables on which it depends.
This paper presents a type system for MetaML-style MSP with mutable state that statically rules out harmful scope extrusion while supporting multi-level code generation, runtime execution, and a variant of CSP. Our system builds on refined environment classifiers (RECs), a discipline that annotates code types with the variable scopes on which generated code depends. To scale RECs to the MetaML-style setting, we refine classifiers so that they track not only variable scopes, but also the scopes of classifiers themselves. Further, we integrated polymorphism over classifiers, enabling more general and reusable code generation patterns in a multi-level setting.
For the resulting system, we define an operational semantics via a definitional interpreter and prove type soundness and safety of offline code generation, showing that generated code can be extracted as standalone well-typed programs. We provide working implementations and mechanized proofs in Rocq.

Article Search Artifacts Available Article: oopslab26main-p847-p doi:10.1145/3839493

Fighting Supply Chain Attacks with Effect Systems
Magnus Madsen, Andreas Stenbæk Larsen, Jakob Schneider Villumsen, and Aslan Askarov
(Aarhus University, Denmark)
Today, most software is developed by building on packages, allowing developers to accelerate development. The proliferation of package dependencies creates a target-rich environment for malicious actors to hijack packages to inject malware, steal sensitive information, or cause destruction. Such supply chain attacks constantly threaten package ecosystems such as Cargo, npm, and Maven.
In this paper, we explore how to fight against such attacks by leveraging effect systems. While effect systems predict the behavior of software components, there is a practical gap between a programming language with an effect system and a programming language ecosystem that can use such effects to thwart attacks. To close this gap, we introduce a notion of an effect-safe package upgrade and develop an effect-aware package manager that enforces safety through effect lock files.
We extend the Flix programming language and its compiler toolchain with an effect-aware package manager. We evaluate the usefulness of the proposed effect-aware package manager with a case study of 51 supply chain attacks from the "Backstabbers Knife Collection" corpus of malware. The study suggests that 48 of these attacks are likely preventable with our proposed effect-aware package manager.

Article Search Artifacts Available Article: oopslab26main-p863-p doi:10.1145/3839494

Agent-Based Automated Remediation for Vulnerabilities in Maven Projects
Lyuye Zhang, He Ye, Federica Sarro, Yuqiang Sun, and Yang Liu
(Nankai University, China; Nanyang Technological University, Singapore; University College London, UK)
Remediating vulnerabilities in open-source software (OSS) dependencies is vital to maintaining software supply chain security. However, current automated approaches almost exclusively rely on dependency upgrades, which is limited by the nature of upgrades, i.e., the availability of secure versions, version pinning, and API incompatibilities. To address the limitation, this paper presents Remedius, an agent-based remediation framework for Maven projects that unifies dependency upgrading and patch porting within a holistic optimization workflow. Remedius dynamically clusters dependencies by usage, gathers project-specific evidence through autonomous LLM-driven agents, and formulates a cost-aware remediation optimization problem solved via Satisfiability Modulo Theory (SMT). The agents translate complex contextual factors—such as compatibility, reachability, and patch difficulty—into solver-ready constraints, enabling flexible and scalable decision-making beyond what static rules or LLM reasoning alone can achieve. By redefining optimization at the vulnerability level rather than the dependency level, Remedius maximizes vulnerability coverage while preserving build correctness and runtime compatibility. An evaluation of 301 real-world Maven projects demonstrates that Remedius outperforms state-of-the-art baselines, achieving the highest number of vulnerabilities fixed and the fewest build or test failures. These results highlight a new direction for automated OSS remediation beyond upgrade-only solutions toward adaptive, agent-driven vulnerability management.

Article Search Article: oopslab26main-p869-p doi:10.1145/3839495

Granthi: Higher-Order Quantum Programming via Unitary Wiring
Samson Abramsky and Radha Jagadeesan
(University College London, UK; DePaul University, USA)
Existing quantum programming languages confine higher-order structure to a classical host while restricting the quantum layer to first-order operations on qubits. This paper presents Granthi, a purely unitary higher-order quantum programming language built on three design commitments: quantum programs are first-class values that may be passed, returned, and coherently composed; additive structure is tag-preserving routing rather than observational branching, so control may remain in superposition; and programmer-facing finite label types with named reversible operations provide domain-level control spaces without exposing tag management.
Every well-typed term—including at function type—denotes a unitary on its boundary interface, and the compiler realizes exactly its wiring as a quantum circuit on the physical qubit layout (assuming correctness of the pytket backend).
Granthi is implemented end-to-end: an OCaml DSL elaborates surface programs through a binder-free core IR to executable quantum circuits via pytket. The language directly supports the quantum switch—the paper’s running example, compiled to a static circuit—as well as interference on control-flow history and structured finite control, all within the purely unitary fragment.

Article Search Artifacts Available Article: oopslab26main-p876-p doi:10.1145/3839496

Planning to Hammer: Difficulty-Aware Decomposition for Automating Rocq Proofs
Ning Zhang, Nongyu Di, Zenan Li, Yuan Yao, and Xiaoxing Ma
(Nanjing University, China; ETH Zurich, Switzerland)
As AI-generated code proliferates, formal verification—particularly through interactive theorem provers such as Rocq and Isabelle—becomes increasingly important for ensuring software correctness. However, producing machine-checked proofs in such provers remains a bottleneck. Existing solutions bring complementary strengths to proof automation: large language models (LLMs) can propose high-level proof strategies but lack local rigor; automated tactics such as CoqHammer can reliably discharge many local goals, but lack long-range planning capabilities. To combine the best of both worlds, we present Quarry, a planning-based proof synthesis framework that separates proof planning from proof execution. Specifically, Quarry asks an LLM to actively propose multiple proof decompositions with arbitrary sublemmas, type-checks them in Rocq under temporarily admitted sublemmas, and ranks candidates using a proof-state-based difficulty model estimating hammer solvability. It then recursively proves sublemmas within a bounded budget, effectively turning long proofs into sequences of hammer-solvable obligations. We implement Quarry on top of SerAPI and CoqHammer and evaluate it using multiple frontier LLMs across multiple benchmarks. The experimental results show that planning-based decomposition with solvability-aware ranking substantially improves automation while maintaining predictable cost. Under a uniform 10-minute wall-clock budget, Quarry improves over the strongest baseline by 7–13 percentage points in success rate across three Rocq benchmarks. These results demonstrate that reliable proof automation can be achieved by coordinating neural planning with symbolic execution rather than replacing either.

Article Search Article: oopslab26main-p880-p doi:10.1145/3839497

Compiling WebAssembly Concolic Execution with Staging, Continuations, and Snapshots
Dinghong Zhong, Alexander Y. Bai, Mikail Khan, and Guannan Wei
(Tufts University, USA; New York University, USA; Carnegie Mellon University, USA)


Article Search Article: oopslab26main-p881-p doi:10.1145/3839498

A New Approach to Optimal Function Inlining for Code Size Minimization via E-graphs
Amir K. Goharshady, Chun Kit Lam, Andreas Pavlogiannis, and Ahmed Khaled Zaher
(Gran Sasso Science Institute, Italy; Hong Kong University of Science and Technology, Hong Kong; Aarhus University, Denmark)
Minimizing code size is a central problem in compiler optimization, especially in the context of embedded systems and mobile applications. One of the classical optimizations that has recently been adopted to reduce the output code size is function inlining, i.e. repeatedly replacing a function call site by the body of the called function. At first glance, the fact that inlining can help reduce code size is counter-intuitive. However, it enables two types of subsequent optimizations which can affect the code size significantly: (i) the intra-procedural optimizations performed within each function, which make use of the additional context provided by inlining, and (ii) the elimination of dead functions. Many existing heuristics, such as those used by LLVM, focus on a local size analysis based on a few call sites. Thus, they miss the global opportunities to remove dead functions. On the other hand, the current state-of-the-art approach of auto-tuning by Theodoridis et al. [ASPLOS 2022] focuses on global code size but inspects each call site independently in order to avoid a combinatorial explosion. However, inlining decisions are not independent in practice. It is possible that two inlining choices each increase code size on their own, but applying both of them together reduces the size.
In this work, we show that the problem of optimal inlining for code size minimization is NP-hard. We then present a completely different approach to this problem. Our algorithm is based on equality graphs (e-graphs), which are a standard tool in automated theorem proving and have recently been adopted by the compiler optimization community as a key ingredient in equality saturation. We show that optimal function inlining can be reduced to e-graph extraction. Although e-graph extraction is also NP-hard, there are efficient solvers that can handle sparse instances of this problem [OOPSLA 2024]. We build upon these solvers and add further inlining-specific heuristics to design an algorithm for code size reduction.
Finally, we present experimental results on the standard SPEC benchmarks. Compared with LLVM, our approach reduces the code size to 95.34%. This is competitive with the state-of-the-art auto-tuning method of [ASPLOS 2022], which achieves 95.24%. In terms of running time, our approach is 20x faster than auto-tuning. More importantly, due to the two methods having orthogonal strengths, applying both of them leads to a further significant improvement, reducing the code size to 93.94% of LLVM's output.

Article Search Artifacts Available Article: oopslab26main-p885-p doi:10.1145/3839499

Programming with Composable Recursive Patterns and Transformations
Luyu Cheng, Florent Ferrari, Lionel Parreaux, and Michael D. Adams
(Hong Kong University of Science and Technology, Hong Kong; ENS de Lyon, France; National University of Singapore, Singapore)


Article Search Article: oopslab26main-p889-p doi:10.1145/3839500

Interactive Data Analysis with Lively Typed Tables
Alexander Bandukwala and Cyrus Omar
(University of Michigan, USA)
Programming systems tailored for working with tabular data (tabular programming systems), such as spreadsheets and computational notebooks, are essential tools in data science. However, widely adopted systems are limited by the absence of static typing, which restricts the editor support they can provide, particularly when code is organized into reusable functions. Statically typed alternatives are limited by the fact that many useful operations on tables produce results whose column schema is data-dependent, e.g. pivots, unstack operations, or one-hot encodings.
This paper introduces Hazel Lab, a new tabular programming system built as an extension of Hazel, a live gradually typed functional programming environment. It aims to combine the expressivity of dynamically typed systems with the editor support of static typing by incorporating several novel mechanisms into Hazel. Tables are manipulated as sequences of labeled tuples, and we add several useful gradually typed operations on labeled tuples to increase expressiveness, including operations that convert field names to and from strings. These operations support best-effort static typing and fall back to the unknown type when a schema cannot be statically determined. We evaluate the expressiveness of these core abstractions using the Brown Benchmark For Table Types (B2T2), finding that Hazel Lab is able to reasonably express every example.
In order to improve type-based feedback, including error localization, when the fallback to the unknown type is needed, we introduce live typing, which builds on the fact that Hazel is a maximally live programming environment, even when there are static errors in the code, to feed dynamically observed instantiations of statically unknown types back into the static type checker. This feedback is complementary to the dynamic feedback that Hazel already distinctively provides by way of its live probes. We introduce rich probes—an extension of live probes with domain-specific table views that allow users to edit their functional data pipelines through direct manipulation interactions.
We evaluate the usability of our overall design by conducting a lab study with 7 participants, asking them to perform a variety of data cleaning and analysis tasks. The study evaluates the usability and usefulness of the proposed features for users already familiar with statically typed functional programming, rather than to assess transfer to data science workflows by scientists without that training. We find that participants could effectively use the table operations for data cleaning and transformation tasks, and that live typing helped them both understand and debug existing analyses. Most participants responded positively to adopting the evaluated features in their own programming environments, with none responding negatively.

Article Search Artifacts Available Article: oopslab26main-p902-p doi:10.1145/3839501

Timeline: Adding the Time Dimension to Spreadsheets
Tomas Petricek and Tomáš Boďa
(Charles University, Czech Republic)


Article Search Article: oopslab26main-p903-p doi:10.1145/3839502

TwinString: Preserving String Semantics with Off-Heap Data on the JVM
Júnior Löff, Daniele Bonetta, and Walter Binder
(USI Lugano, Switzerland; VU Amsterdam, Netherlands)
Strings are the primary mechanism through which Java applications ingest external textual data, including data read from files, databases, network interfaces, and native libraries. In data-intensive applications, such data must either be materialized as heap-allocated java.lang.String objects, incurring allocation, copying, encoding, and garbage-collection costs, or accessed through low-level and unsafe foreign-memory mechanisms that require non-standard string APIs and explicit reasoning about memory management and object lifetimes. Neither option is well suited to high-volume ingestion workloads that require both efficiency and seamless integration with existing Java code. We present TwinString, an alternative representation of java.lang.String that decouples string semantics from the physical placement of its contents. A TwinString stores its data outside the regular Java heap while preserving the standard String type and behavior expected by Java programs and libraries. VM support controls this data and manages its lifetime with garbage collection, allowing foreign textual data to be exposed as ordinary strings without introducing additional custom string types. We implement TwinStrings in GraalVM Native Image and evaluate them across several workloads, including microbenchmarks, text-processing applications over real-world datasets, and data-heavy applications using JDBC and SQLite. The results show that TwinStrings significantly reduce allocation overhead while remaining compatible with the original String API, and reduce P99.9 tail latency by up to 42.2% in realistic library and JDBC workloads by alleviating heap allocation and garbage-collection pressure.

Article Search Artifacts Available Article: oopslab26main-p914-p doi:10.1145/3839503

Filtr: Compiling Bioinformatics Recurrences
Bala Vinaithirthan, Shiv Sundram, Sneha Goenka, and Fredrik Kjolstad
(Stanford University, USA; Princeton University, USA)
Many bioinformatics algorithms, such as sequence alignment and structure prediction, can be expressed as recurrence equations over a dynamic programming matrix. Efficient implementations of these algorithms for large-scale biological data often require changing the order in which matrix cells are calculated and pruning ineffectual regions of the matrix from consideration altogether, but these techniques typically complicate implementation. We introduce Filtr, a domain-specific language (DSL) and compiler framework for bioinformatics recurrences. Filtr keeps the core recurrence rules separate from the pruning and scheduling strategies, where pruning acts as an approximation to limit where in the DP matrix cells are computed, and scheduling determines the iteration order for how cells are explored. Filtr compiles these high-level descriptions into optimized C++ code that matches the performance of hand-tuned implementations while enabling rapid exploration of new heuristics. Filtr is competitive with hand-optimized sequence-alignment libraries, ranging from 0.95× to 30× faster across biological benchmarks.

Article Search Artifacts Available Article: oopslab26main-p916-p doi:10.1145/3839504

Revisiting Row Polymorphism for Set-Theoretic Types
Mickaël Laurent, Pierre Donat-Bouillud, Filip Křikava, and Jan Vitek
(Charles University, Czech Republic; Czech Technical University, Czech Republic)
Set-theoretic types support expressive record types through unions, intersections, and negations, but they lack the row polymorphism needed to type operations that propagate unknown fields across records. Prior work addresses this by allowing Boolean combinations of rows in type substitutions, which complicates the formalism and prevents the tallying algorithm from being complete. We propose an alternative: instead of enriching substitutions, we allow Boolean combinations of row variables directly within record type constructors, where the tail of a record has the same shape as any field. This design keeps substitutions simple---a row variable maps to a single row---and yields a natural extension of the subtyping and tallying algorithms. Tallying is complete for all solutions whose rows are constant over labels not mentioned in the constraints. We implement our approach in the set-theoretic type library SSTT and the type checker MLsem, providing the first implementation of a type system that combines semantic subtyping with row polymorphism. We demonstrate the expressiveness of the system by encoding several data structures from the R programming language: heterogeneous lists, variadic function arguments, and class-based dispatch.

Article Search Artifacts Available Article: oopslab26main-p917-p doi:10.1145/3839505

Verifying Repeat-until-Success Protocols using Automata
Jyun-Ao Lin, Yu-Fang Chen, Jakub Havlík, Ondřej Lengál, Fang-Yi Lo, Wei-Lun Tsai, and You-Jie Wu
(National Taipei University of Technology, Taiwan; Academia Sinica, Taiwan; Brno University of Technology, Czech Republic; National Taiwan University, Taiwan)
Repeat-until-success (RUS) protocols implement single-qubit unitaries using measurement, classical control, and unbounded looping. Verifying their functional correctness is challenging due to the combination of probabilistic branching, unbounded looping, and the need to reason about all input states. In this paper, we develop a fully automated framework for verifying the functional correctness of these protocols. The framework is based on viewing quantum states as trees and sets of quantum states as sets of trees, which can be represented using tree automata. The particular automata model that we use are level-synchronized tree automata (), in which nondeterminism is labelled by a choice. Since we can map a sequence of choices to a particular tree (and therefore a quantum state) in the language of an LSTA, we can use the choice-sequence semantics to track input-output correspondence (which input quantum state got transformed into which output quantum state) and enable relational verification. To deal with reasoning about infinitely many quantum states, we prove a three-test theorem, which reduces verifying correctness of RUS protocols to testing correctness on finitely many inputs, enabling automatic invariant synthesis and decidable verification. We implemented our approach and identified previously unreported bugs in the RUS literature.

Article Search Artifacts Available Article: oopslab26main-p918-p doi:10.1145/3839506

RGSep under Release/Acquire Consistency
Ellen Arlt and Viktor Vafeiadis
(MPI-SWS, Germany)
RGSep is a program logic for reasoning about the correctness of concurrent programs that combines rely-guarantee reasoning and separation logic. Although RGSep was initially developed for sequential consistency, we show that it is also sound under the much weaker release-acquire (RA) consistency model, which is a well-behaved subset of the C++11 concurrency model. Our result provides a simpler way to reason about RA programs than the state-of-the-art program logics that support weak memory consistency models.

Article Search Article: oopslab26main-p933-p doi:10.1145/3839507

When FPGA Meets Dataflow Analysis: An Explorative Step
Fang Wei, Qinlin Chen, Nairen Zhang, Jiacai Cui, Tian Tan, Zhiqiang Zuo, and Yue Li
(Nanjing University, China)
Set-based (a.k.a. bit-vector-based) dataflow analysis is a fundamental building block for many static analysis tasks, and significant effort has been devoted to accelerating it. Existing acceleration approaches address the problem from a software perspective, leveraging various general-purpose computing platforms, such as single- and multi-core CPUs, GPUs, and distributed systems. In contrast, a hardware-centric approach—designing specialized hardware that directly accelerates dataflow analysis—remains unexplored.
Motivated by this gap and out of pure research curiosity, we conduct a preliminary exploration of designing specialized hardware for dataflow analysis using FPGAs, which are highly customizable and well suited for rapidly prototyping domain-specific hardware. As a first step toward hardware-accelerated dataflow analysis, we focus on the widely used intra-procedural dataflow analysis. However, we find that designing specialized hardware even for this setting is already challenging: a straightforward FPGA implementation of the classical worklist algorithm is infeasible, because its space complexity grows superlinearly with procedure size, quickly exhausting the FPGA's limited high-speed on-chip memory when analyzing large procedures.
To address this challenge, we introduce FpgaFlow, a specialized hardware design for dataflow analysis that (1) overcomes the spatial infeasibility challenge by leveraging the distributivity of set-based dataflow analysis to achieve linear spatial scalability, and (2) accelerates analysis through hardware-specific parallelism—pipelining with data forwarding and BRAM partitioning and replication.
We evaluate FpgaFlow on diverse and popular real-world Java projects (averaging 32.5k GitHub stars) using two representative dataflow analyses—live variables and reaching definitions—and compare it against their software implementations in a state-of-the-art Java static analyzer Tai-e. In terms of correctness, FpgaFlow produces exactly the same analysis results as Tai-e, amounting to 75 billion bits. In terms of acceleration, even on a modest Xilinx Zynq-7020 FPGA (55 MHz), FpgaFlow achieves an average speedup of 15.45x for live variables and 12.32x for reaching definitions compared with Tai-e running on a server-grade CPU (2.20 GHz to 3.00 GHz). We hope this work offers useful insights toward future FPGA-accelerated static analysis.

Article Search Artifacts Available Article: oopslab26main-p935-p doi:10.1145/3839508

Understanding Accelerator Compilers via Performance Profiling
Ayaka Yorihiro, Griffin Berlstein, Pedro Pontes García, Kevin Laeufer, and Adrian Sampson
(Cornell University, USA)
Accelerator design languages (ADLs), high-level languages that compile to hardware units, help domain experts quickly design efficient application-specific hardware. ADL compilers optimize datapaths and convert software-like control flow constructs into control paths. Such compilers are necessarily complex and often unpredictable: they must bridge the wide semantic gap between high-level semantics and cycle-level schedules, and they typically rely on advanced heuristics to optimize circuits. The resulting performance can be difficult to control, requiring guesswork to find and resolve performance problems in the generated hardware. We conjecture that ADL compilers will never be perfect: some performance unpredictability is endemic to the problem they solve.
In lieu of compiler perfection, we argue for compiler understanding tools that give ADL programmers insight into how the compiler’s decisions affect performance. We introduce Petal, a cycle-level profiler for ADLs that compile to the Calyx intermediate language (IL). Petal instruments the Calyx code with probes and then analyzes the trace from a register-transfer-level simulation. It then maps the events in the trace back to high-level control constructs in the Calyx code to determine when each construct was active. Petal processes that information into a trace of call trees, each representing active events in a specific cycle and their relationships. Lastly, Petal uses metadata generated by the ADL compiler to construct an ADL-level profile. Using case studies, we demonstrate that Petal’s cycle-level profiles can identify performance problems in existing accelerator designs. We show that these insights can also guide developers toward optimizations that the compiler was unable to perform automatically, including a reduction by 46.9% of total cycles for one application.

Article Search Artifacts Available Article: oopslab26main-p940-p doi:10.1145/3839509

Bonsai: Efficient and Optimal Automatic Tensor Rematerialization for Memory-Constrained DNN Training
Dat Nguyen, Vasudha Devarakonda, Anxiao Jiang, and Khanh Nguyen
(Texas A&M University, USA)
GPU memory is increasingly the primary bottleneck in scaling deep neural network (DNN) training, where the activation tensors footprint of a model may exceed the memory capacity. Tensor recomputation is a powerful technique that trades additional computation for reduced peak memory usage. However, existing approaches face a fundamental tension between performance optimality and computational scalability. On the one hand, solvers leverage Integer Linear Programming (ILP) to provide mathematically optimal solutions but suffer from the combinatorial explosion of the search space and thus become intractable for modern DNN models. On the other hand, heuristics-based approaches achieve scalability but sacrifice optimality altogether, resulting in suboptimal execution schedules.
The root cause of these inefficiencies in the state of the art is the mismatch in abstraction. This paper introduces Bonsai, a framework that tackles this scalability-granularity tension. At the heart of Bonsai is a novel abstraction of operator segmentation that breaks the computation graph into flexible, variable-sized units to enable a lightweight yet effective segment-based ILP formulation. By having segments, Bonsai collapses the search space and prunes redundant solutions that stall existing solvers. This abstraction enables Bonsai to maintain a holistic view of the entire model, ensuring that no optimization opportunity is lost while reducing the number of decision variables by orders of magnitude. The evaluation across a diverse set of DNN architectures and models demonstrates that Bonsai scales to real-world models, is up to 10.13× lower solver cost than state-of-the-art ILP solvers, and delivers up to 11

Article Search Artifacts Available Article: oopslab26main-p941-p doi:10.1145/3839510

Sound and Complete Solving for Multi-width Parametric Bitvectors via Principled Reductions
Siddharth Bhat, Léo Stefanesco, George Rennie, John Regehr, and Tobias Grosser
(University of Cambridge, UK; University of Utah, USA)
Bitvectors are foundational for automated reasoning about programs, and fixed-width bitvector solvers (QF_BV) are fast and ubiquitous. However, the theory of parametric bitvectors (PBV), where widths are symbolic, is much less well understood. The theory of multi-width PBV, where expressions may involve n distinct symbolic widths (PBV_n), is particularly challenging. The only existing complete approach for bounded PBV (where all widths have a concrete upper bound) is exhaustive enumeration, requiring one call to a QF_BV solver for each of the exponentially many possible width assignments. This is a significant bottleneck in tools, such as Alive2 and Hydra, that formally reason about compiler optimizations. To address this problem, we first prove that any PBV_n formula can be reduced to an equisatisfiable mono-width (PBV_1) formula with only a linear increase in formula size. The key idea is to encode symbolic widths as bitmasks. This reduction lets us create two solvers for flavors of multi-width PBV. (1) A sound and complete bounded PBV solver, which instantiates the width variable in the PBV_1 formula to a concrete bound, and therefore requires only a single QF_BV solver call. In practice, this solver proves LLVM rewrites in seconds that enumeration fails to prove in hours. (2) By composing our reduction with existing automata-theoretic decision procedures for PBV_1, we obtain a new sound and complete decision procedure for a fragment of PBV_n with parametric widths. This new decidable fragment subsumes the prior state-of-the-art fragment of linear and bitwise operations, by adding support for zero and sign extension. All our solvers are implemented in Lean, with mechanized proofs of soundness and completeness for the unbounded solver. Empirically, we find that our equisatisfiable reduction from PBV_n to PBV_1 turns exponential enumeration into a single QF_BV query that nearly saturates standard PBV benchmarks (506 of 528 problems across all datasets), while our unbounded solvers solve 1.5x as many problems as the state of the art CVC5-based solver for all bitwidths.

Article Search Artifacts Available Article: oopslab26main-p950-p doi:10.1145/3839511

Spatial and Temporal Decomposition for Faster Translation Validation
Benjamin Mikek, Chathur Bommineni, Qirun Zhang, and Thomas Reps
(Georgia Institute of Technology, USA; University of Wisconsin-Madison, USA)
Translation validation is a critical tool in program analysis: when a program P is transformed into a new program P′, translation validation asks whether P and P′ have the same semantics. It serves as a middle ground between compiler testing and formal verification, capable of proving that a particular run of a compiler produced correct results. However, one bottleneck holds back wider adoption of translation validation: performance. State-of-the-art tools frequently time out or require extensive manual engineering to adapt to specific use cases. In this paper, we propose a new approach to improving the scalability of translation validation by decomposing the problem along two axes. Our primary contribution is a method for harnessing compiler information to extract subprograms whose equivalence result implies equivalence of the overall transformation (the spatial axis). We augment this method by utilizing compiler information to dynamically group transformation passes for validation (the temporal axis). Our evaluation demonstrates that this approach validates 10% of translations that existing approaches fail to validate, and speeds up validation by up to 2.4×.

Article Search Artifacts Available Article: oopslab26main-p964-p doi:10.1145/3839512

Random Testing via Runtime Abstract Interpretation
Zain K. Aamer and Benjamin C. Pierce
(University of Pennsylvania, USA)
Property-based testing of C programs can be automated by synthesizing random input generators from separation-logic specifications. Existing work in this space, such as the Bennet testing tool, uses randomized backtracking search, generating random values and checking them against constraints, backtracking on failure. Although this approach performs well on simple recursive heap structures, it struggles as constraints grow more complex, particularly when they involve pointer arithmetic—as, for example, in the many forms of specialized storage allocators that arise in low-level systems software. Existing work uses targeted optimizations and heuristics to satisfy specific classes of constraints, but this requires continual expansion as new special cases arise, resulting in complex tools.
We reframe generation as the iterative refinement of abstract domain elements, where sampling a concrete value is the final refinement. By applying abstract interpretation at runtime to obtain an abstract element, we obtain a lightweight form of constraint solving and propagation that enables randomized testing of programs with complex preconditions. We identify three strategies for applying abstract interpretation: (1) speculative refinement, refining abstract elements before sampling based on immediately following constraints, (2) corrective refinement, calculating “desired” abstract elements from information gleaned from failed constraints, and (3) cascading propagation, propagating information from failures to components of compound expressions. We formalize these ideas in a generator DSL whose monadic semantics are parametric over abstract domains.
We implement this DSL in a new tool called Lucas and evaluate it on sixteen workloads: the six original case studies from the Bennet paper, six position-independent data structures, and four free-list allocators. Comparing configurations with and without refinement, we find that refinement finds bugs in all four allocators and in two of the position-independent data structures that Bennet-style random backtracking fails to find.

Article Search Artifacts Available Article: oopslab26main-p996-p doi:10.1145/3839513

Modular Type Safety for Traits with Extensible Variants and Deep Pattern Matching
Andong Fan, Lionel Parreaux, and Ningning Xie
(University of Toronto, Canada; Hong Kong University of Science and Technology, Hong Kong)
Traits provide a powerful mechanism for code reuse by allowing the definition of shared behaviors that can be composed into classes. Scala traits in particular have been used extensively in both academia and industry to help define reusable components, especially in the context of domain-specific language (DSL) compilers. Pattern matching on the extensible data types representing a DSL’s constructs plays a key role in these applications. However, guaranteeing static type safety in this context is challenging: in Scala, a program using traits may successfully type check but then throw a runtime exception due to non-exhaustive pattern matching. This paper proposes a novel trait language which, for the first time, combines several important features: extensible data types with principled exhaustive pattern matching guarantees, separate type checking, method overriding, and deep pattern matching. The latter two, in particular, are crucial to supporting DSL analysis and optimization use cases, and the former two are important for reliable and scalable software development in the large. We formalize our approach in the framework of Boolean-algebraic subtyping, but its core ideas could be adapted to other type systems: our approach can be used to make languages with traits and extensible variants finally type safe, improving the experience of developers working with DSL compilation.

Article Search Article: oopslab26main-p1000-p doi:10.1145/3839514

ReFun: Reconstructing Function Boundaries in EVM Bytecode
Yichuan Li, Wei Song, Jeff Huang, and Hans-Arno Jacobsen
(Nanjing University of Science and Technology, China; Texas A&M University, USA; University of Toronto, Canada)
Recovering the structure of a Solidity smart contract from its deployed bytecode is a prerequisite for various downstream analyses, such as control-flow graph construction, decompilation, and clone detection. A central step in this task is identifying private functions. However, since all source-level function boundaries are completely lost after compilation, the major challenge of this task lies in how to differentiate function calls from intra-procedural control transfers, because both are implemented via the JUMP/JUMPI instructions. We observe that although jump-based control transfers are superficially uniform, their context information is different. Some contexts provide definitive evidence of an intra-procedural control transfer or a function call, which inspires us to address this problem through progressive refinement rather than naive binary classification. Specifically, we first construct an over-approximated set of potential function call sites based on EVM execution semantics, and then narrow them down using rule-based reasoning. The remaining uncertain cases are finally resolved through probabilistic inference over suggestive contexts. For each identified function, we further analyze the instructions before each jump to determine its target and reassemble scattered code fragments into a continuous instruction sequence. We implement our approach as an open-source tool, dubbed ReFun, and evaluate it on 8,696 real-world Solidity smart contracts across multiple Solidity compiler versions and optimization settings. The experimental results demonstrate that ReFun achieves 94.3% precision and 95.5% recall in function recovery, and it is also efficient, completing function identification and separation for 82% of contracts within eight seconds per contract. Finally, we show how ReFun is applied to the downstream tasks, including contract decompilation and clone detection.

Article Search Artifacts Available Article: oopslab26main-p1030-p doi:10.1145/3839515

Automated Debugging of Datalog Programs
Jiashen Wei, Baoyuan Luo, Runshuo Xie, Yun Qi, Yiyu Zhang, Xizao Wang, Xintao Niu, and Zhiqiang Zuo
(Nanjing University, China)
Datalog has become a widely adopted language in program analysis, security, and data-intensive systems. However, debugging Datalog programs remains fundamentally challenging due to their declarative semantics, lack of explicit control flow, and massive scale of derived facts. Existing approaches, such as inspecting proof trees, algorithmic debugging, or interactive debugging, all require developers to manually navigate through deeply recursive derivations, which quickly becomes infeasible for real-world programs.
In this paper, we take a step toward fully automated debugging of Datalog programs. Our key insight is to reinterpret Datalog execution through a statistical lens: instead of explaining individual facts, we analyze multiple facts collectively, treating derived facts as test cases and their proof trees as execution spectra. This abstraction enables us to adapt Spectrum-based Fault Localization (SBFL) to Datalog, bridging the paradigm gap between declarative logic programs and automated debugging techniques originally designed for imperative languages. To enable systematic evaluation, we construct, to the best of our knowledge, the first benchmark suite for Datalog debugging, comprising 96 real-world instances (37 unique faults) mined from the evolution history of the Doop framework. Each instance is annotated with ground-truth faulty rules and organized under a three-level fault taxonomy. Experimental results demonstrate that our approach effectively localizes faults without any user interaction. The best suspiciousness metric achieves 87.50% Hit@1 (i.e., top-1 hit rate) for faulty rule localization, while faulty predicate localization reaches 37.50%–53.12% Hit@1.

Article Search Artifacts Available Article: oopslab26main-p1057-p doi:10.1145/3839516

ZSafe: Proving the Safety of Proprietary Hardware Designs in Zero Knowledge
Zhaoxiang Liu, James Parker, and Ning Luo
(Kansas State University, USA; Ossa Network, USA; University of Illinois at Urbana-Champaign, USA)
Protecting the confidentiality of hardware designs is essential, especially during third-party verification, where proprietary designs must be examined by potentially untrusted verifiers. Existing approaches, such as obfuscation, watermarking, design encryption, and prior privacy-preserving verification techniques, are either not applicable, rely on trusted third parties, or lack scalable formal guarantees.
We present ZSafe, the first zero-knowledge (ZK) framework to provide formal safety guarantees for proprietary hardware designs. ZSafe enables a designer to prove the safety of confidential hardware to a verifier without revealing the design. Our approach introduces (i) an encoding scheme for hardware design, and a ZK-friendly constraint system that binds hardware design and its formula representation, (ii) an efficient ZKP protocol for validating logical implication, avoiding the prohibitive overhead of formula translation by using probabilistic checking, and (iii) a shared-structure unsatisfiability proof protocol to handle interrelated verification checks efficiently. We implement ZSafe and evaluate it on 69 adapted HWMCC’24 hardware verification benchmarks with up to 300,000 gates. The results demonstrate practical scalability: 90% of instances are proven within an hour.

Article Search Artifacts Available Article: oopslab26main-p1118-p doi:10.1145/3839517

Type, Ability, and Effect Systems: Perspectives on Purity, Semantics, and Expressiveness
Yuyan Bao and Tiark Rompf
(Augusta University, USA; Purdue University, USA)


Article Search Article: oopslab26main-p1136-p doi:10.1145/3839518

A Design Space Exploration of Async/Await
Gavin Gray, Shriram Krishnamurthi, and Will Crichton
(Brown University, USA)
Many modern programming languages include some form of asynchronous programming. In particular, a growing number now have what we call straight-line asynchrony: attempts to provide asynchronous functions that look similar to synchronous functions, thereby enabling asynchrony without introducing complex control. These languages often share construct names like “async” and “await,” which suggests that they have deep semantic similarities. Yet, a close examination reveals that these languages are quite different along several dimensions, often subtly. These differences have real semantic consequences: similar-looking programs can exhibit divergent behavior, confusing developers and language designers alike.
This paper therefore presents a design space exploration of straight-line asynchrony. We dissect several existing languages, and show how no two of them agree as a whole on design decisions that affect the presence and ordering of execution. We articulate a design space with nine dimensions covering the full lifecycle of an asynchronous computation, covering questions such as: What precise guarantees does a language give upon calling an asynchronous function? What happens at the end of a task’s life? How can a task handle being cancelled? We explore these questions through concrete examples, informal design discussion, and a formal semantics. Our ultimate goal is to help programmers, language designers, and language theorists all better understand the emerging landscape of straight-line asynchrony.

Article Search Artifacts Available Article: oopslab26main-p1146-p doi:10.1145/3839519

Infinitary Relational Logic
Vladimir Gladshtein, Qiyuan Zhao, Yuxi Ling, Sean Wang, and Ilya Sergey
(National University of Singapore, Singapore; Princeton University, USA)
Relational program logics are a popular formalism for stating and proving properties that relate executions of several computations. We present Infinitary Relational Logic (IRL)—the first Hoare-style Separation Logic that allows one to state and prove relational properties of possibly infinite families of arbitrary programs. The key insights behind IRL are to (a) generalise relational program specifications in the style of Separation Logic triples to families of programs indexed by arbitrary infinite sets, and (b) provide general proof rules that support reasoning principles guided by the structure of these index sets.
We have implemented IRL as a foundational embedding and verification tool on top of the Lean proof assistant. We demonstrate its power by showcasing both the practical and theoretical advances IRL brings to the state of the art in deductive program verification. To show the former, we use IRL to specify and prove the correctness of a series of previously unverified algorithms from computer graphics and geo-spatial information systems that iterate over array-encoded continuous objects. In doing so, we show that specifying representations of implicitly continuous data using code rather than traditional state invariants offers pragmatic benefits in the form of concise and reusable proofs, while retaining full compatibility with conventional non-relational Hoare-style reasoning. To show the latter, we use IRL to specify and verify a novel notion we call Weird Machine Realisability, providing the first conceptual framework that formally characterises the space of unintended behaviours permitted by a vulnerable program. All our case studies are formalised in Lean.

Article Search Artifacts Available Article: oopslab26main-p1152-p doi:10.1145/3839520

Tracking Borrows with Regular Expressions
Todd Nowacki, Sam Blackshear, John Mitchell, Shaz Qadeer, and Ilya Sergey
(Mysten Labs, USA; Stanford University, USA; Microsoft, USA; National University of Singapore, Singapore)
Safe systems languages such as Rust enforce an ownership discipline through types: every value has a unique owner, and the type system tracks borrows—references that provide temporary access to values without transferring their ownership. Borrow checking is a static analysis ensuring that no borrow outlives its owner and that no two mutable borrows are aliases, preventing dangling references and data races at compile time. Move, a smart contract language deployed on Sui and Aptos blockchains, adopts this model but restricts references to structured access paths rooted in local variables, eliminating the need for complex lifetime tracking mechanisms such as lifetime annotations. We present a novel type system for Move's borrow checker in which access paths are tracked by regular expressions. In this model, Brzozowski derivatives make it possible to express the reachability consequences of borrowing operations, Kleene star summarises borrow chains from function calls and loops, and the aliasing check reduces to the decidable regex emptiness. The design of the type system with regular expression-based borrow tracking extends naturally to vectors and enumeration types. The proposed design of a borrow checker has been implemented in the Move bytecode verifier for Sui blockchain, where it superseded the original borrow analyser while maintaining full backwards compatibility. We mechanised the type system in Lean with a machine-checked soundness proof and an executable algorithmic type checker tested against the production Move compiler. Notably, this 39,000-line metatheory was developed with an AI proof assistant in roughly one month, and we report on our experience of conducting this proof effort, which is among the largest AI-assisted PL metatheory mechanisations to date.

Article Search Artifacts Available Article: oopslab26main-p1171-p doi:10.1145/3839521

PRDTs: Composable Design and Verification of Consensus Protocols using Replicated Data Types
Julian Haas, Ragnar Mogk, Annette Bieniusa, and Mira Mezini
(Technische Universität Darmstadt, Germany; Rheinland-Pfälzische Technische Universität Kaiserslautern-Landau, Germany)
Consensus protocols are fundamental in distributed systems as they enable services with strong consistency properties. However, designing protocols optimized for specific use-cases under certain system assumptions is typically an error-prone process requiring expert knowledge. Furthermore, while most recent optimized protocols are variations of well-known algorithms like Paxos or Raft, they often necessitate complete re-implementations, potentially introducing new bugs and complicating the application of existing verification results. This approach impedes application-specific consistency protocols that can easily be amended or swapped out, depending on the given application and deployment scenario.
We propose Protocol Replicated Data Types (PRDTs), a novel programming model for implementing consensus protocols using replicated data types (RDTs). Inspired by the knowledge-based view of consensus, PRDTs employ RDTs to monotonically accumulate knowledge until agreement is reached. This approach allows for implementations focusing on high-level protocol logic that abstracts away network details and facilitates automated verification. Moreover, by applying existing algebraic composition techniques for RDTs in the PRDT context, we enable composable protocol building-blocks for implementing complex protocols. We present a formal model of our approach and implement a proof procedure that allows automated reasoning about the consensus safety of concrete PRDT implementations. Additionally, we demonstrate the applicability of our model in verified PRDT-based implementations of existing consensus protocols, and report empirical performance evaluation results. Our findings indicate that the PRDT approach offers enhanced flexibility and composability in protocol design, facilitates reasoning about correctness, and is suited for real-world adoption without intrinsic performance drawbacks.

Article Search Artifacts Available Article: oopslab26main-p1189-p doi:10.1145/3839522

AADT: Abstract Abstract Data Types
Julien Simonnet, Matthieu Lemerre, and Mihaela Sighireanu
(Université Paris-Saclay - CEA LIST, France; Université Paris-Saclay - ENS Paris-Saclay - CNRS - LMF, France)
Proving properties of programs that manipulate compound data structures requires both disjunctive reasoning (e.g., a pointer may target different arrays) and relational reasoning. Existing abstract interpreters struggle to combine both: non-relational designs support modular composition of abstract domains but lose relations, while assignment-based relational designs capture relations but hinder modularity and reuse. We introduce open lattices and abstract abstract datatypes (AADT), a new foundation for building precise and reusable abstract domains for structured values. Open lattices generalize classical lattices by introducing shared symbolic values constrained by an abstract valuation domain, enabling relational reasoning across independently defined abstractions. AADTs are compositional transformers over open lattices that mirror the structure of concrete data types: addresses, records, unions, variants, arrays, and their arbitrary nesting. Because each AADT closely follows the concrete datatype definition, abstract domain operations are modular and easy to reuse or extend. Most AADT transformers that we provide are exact: when the abstract valuation domain is exact, the resulting abstraction is a precise translation of the concrete semantics. This enables applications beyond static analysis, such as counter-example generation. We formalize open lattices and AADTs, present key instances, and implement them in a framework for the analysis of C and binary programs. Our experiments show precision gains over state-of-the-art abstract interpreters, while maintaining comparable analysis times.

Article Search Article: oopslab26main-p1236-p doi:10.1145/3839523

Synthesizing Graph Queries from Demonstrations
Xiaoyu Liu, Qikang Liu, Evan Dyce, Keval Vora, and Yuepeng Wang
(Simon Fraser University, Canada)
Writing graph queries is challenging for non-experts due to the complexity of graph data models and the need to identify proper graph patterns. While recent research has advanced query synthesis for relational and document databases, the problem of synthesizing graph queries remains under-explored. We present a novel approach for synthesizing graph queries from computation demonstrations, where users specify the desired output through expressions over properties of input graphs. Our method addresses the challenge of inferring meaningful graph patterns for matching and efficiently constructing the remaining components of the query. Specifically, we combine graph mining, which identifies candidate patterns across input graphs, with deduction-based pruning, which guides an efficient synthesis of the filtering predicate and return clause. We have implemented our approach in a tool called DMiner and evaluated it on 90 benchmarks. Experimental results show that DMiner successfully synthesizes desired queries for 87 benchmarks, with an average synthesis time of 0.6 seconds per query. This outperforms both enumerative search and LLM baselines. We also conducted a user study, which shows that users can provide demonstrations with modest effort and 87.5% of the provided demonstrations are sufficient for DMiner to synthesize the desired query.

Article Search Artifacts Available Article: oopslab26main-p1253-p doi:10.1145/3839524

Reducing Hallucinations in LLM-Generated Code via Semantic Triangulation
Yihan Dai, Sijie Liang, Haotian Xu, Peichu Xie, and Sergey Mechtaev
(Peking University, China; Beijing Forestry University, China; Independent, China)
Large language models (LLMs) can generate executable code from natural language descriptions, but the resulting programs frequently contain bugs due to hallucinations. In the absence of formal specifications, existing approaches attempt to assess correctness using LLM-generated proxies such as tests or auto-formalized specifications. However, these proxies are produced by the same imperfect models and thus often corroborate rather than catch errors, especially when the model exhibits correlated errors. We introduce semantic triangulation, a theory-grounded framework that decorrelates model errors by transforming the original problem into a dissociative variant---one likely requiring a fundamentally different algorithm---and checks consistency between independently sampled solutions to both problems. We identify theoretical requirements for this framework, and we prove that under a formal model of LLM hallucinations, these properties confer higher confidence in program correctness. We instantiate the framework through four concrete triangulation methods based on problem inversion, decomposition, and solution enumeration. Evaluated on LiveCodeBench and CodeElo across GPT-4o, DeepSeek-V3, and Gemini 2.5 Flash, our tool increases the probability of selecting a correct program by 16% over baselines (test generation, metamorphic testing, and auto-formalized specifications) and achieves 7% higher reliability and 7% higher F1 score in selection-or-abstention scenarios, while being the only method that consistently handles inexact problems admitting multiple valid solutions.

Article Search Article: oopslab26main-p1277-p doi:10.1145/3839525

Accurate Residues for Floating-Point Debugging
Yumeng He and Pavel Panchekha
(University of Utah, USA)
Floating-point arithmetic is error-prone and unintuitive. Floating-point debuggers instrument programs to monitor floating-point arithmetic at run time and flag numerical issues. To do so, they estimate residues—the difference between actual floating-point and ideal real values—for every floating-point value in the program. A large literature has explored various approaches for computing these residues accurately (leading to few false reports, i.e., false positives and false negatives) and efficiently (leading to low overhead over uninstrumented execution). Unfortunately, the most efficient methods, based on "error-free transformations", have a high rate of false positives, while the most accurate methods, based on high-precision arithmetic, are very slow. This paper builds on error-free-transformations-based approaches and aims to improve their accuracy while preserving efficiency.
To more accurately compute residues, this paper divides residue computation into two steps—rounding error computation and residue function evaluation—and shows how to perform each step accurately via careful improvements to the current state of the art. We evaluate on 44 large scientific computing workloads, focusing on the 14 benchmarks where prior tools produce false reports: our approach eliminates false reports on 10 benchmarks and substantially reduces them on the remaining benchmarks.
Moreover, we find that more complex numerical issues, such as those found in numerical analysis textbooks, require additional care, because floating-point debuggers suffer from absorption, in which two different machine-precision residues cannot both be computed accurately in a single execution. To address absorption, this paper introduces residue override, which re-executes the program multiple times, computing different residues in different executions and assembling a final "patchwork" execution where all residues are accurately computed. We evaluate on 169 standard benchmarks drawn from numerical analysis papers and textbooks, requiring only 3.6 re-executions on average. Among 34 benchmarks with false reports in the initial run, residue override is triggered on 29 of them and reduces false reports on 25 of them, averaging 7.1 re-executions.

Article Search Artifacts Available Article: oopslab26main-p1278-p doi:10.1145/3839526

Real-to-Sim Generation: Synthesizing Scenario Programs from Real-World Data via Constraint Solving
Peishan Huang, Wenmeng Zhang, Yusen Chen, and Zhenbang Chen
(National University of Defense Technology, China)
The demand for synthetic training data is hindered by the sim-to-real gap, as current data-driven and LLM-based generators often produce physically implausible scenarios. To address this, we propose R2SGEN, a Real-to-Sim framework that synthesizes structured scenario programs from real-world data. To overcome the combinatorial explosion and intractability of monolithic Satisfiability Modulo Theories (SMT) encoding, we introduce a decoupled synthesis strategy. This approach separates the discrete structural program search from continuous geometric resolution using lightweight, atomic SMT constraints. Furthermore, we significantly accelerate the search process by integrating two tailored pruning mechanisms: Common Prefix Abstraction-based pruning for Breadth-First Search and Branch-and-Bound for Depth-First Search. We evaluate R2SGEN on 20 real-world scenes of varying complexity from the nuScenes dataset. Experimental results show that our method guarantees consistency with the input scene and produces substantially lower-cost programs than the LLM-based baselines under the evaluated inputs. Both proposed search paradigms exhibit complementary advantages, proving highly efficient and scalable for high-complexity synthetic data generation.

Article Search Article: oopslab26main-p1287-p doi:10.1145/3839527

Quantum Uncomputation of Clean and Dirty Ancilla Qubits
Chenke Liu, Li Zhou, and Boning Meng
(Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China)
Automatic uncomputation aims to provide programming-language-level support to facilitate the correct and safe use of ancilla qubits in quantum computing, but efforts have only been made for clean ancillas, leaving dirty ancillas unexplored. We present a unified formalization of the uncomputation of both clean and dirty ancillas. For the first time, we prove that checking the existence of uncomputation is coNP-hard. We introduce two complementary synthesis-oriented existence checking methods: a syntax-directed static reasoning system and a rewrite-based normalization procedure (RwUn), together forming a top-down pipeline. We implement RwUn in Qiskit. Compared to the state-of-the-art Reqomp, RwUn achieves 100% coverage on complex-dependency benchmarks, twice the coverage on random classical circuits, and about 50% coverage on random quantum circuits beyond the scope of existing methods, demonstrating broader applicability.

Article Search Artifacts Available Article: oopslab26main-p1342-p doi:10.1145/3839528

BackSmith: A Systematic Approach to Testing Compiler Backends
Hongyu Chen, Yu Wang, Jianhua Zhao, and Ke Wang
(Nanjing University, China)
Compiler backends are critical for translating high-level code into efficient machine instructions, yet they remain relatively underexplored in compiler testing. Effective backend testing requires programs that expose low-level backend behaviors, but such features are difficult to generate and are frequently eliminated by earlier optimization passes. As a result, existing testing approaches often fail to adequately exercise backend behaviors and are therefore less effective at uncovering backend defects.
We present BackSmith, a black-box approach for testing compiler backends across compilers and architectures. BackSmith generates code snippets with two complementary properties: backend-oriented features that directly stress backend mechanisms such as instruction selection and register allocation, and optimization-resistant features that preserve program diversity by resisting excessive middle-end canonicalization. To further increase coverage of rare but critical backend behaviors, BackSmith also generates code snippets whose compiled assembly rarely arises during random generation. It then integrates all three kinds of features into seed programs for backend testing.
We evaluated BackSmith on 16 mature GCC and LLVM backends. Over five months of testing, BackSmith uncovered 104 previously unknown backend bugs, 88 of which have been confirmed or fixed, demonstrating the effectiveness of our approach in systematically exposing backend defects.

Article Search Artifacts Available Article: oopslab26main-p1391-p doi:10.1145/3839529

Efficient Extraction for Effectful E-graphs
Oliver Flatt, Anjali Pal, Yihong Zhang, Ryan Tjoa, Kirsten Graham, Alex Fischman, Chandrakana Nandi, Eli Rosenthal, Zachary Tatlock, and Haobin Ni
(University of Washington, USA; Certora, USA; Google, USA)
E-Graphs have enabled recent advances in program optimization, synthesis, and verification, yet remain difficult to apply to effectful programs whose memory and I/O operations must respect execution order. Existing effect-aware extraction algorithms rely on integer linear programming (ILP) and dominate total runtime.
We introduce Statewalk DP, a new extraction algorithm that enforces effect ordering efficiently without external solvers. We prove that finding any effect-safe extraction is NP-complete, but show that Statewalk DP is tractable in statewalk width, a parameter that measures the complexity of dataflow interactions among effects. In practice, statewalk width generally remains small, enabling Statewalk DP to achieve order-of-magnitude speedups over ILP extraction while producing programs comparable to LLVM across our benchmarks. We implement the algorithm in EGGCC, a prototype e-graph-based compiler for imperative Bril programs, and demonstrate that effect-aware extraction is no longer a bottleneck.

Article Search Artifacts Available Article: oopslab26main-p1395-p doi:10.1145/3839530

Semi-declarative Language for Combinatorial Search
Ziyi Yang and Ilya Sergey
(National University of Singapore, Singapore)
Combinatorial search—finding solutions that meet constraints within an exponentially large space of candidates—underpins problems from hardware verification to scheduling and combinatorial design. The most successful approach in practice is Propositional Satisfiability (SAT) solving, but modelling a problem for a SAT solver requires manually translating high-level requirements into conjunctions of boolean clauses, a tedious step that sacrifices clarity and modularity. Answer Set Programming (ASP) offers a higher-level alternative, with a rule-based language whose variables and finite-domain reasoning yield more compact problem descriptions that can be automatically compiled into low-level solver input. Yet, ASP has its own shortcomings: its semantics, defined via a notion of stable models, is hard to build intuition for; it does not allow arbitrary first-order logic formulas as constraints; and its programs tend to be monolithic, making modular design and reuse difficult.
We propose SetLah!, a semi-declarative language for combinatorial search that addresses the shortcomings of both SAT and ASP. A SetLah! program is a sequence of stratified blocks, each containing rules that define the search space and arbitrary first-order logic constraints that prune it. This block structure enables modular problem decomposition, allowing for an intuitive semantics: candidate solutions are generated and filtered block by block. We built a compiler from SetLah! programs into ASP, allowing us to take full advantage of the existing efficient ASP solvers, while also automatically optimising the generated encodings. Our empirical evaluation demonstrates that SetLah! offers substantially more concise and intuitive specifications for common combinatorial search problems, and its compiled ASP encodings can significantly outperform SAT-based tools.

Article Search Artifacts Available Article: oopslab26main-p1419-p doi:10.1145/3839531

TensorRocq: Enabling Diagrammatic Reasoning in Rocq
Ben Caldwell, William Spencer, Aleks Kissinger, and Robert Rand
(University of Chicago, USA; University of Oxford, UK)
Symmetric monoidal categories (SMCs) are a common framework for reasoning about computation, focusing on the parallel and sequential compositionality of operations. String diagrams are a ubiquitous and powerful tool for reasoning about equations in SMCs, eliding the fine details of compositionality to focus on connectivity. However, when working with SMCs in a proof assistant, the rigid equational structure of composition obscures the essential connective information, leading to longer proofs filled with syntactic manipulation. To address the gap between proof assistants and paper proofs, we have developed verified tools for diagrammatic reasoning in Rocq, including inferring term equivalence and rewriting modulo the deformation of string diagrams. This is achieved by converting between syntactic representations of SMC terms and hypergraphs with interfaces, while preserving a common tensor semantics. We provide tools to develop simple SMC theories from generators and relations, and perform equational reasoning over these systems. Our tactics can also be used in existing verification projects about symmetric monoidal categories that can be treated as tensors.

Article Search Article: oopslab26main-p1457-p doi:10.1145/3839532

Probabilistic Programming with Programmable Divide-Conquer-Combine Inference on Modern Hardware
Markus Böck and Jürgen Cito
(TU Wien, Austria)
Universal probabilistic programming languages (PPLs) enable the specification of models with stochastic support structure. Posterior inference is notoriously hard for this class of models and remains difficult to accelerate on modern hardware. In response to these challenges, we introduce Upix - the first probabilistic programming system that realises the divide-conquer-combine (DCC) inference algorithm as a framework. In Upix, a model expressed in a universal PPL is automatically split into multiple sub-models with static support structure, which are then compiled with JAX for execution on accelerator hardware. The system allows extensive customisation of inference algorithms by incorporating established concepts from programmable inference literature. To evaluate our system, we implemented two existing DCC algorithms in Upix and instantiated three novel algorithms. We show that our implementation can result in better approximation quality compared to existing approaches by achieving up to 1070 times more computation within the same time budget. On machines with up to 64 CPU cores and 8 GPU devices, we demonstrate that Upix enables the scaling of inference algorithms to workloads that are impractically slow for CPUs and prior methods.

Article Search Artifacts Available Article: oopslab26main-p1458-p doi:10.1145/3839533

Type-Directed Discretization of Probabilistic Programs
Katherine Wu, Jules Jacobs, Kevin Batz, and Alexandra Silva
(Cornell University, USA; Jane Street, USA)
We study exact discretization as a semantics-preserving transformation for recursive, higher-order probabilistic programs with continuous distributions. We target programs where continuous values are compared against finitely many constants, so exact inference reduces to a discrete problem. Our central technical contribution is a non-local, type-directed analysis that infers where continuous values can be partitioned into finitely many observationally relevant regions, then rewrites sampling and comparison behavior over those regions. We call this transformation Slice. Because this construction is global and type-directed, correctness requires reasoning beyond the local syntax: we formalize the transformation and prove soundness for boolean queries using a coupling-style logical relations argument over operational semantics. As an application, transformed programs can be executed by discrete engines such as Dice, Roulette, and Storm. Our empirical evaluation shows two complementary strengths of Slice when paired with discrete backends: it enables exact inference for challenging continuous programs that lie beyond the reach of previous exact systems, and, on benchmarks where direct comparison is possible, it is competitive with state-of-the-art exact inference systems for continuous programs.

Article Search Artifacts Available Article: oopslab26main-p1463-p doi:10.1145/3839534

P4-SpecTec: Integrating a Language Mechanization Framework into the Real-World P4 Specification
Jaehyun Lee, Seokhun Jeong, Sehyuk Ahn, Haechan Kwon, and Sukyoung Ryu
(KAIST, Republic of Korea)
Programming languages evolve over time, but often without a complete and unambiguous definition of their syntax and semantics. Ambiguities and inconsistencies are silently introduced into specifications, and manifest as divergences between the specification, implementations, and formalizations that constitute the language ecosystem. Even in rare cases when a normative specification exists, like JavaScript and WebAssembly (Wasm), keeping the ecosystem in sync is a daunting task. Language mechanization frameworks address this problem by treating a mechanized specification as the single source of truth, from which implementations and documents are generated. Recently, this approach has been integrated into the actual JavaScript and Wasm specifications with ESMeta and Wasm-SpecTec, respectively. Despite these successes, it remains an open question how to extrapolate ESMeta and Wasm-SpecTec to other language specifications. Both framework designs leverage the existence of JavaScript and Wasm’s normative specifications, which is not the case for many languages. As a first step towards addressing this question, we present P4-SpecTec, a language mechanization framework for the P4 programming language, as a case study of real-world adoption of language mechanization. P4 is a statically-typed domain-specific language for programming packet processors. It is evolving without a normative specification, thereby introducing inconsistencies and errors into the P4 ecosystem. From a mechanization framework perspective, P4 introduces unique challenges, in particular the requirement that its type system mechanization should be executable, which is not supported by either ESMeta or Wasm-SpecTec. To address this challenge, we introduce algorithmic inference rules as the primary instrument for mechanization, enabling the mechanized P4 static and dynamic semantics to be executed as a P4 type checker and interpreter, respectively. We mechanized the most recent P4 specification, and utilizing its executability, identified 24 bugs across the official P4 specification and the reference compiler. Furthermore, P4-SpecTec derives a specification document as prose algorithms, making it accessible to P4 developers. P4-SpecTec is conditionally adopted as the official P4 specification authoring toolchain. We share the lessons learned from our case study, to provide insights for integrating mechanization into real-world languages without normative specifications.

Article Search Article: oopslab26main-p1509-p doi:10.1145/3839535

LLM-Based Alarm Resolution Guided by Bayesian Program Analysis
Yifan Zhang, Yuanfeng Shi, Haoran Lin, Yingfei Xiong, and Xin Zhang
(Peking University, China)
Abstract-interpretation-based static analyzers often report large numbers of alarms due to over-approximation. Although large language models (LLMs) can help filter alarms, per-alarm prompting is often inaccurate and expensive. LLMs often misjudge such end alarms, and the repeated context across queries wastes many tokens. We shift LLM judgment from end alarms to intermediate facts (e.g., alias or flow edges), which are easier to validate. If a fact is judged false, all dependent facts and alarms can be pruned. We capture these dependencies in a derivation graph, enabling analyzer-agnostic pruning for any tool that exposes derivations. Under a token budget, we define the fact impact prioritization problem, which asks which facts to query first to maximize expected downstream pruning. We solve it with Bayesian program analysis by estimating each fact’s pruning impact from rule probabilities and fact posteriors. Building on these ideas, we present an LLM-based alarm resolution framework guided by Bayesian program analysis. It iteratively queries high-impact facts that LLMs can judge accurately, prunes downstream nodes when a fact is false, and feeds the judgments back to the Bayesian model as high-confidence evidence. We evaluate our approach on a Java datarace analysis and a C taint analysis, showing that it improves alarm-resolution quality while substantially reducing token consumption compared with both unfiltered static analysis and per-alarm LLM judging.

Article Search Artifacts Available Article: oopslab26main-p1540-p doi:10.1145/3839536

Validating Optimizing SMT Solvers via Cross-Theory Approximation
Maolin Sun, Fuqi Jia, Yibiao Yang, and Yuming Zhou
(Nanjing University, China; Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China)
Optimization Modulo Theories (OMT) extends Satisfiability Modulo Theories (SMT) by integrating logical reasoning with numerical optimization to address constrained optimization problems across diverse theories. Optimizing SMT solvers (also known as OMT solvers), designed to handle such problems, serve as foundational components in numerous applications within programming languages research and practice. However, despite their widespread adoption, OMT solvers are susceptible to subtle yet critical bugs that can silently mislead downstream applications by providing incorrect optimal solutions, potentially leading to severe consequences. Validating these solvers poses a fundamental challenge, as obtaining precise ground truth for optimal solutions is inherently difficult, particularly under complex or theory-specific objective functions. Moreover, existing SMT solver testing techniques are inadequate, as they fail to capture the intricate interplay between satisfiability checking and optimization reasoning in OMT. To overcome these challenges, we propose cross-theory approximation, a novel validation methodology that leverages the relationships between solution spaces of different logical theories. The key insight is that an optimal solution produced in one theory should maintain expected relationships when interpreted in another comparable theory's solution space. By defining these cross-theory consistency properties and comparing optimal solutions obtained through theory-specific transformations, we can detect discrepancies that indicate potential solver bugs. For instance, an integer-optimal solution should map cleanly into the broader real-arithmetic domain; deviations from this expected relationship signal incorrect optimization behavior. We implement this methodology in Iris, a practical framework for validating OMT solvers. When testing on the advanced OMT solvers, including Z3 and OptiMathSAT, Iris uncovers 24 previously unknown bugs, 20 of which were subsequently resolved by developers. Notably, most of our reported bugs are correctness issues, emphasizing the effectiveness of our approach in enhancing OMT solver reliability.

Article Search Article: oopslab26main-p1547-p doi:10.1145/3839537

Top-Down = Bottom-Up: Sound and Complete Characterisations of Liveness by Multiparty Global Protocols
Kai Pischke and Nobuko Yoshida
(University of Oxford, UK)
Multiparty session types (MPST) are a type discipline for concurrent and distributed systems, designed to ensure not only type safety and deadlock-freedom, but also liveness of typed communicating processes. Two main MPST methodologies, top-down and bottom-up, have been proposed and are integrated into a wide range of programming languages and tools. The top-down strategy starts by specifying the overall choreography of the protocol (called a global type), from which a set of local types that satisfy safety and liveness are generated by endpoint projection (EPP). Once each participant is type-checked against a generated local type, liveness of the set of typed processes is automatically ensured by construction. The bottom-up strategy directly checks whether local types inferred from processes satisfy liveness in order to enforce liveness of processes. Since the top-down strategy depends on global types and the EPP algorithms, it has often been considered that the top-down system offers strictly less typability than the bottom-up system. Our paper negates this belief. We prove that, using the precise subtyping for the subsumption rule, the top-down strategy offers exactly the same typability as the bottom-up system. More precisely, a multiparty session M is typable and verified to be live by the bottom-up typing system if and only if M is typable by the top-down typing system. The key to the proof is the development of a principal global type inference algorithm which builds a principal global type from an arbitrary set of live local types. We have implemented the global type inference algorithm together with projection, process type checking and local type inference algorithms, and built a toolchain for both the top-down and bottom-up strategies. We evaluated our toolchain with representative examples from the literature, confirming that the top-down approach is more efficient than the bottom-up approach.

Article Search Artifacts Available Article: oopslab26main-p1566-p doi:10.1145/3839538

From Similarity Ranking to Definitive Verdict: LLM-Enhanced Source-to-Binary Function Localization
Jingyi Shi, Chengyue Liu, Zhengzi Xu, Yang Xiao, Xingchu Chen, Yeting Li, Wei Huo, and Yang Liu
(Institute of Information Engineering at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; Nanyang Technological University, Singapore; Imperial Global Singapore, Singapore)
Locating a known source function in a stripped binary is a prerequisite for many security and software engineering tasks, including Software Composition Analysis (SCA) false-positive elimination, patch presence verification, malware analysis, code plagiarism detection, and license compliance auditing. We formalize this need as source-to-binary function localization: given the source code of a target function and its encompassing source package, determine whether the function is present in a stripped binary and, if so, report its address. Two fundamental challenges arise: cross-modal alignment, as source code and stripped binary reside in vastly different representation spaces; and similar function disambiguation, as compilation erases the symbolic features that distinguish functionally similar functions.
We present XLoc, a recall-then-verify framework built on two insights. First, cross-modal alignment does not require costly and error-prone compilation; it only demands token-level alignment, a process that can be reliably approximated. Second, the information needed to disambiguate similar functions is already available on the source side and can be extracted ahead of time to guide verification. Building on these insights, XLoc implements a multi-stage recall module in which an LLM transforms source code into pseudo-decompiled representations aligned with binary decompilation output, bridging the cross-modal gap. For verification, XLoc identifies potentially confusing similar functions, extracts differential summaries, and uses them to guide the verification process toward the specific distinguishing evidence for each candidate, producing definitive accept/reject verdicts rather than similarity rankings.
We evaluate XLoc on two complementary datasets spanning 196 CVEs, 480 vulnerable functions, and 756 binaries. XLoc achieves up to 84.4% localization accuracy (4.2× over the best baseline) and HM=87.1% for positive/negative discrimination (vs. 35.1% for the best baseline). These results demonstrate that XLoc can locate target functions with high accuracy, reliably discriminate between positive and negative cases, and produce definitive verdicts.

Article Search Artifacts Available Article: oopslab26main-p1602-p doi:10.1145/3839539

Systematic Design of Separation Logics
Roberto Bruni, Lorenzo Gazzella, and Roberta Gori
(University of Pisa, Italy)
Thanks to the locality principle, separation logics support modular, scalable analysis of large codebases by relying on local axioms and frame rules to focus only on the heap fragments required for verification. However, depending on the direction—forward vs. backward—and sense of approximation—over vs. under—of the analysis, designing the corresponding proof systems can require some ingenuity. In his work on the calculational design of program logics, Patrick Cousot outlines a methodology for deriving proof systems directly from program semantics using abstract interpretation, covering both correctness and incorrectness analyses. Unfortunately, when applied to heap-manipulating programs, Cousot’s calculational approach cannot handle the locality principle, because it does not provide a calculational way to derive frame rules and produces axioms that refer to the global heap. In this paper, we propose a general methodology for systematically deriving local axioms in which the locality principle is embedded by construction. For heap-manipulating primitives, we can derive the minimal required heap and the corresponding pre- and postconditions, complemented by universal frame rules without additional syntactic side conditions. Our method is parametric w.r.t. a set of semantic closure properties that are exploited to design local axioms; it can deal with different memory models; it favors the reuse of many inference rules across over- and under-approximation; and it produces logical systems capable of deriving a broader range of triples w.r.t. existing, cleverly designed, program logics for (in)correctness, ranging from Separation Logic (SL) and Incorrectness Separation Logic (ISL) to Separation Sufficient Incorrectness Logic (SepSIL). Furthermore, we demonstrate the flexibility of our methodology by applying it to design a novel proof system for inferring necessary preconditions with separation logic.

Article Search Article: oopslab26main-p1694-p doi:10.1145/3839540

First-Class Refinement Types for Scala
Matt Bovel, Viktor Kunčak, and Martin Odersky
(EPFL, Switzerland)
Refinement types—types qualified with logical predicates—have proven effective for lightweight verification in languages like Liquid Haskell, F*, and Dafny. However, in these systems refinements are either written in a separate specification language or treated as second-class annotations, disconnected from the host language's type system. This disconnect creates usability barriers: programmers must maintain two mental models, and refinements cannot interact with features like type inference, subtyping, or overloading.
We present the design of first-class refinement types for Scala~3, where refinements are ordinary types that participate in subtyping, inference, and pattern matching alongside existing language features. We prove type soundness of a core, pure calculus mechanized in Rocq, combining dependent function types, bounded polymorphism, positive equi-recursive types, union and intersection types, and refinement types, using a fuel-bounded definitional interpreter and semantic typing. A distinctive design choice is our partial-correctness semantics: predicates are arbitrary terms that may diverge, and type soundness requires no termination assumptions. Finally, we implement our design as a prototype extension of the Scala~3 compiler with a lightweight e-graph-based solver for predicate entailment.

Article Search Artifacts Available Article: oopslab26main-p1986-p doi:10.1145/3839541