OOPSLA2 2026
Proceedings of the ACM on Programming Languages, Volume 10, Number OOPSLA2
Powered by
Conference Publishing Consulting

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

OOPSLAB – Journal Issue

Contents - Abstracts - Authors

Frontmatter

Title Page


Article: oopslab26foreword-fm000-p doi:
Sponsors


Article: oopslab26foreword-fm003-p doi:

Editorial

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

Papers

Probabilistic Floating-Point Round-Off Analysis via Concentration Inequalities
Yichen Tao, Hongfei Fu, Jiawei Chen, and Jean-Baptiste Jeannin
(University of Michigan, USA; Shanghai Jiao Tong University, China)


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)


Article Search 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)


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)


Article Search 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)


Article Search 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)


Article Search 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)


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)


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)


Article Search 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)


Article Search 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)


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)


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)


Article Search 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)


Article Search 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)


Article Search 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)


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)


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)


Article Search Article: oopslab26main-p559-p doi:10.1145/3839469
Equivalence Checking of ML GPU Kernels
Kshitij Dubey, Benjamin Driscoll, Anjiang Wei, Neeraj Kayal, Rahul Sharma, and Alex Aiken
(Microsoft Research, India; Stanford University, USA; Google DeepMind, India)


Article Search Article: oopslab26main-p562-p doi:10.1145/3839470
Semantics for 2D Rasterization
Bhargav Kulkarni, Henry Whiting, and Pavel Panchekha
(University of Utah, USA)


Article Search 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)


Article Search 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)


Article Search 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)


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)


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; Meta, 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)


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)


Article Search 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)


Article Search 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, France; CNRS, France; ENS Paris-Saclay, France; Inria, France; IBM Research, USA; IBM Research Zurich, Switzerland; Independent, USA)


Article Search 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, Clément Pit-Claudel, and Thomas Bourgeat
(EPFL, Switzerland)


Article Search 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)


Article Search 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)


Article Search 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)


Article Search 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)


Article Search 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)


Article Search Article: oopslab26main-p835-p doi:10.1145/3839491
Sound Enforcement of Dynamic Release Information Flow Policy
Jeffrey Ching and Danfeng Zhang
(Duke University, USA)


Article Search 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 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
(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)


Article Search 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)


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
(University of Oxford, UK; Hong Kong University of Science and Technology, Hong Kong; Aarhus University, Denmark)


Article Search 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)


Article Search 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)


Article Search Article: oopslab26main-p914-p doi:10.1145/3839503
Compiling Bioinformatics Recurrences
Bala Vinaithirthan, Shiv Sundram, Sneha Goenka, and Fredrik Kjolstad
(Stanford University, USA; Princeton University, USA)


Article Search 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 within 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)


Article Search Article: oopslab26main-p918-p doi:10.1145/3839506
RGSep under Release/Acquire Consistency
Ellen Arlt and Viktor Vafeiadis
(MPI-SWS, Germany)


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)


Article Search Article: oopslab26main-p940-p doi:10.1145/3839509
Bonsai: Efficient and Optimal Automatic Tensor Rematerialization for Memory-Constrained DNN Training
Dat Nguyen, Vasudha Devarakonda, Khanh Nguyen, and Anxiao Jiang
(Texas A&M University, USA)


Article Search Article: oopslab26main-p941-p doi:10.1145/3839510
Sound and Complete Solving for Multi-width Parametric Bitvectors via Principled Reductions
Siddharth Bhat, Leo Stefanesco, George Rennie, John Regehr, and Tobias Grosser
(University of Cambridge, UK; University of Utah, USA)


Article Search 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)


Article Search 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)


Article Search 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)


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)


Article Search 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)


Article Search 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)


Article Search 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)


Article Search 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)


Article Search 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
(TU Darmstadt, Germany; RPTU University of Kaiserslautern-Landau, Germany)


Article Search Article: oopslab26main-p1189-p doi:10.1145/3839522
AADT: Abstract Abstract Data Types
Matthieu Lemerre, Julien Simonnet, and Mihaela Sighireanu
(Université Paris-Saclay, France; CEA LIST, France; ENS Paris-Saclay, France; CNRS, France)


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)


Article Search 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)


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)


Article Search 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)


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)


Article Search 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)


Article Search Article: oopslab26main-p1395-p doi:10.1145/3839530
Semi-declarative Language for Combinatorial Search
Ziyi Yang and Ilya Sergey
(National University of Singapore, Singapore)


Article Search 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)


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)


Article Search Article: oopslab26main-p1463-p doi:10.1145/3839534
Language Mechanization Frameworks into Real-World Programming Language Specifications in the Wild
Jaehyun Lee, Seokhun Jeong, Sehyuk Ahn, Haechan Kwon, and Sukyoung Ryu
(KAIST, Republic of Korea)


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)


Article Search 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)


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)


Article Search Article: oopslab26main-p1602-p doi:10.1145/3839539
Systematic Design of Separation Logics
Lorenzo Gazzella, Roberto Bruni, and Roberta Gori
(University of Pisa, Italy)


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)


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

proc time: 0.41