OOPSLA1 2025
Proceedings of the ACM on Programming Languages, Volume 9, Number OOPSLA1

Title Page

Article: oopslaa25foreword-fm000-p doi:

Editorial Message

Article: oopslaa25foreword-fm001-p doi:

A Complete Formal Semantics of eBPF Instruction Set Architecture for Solana
Shenghao Yuan, Zhuoruo Zhang, Jiayi Lu, David Sanan, Rui Chang, and Yongwang Zhao
(Zhejiang University, China; Singapore Institute of Technology, Singapore)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced Article: oopslaa25main-p4-p doi:10.1145/3720414

Binary Cryptographic Function Identification via Similarity Analysis with Path-Insensitive Emulation
Yikun Hu, Yituo He, Wenyu He, Haoran Li, Yubo Zhao, Shuai Wang, and Dawu Gu
(Shanghai Jiao Tong University, China; State Key Laboratory of Cryptology, China; Hong Kong University of Science and Technology, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Results Reproduced Article: oopslaa25main-p5-p doi:10.1145/3720415

Dependency-Aware Compilation for Surface Code Quantum Architectures
Abtin Molavi, Amanda Xu, Swamit Tannu, and Aws Albarghouthi
(University of Wisconsin-Madison, USA)

Publisher's Version Article: oopslaa25main-p6-p doi:10.1145/3720416

Efficient Incremental Verification of Neural Networks Guided by Counterexample Potentiality
Guanqin Zhang, Zhenya Zhang, H.M.N. Dilum Bandara, Shiping Chen, Jianjun Zhao, and Yulei Sui
(UNSW, Australia; CSIRO's Data61, Australia; Kyushu University, Japan)

Publisher's Version Info Article: oopslaa25main-p9-p doi:10.1145/3720417

JavART: A Lightweight Rule-Based JIT Compiler using Translation Rules Extracted from a Learning Approach
Hanzhang Wang, Wei Peng, Wenwen Wang, Yunping Lu, Pen-Chung Yew, and Weihua Zhang
(Fudan University, China; University of Georgia, USA; University of Minnesota at Twin Cities, USA)

Publisher's Version Article: oopslaa25main-p11-p doi:10.1145/3720418

UTFix: Change Aware Unit Test Repairing using LLM
Shanto Rahman, Sachit Kuhar, Berk Cirisci, Pranav Garg, Shiqi Wang, Xiaofei Ma, Anoop Deoras, and Baishakhi Ray
(University of Texas at Austin, USA; Amazon Web Services, USA; Amazon Web Services, Germany; Meta, USA)

Publisher's Version Article: oopslaa25main-p12-p doi:10.1145/3720419

Inductive Synthesis of Inductive Heap Predicates
Ziyi Yang and Ilya Sergey
(National University of Singapore, Singapore)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslaa25main-p16-p doi:10.1145/3720420

Code Style Sheets: CSS for Code
Sam Cohen and Ravi Chugh
(University of Chicago, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced Article: oopslaa25main-p17-p doi:10.1145/3720421

Fast Constraint Synthesis for C++ Function Templates
Shuo Ding and Qirun Zhang
(Georgia Institute of Technology, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Results Reproduced Article: oopslaa25main-p20-p doi:10.1145/3720422

Destination Calculus: A Linear 𝜆-Calculus for Purely Functional Memory Writes
Thomas Bagrel and Arnaud Spiwack
(Tweag, France; LORIA, France; Inria, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Results Reproduced Article: oopslaa25main-p25-p doi:10.1145/3720423

Denotational Foundations for Expected Cost Analysis
Pedro H. Azevedo de Amorim
(University of Oxford, UK)

Publisher's Version Article: oopslaa25main-p29-p doi:10.1145/3720424

Hambazi: Spatial Coordination Synthesis for Augmented Reality
Yi-Zhen Tsai, Jiasi Chen, and Mohsen Lesani
(University of California at Riverside, USA; University of Michigan, USA; University of California at Santa Cruz, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced Article: oopslaa25main-p37-p doi:10.1145/3720425

QED in Context: An Observation Study of Proof Assistant Users
Jessica Shi, Cassia Torczon, Harrison Goldstein, Benjamin C. Pierce, and Andrew Head
(University of Pennsylvania, USA; University of Maryland at College Park, USA)

Publisher's Version Published Artifact Artifacts Available Article: oopslaa25main-p38-p doi:10.1145/3720426

Carapace: Static–Dynamic Information Flow Control in Rust
Vincent Beardsley, Chris Xiong, Ada Lamba, and Michael D. Bond
(Ohio State University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslaa25main-p39-p doi:10.1145/3720427

Unveiling Heisenbugs with Diversified Execution
Arjun Ramesh, Tianshu Huang, Jaspreet Riar, Ben L. Titzer, and Anthony Rowe
(Carnegie Mellon University, USA; Bosch Research, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Results Reproduced Article: oopslaa25main-p45-p doi:10.1145/3720428

Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
Kevin Batz, Joost-Pieter Katoen, Francesca Randone, and Tobias Winkler
(RWTH Aachen University, Germany; University College London, UK; University of Trieste, Italy)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced Article: oopslaa25main-p47-p doi:10.1145/3720429

Pathological Cases for a Class of Reachability-Based Garbage Collectors
Matthew Sotoudeh
(Stanford University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced Article: oopslaa25main-p49-p doi:10.1145/3720430

Scalable and Accurate Application-Level Crash-Consistency Testing via Representative Testing
Yile Gu, Ian Neal, Jiexiao Xu, Shaun Christopher Lee, Ayman Said, Musa Haydar, Jacob Van Geffen, Rohan Kadekodi, Andrew Quinn, and Baris Kasikci
(University of Washington, USA; University of Michigan, USA; Veridise, USA; University of California at Santa Cruz, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced Article: oopslaa25main-p60-p doi:10.1145/3720431

A Mechanized Semantics for Dataflow Circuits
Tony Law, Delphine Demange, and Sandrine Blazy
(Univ Rennes - Inria - CNRS - IRISA, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced Article: oopslaa25main-p65-p doi:10.1145/3720432

QbC: Quantum Correctness by Construction
Anurudh Peduri, Ina Schaefer, and Michael Walter
(Ruhr University Bochum, Germany; KIT, Germany)

Publisher's Version Article: oopslaa25main-p75-p doi:10.1145/3720433

Notions of Stack-Manipulating Computation and Relative Monads
Yuchen Jiang, Runze Xue, and Max S. New
(University of Michigan, USA; University of Cambridge, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced Article: oopslaa25main-p81-p doi:10.1145/3720434

Soundness of Predictive Concurrency Analyses
Shuyang Liu, Doug Lea, and Jens Palsberg
(University of California at Los Angeles, USA; SUNY Oswego, USA)

Publisher's Version Article: oopslaa25main-p84-p doi:10.1145/3720435

IncIDFA: An Efficient and Generic Algorithm for Incremental Iterative Dataflow Analysis
Aman Nougrahiya and V. Krishna Nandivada
(IIT Madras, India)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced Article: oopslaa25main-p91-p doi:10.1145/3720436

Type-Preserving Flat Closure Optimization
Adam T. Geller, Sean Bocirnea, Chester J. F. Gould, Paulette Koronkevich, and William J. Bowman
(University of British Columbia, Canada)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced Article: oopslaa25main-p94-p doi:10.1145/3720437

Orax: A Feedback-Driven Framework for Efficiently Solving Satisfiability Modulo Theories and Oracles
Zhineng Zhong, Ziqi Zhang, Hanqin Guan, and Ding Li
(Peking University, China; University of Illinois at Urbana-Champaign, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: oopslaa25main-p96-p doi:10.1145/3720438

Checking δ-Satisfiability of Reals with Integrals
Cody Rivera, Bishnu Bhusal, Rohit Chadha, A. Prasad Sistla, and Mahesh Viswanathan
(University of Illinois at Urbana-Champaign, USA; University of Missouri, USA; University of Illinois at Chicago, USA; Discovery Partners Institute, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced Article: oopslaa25main-p97-p doi:10.1145/3720446

FO-Complete Program Verification for Heap Logics
Adithya Murali, Hrishikesh Balakrishnan, Aaron Councilman, and P. Madhusudan
(University of Wisconsin-Madison, USA; University of Illinois Urbana-Champaign, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslaa25main-p99-p doi:10.1145/3720447

Metamorph: Synthesizing Large Objects from Dafny Specifications
Aleksandr Fedchin, Alexander Y. Bai, and Jeffrey S. Foster
(Tufts University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced Article: oopslaa25main-p107-p doi:10.1145/3720448

API-Guided Dataset Synthesis to Finetune Large Code Models
Zongjie Li, Daoyuan Wu, Shuai Wang, and Zhendong Su
(Hong Kong University of Science and Technology, China; ETH Zurich, Switzerland)

Publisher's Version Article: oopslaa25main-p109-p doi:10.1145/3720449

Adaptive Shielding via Parametric Safety Proofs
Yao Feng, Jun Zhu, André Platzer, and Jonathan Laurent
(Tsinghua University, China; KIT, Germany; Carnegie Mellon University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced Article: oopslaa25main-p110-p doi:10.1145/3720450

Semantics of Sets of Programs
Jinwoo Kim, Shaan Nagy, Thomas Reps, and Loris D'Antoni
(University of California at San Diego, USA; University of Wisconsin-Madison, USA)

Publisher's Version Article: oopslaa25main-p113-p doi:10.1145/3720515

Automatically Verifying Replication-Aware Linearizability
Vimala Soundarapandian, Kartik Nagar, Aseem Rastogi, and KC Sivaramakrishnan
(IIT Madras, India; Microsoft Research, India; Tarides, India)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced Article: oopslaa25main-p116-p doi:10.1145/3720452

Bridging the Gap between Real-World and Formal Binary Lifting through Filtered-Simulation
Jihee Park, Insu Yun, and Sukyoung Ryu
(KAIST, Republic of Korea)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced Article: oopslaa25main-p119-p doi:10.1145/3720524

Adequacy for Algebraic Effects Revisited
G. A. Kavvos
(University of Bristol, UK)

Publisher's Version Article: oopslaa25main-p124-p doi:10.1145/3720457

LOUD: Synthesizing Strongest and Weakest Specifications
Kanghee Park, Xuanyu Peng, and Loris D'Antoni
(University of California at San Diego, USA)

Publisher's Version Published Artifact Artifacts Available Article: oopslaa25main-p125-p doi:10.1145/3720470

Verification of Bit-Flip Attacks against Quantized Neural Networks
Yedi Zhang, Lei Huang, Pengfei Gao, Fu Song, Jun Sun, and Jin Song Dong
(National University of Singapore, Singapore; ShanghaiTech University, China; ByteDance, China; Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; Nanjing Institute of Software Technology, China; Singapore Management University, Singapore)

Publisher's Version Info Article: oopslaa25main-p136-p doi:10.1145/3720471

The Simple Essence of Monomorphization
Matthew Lutze, Philipp Schuster, and Jonathan Immanuel Brachthäuser
(Aarhus University, Denmark; University of Tübingen, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced Article: oopslaa25main-p140-p doi:10.1145/3720472

Finch: Sparse and Structured Tensor Programming with Control Flow
Willow Ahrens, Teodoro Fields Collin, Radha Patel, Kyle Deeds, Changwan Hong, and Saman Amarasinghe
(Massachusetts Institute of Technology, USA; University of Washington, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced Article: oopslaa25main-p141-p doi:10.1145/3720473

KestRel: Relational Verification using E-Graphs for Program Alignment
Robert Dickerson, Prasita Mukherjee, and Benjamin Delaware
(Purdue University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced Article: oopslaa25main-p150-p doi:10.1145/3720474

Peepco: Batch-Based Consistency Optimization
Ivan Kuraj, John Feser, Nadia Polikarpova, and Armando Solar-Lezama
(Massachusetts Institute of Technology, USA; Basis, USA; University of California at San Diego, USA)

Publisher's Version Article: oopslaa25main-p156-p doi:10.1145/3720513

Modal Effect Types
Wenhao Tang, Leo White, Stephen Dolan, Daniel Hillerström, Sam Lindley, and Anton Lorenzen
(University of Edinburgh, UK; Jane Street, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced Article: oopslaa25main-p161-p doi:10.1145/3720476

HpC: A Calculus for Hybrid and Mobile Systems
Xiong Xu, Jean-Pierre Talpin, Shuling Wang, Hao Wu, Bohua Zhan, Xinxin Liu, and Naijun Zhan
(Institute of Software at Chinese Academy of Sciences, China; Inria, France; Huawei Technologies, China; Peking University, China)

Publisher's Version Article: oopslaa25main-p171-p doi:10.1145/3720478

Guarding the Privacy of Label-Only Access to Neural Network Classifiers via iDP Verification
Anan Kabaha and Dana Drachsler Cohen
(Technion, Israel)

Publisher's Version Article: oopslaa25main-p188-p doi:10.1145/3720480

Language-Parametric Reference Synthesis
Daniel A. A. Pelsmaeker, Aron Zwaan, Casper Bach, and Arjan J. Mooij
(Delft University of Technology, Netherlands; TNO-ESI, Netherlands; Zurich University of Applied Sciences, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced Article: oopslaa25main-p208-p doi:10.1145/3720481

Multi-Language Probabilistic Programming
Sam Stites, John M. Li, and Steven Holtzen
(Northeastern University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced Article: oopslaa25main-p214-p doi:10.1145/3720482

Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
Dongjae Lee, Janggun Lee, Taeyoung Yoon, Minki Cho, Jeehoon Kang, and Chung-Kil Hur
(Massachusetts Institute of Technology, USA; Seoul National University, Republic of Korea; KAIST, Republic of Korea; FuriosaAI, Republic of Korea)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced Article: oopslaa25main-p219-p doi:10.1145/3720525

The Simulation Semantics of Synthesisable Verilog
Andreas Lööw
(Imperial College London, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced Article: oopslaa25main-p221-p doi:10.1145/3720484

Revealing Sources of (Memory) Errors via Backward Analysis
Flavio Ascari, Roberto Bruni, Roberta Gori, and Francesco Logozzo
(University of Pisa, Italy; Meta Platforms, USA)

Publisher's Version Article: oopslaa25main-p222-p doi:10.1145/3720486

Artemis: Toward Accurate Detection of Server-Side Request Forgeries through LLM-Assisted Inter-procedural Path-Sensitive Taint Analysis
Yuchen Ji, Ting Dai, Zhichao Zhou, Yutian Tang, and Jingzhu He
(ShanghaiTech University, China; IBM Research, USA; University of Glasgow, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Results Reproduced Article: oopslaa25main-p233-p doi:10.1145/3720488

PAFL: Enhancing Fault Localizers by Leveraging Project-Specific Fault Patterns
Donguk Kim, Minseok Jeon, Doha Hwang, and Hakjoo Oh
(Korea University, Republic of Korea; Samsung Electronics, Republic of Korea)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced Article: oopslaa25main-p240-p doi:10.1145/3720526

Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials
Qihao Lian and Di Wang
(Peking University, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced ACM SIGPLAN Distinguished Paper Award Article: oopslaa25main-p247-p doi:10.1145/3720492

Characterizing Implementability of Global Protocols with Infinite States and Data
Elaine Li, Felix Stutz, Thomas Wies, and Damien Zufferey
(New York University, USA; University of Luxembourg, Luxembourg; NVIDIA, Switzerland)

Publisher's Version Article: oopslaa25main-p248-p doi:10.1145/3720493

Polymorphic Records for Dynamic Languages
Giuseppe Castagna and Loïc Peyrot
(CNRS - Université Paris Cité, France; IMDEA Software Institute, Spain)

Publisher's Version Article: oopslaa25main-p255-p doi:10.1145/3720497

Efficient Algorithms for the Uniform Tokenization Problem
Angela W. Li and Konstantinos Mamouras
(Rice University, USA)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslaa25main-p261-p doi:10.1145/3720498

Laurel: Unblocking Automated Verification with Large Language Models
Eric Mugnier, Emmanuel Anaya Gonzalez, Nadia Polikarpova, Ranjit Jhala, and Zhou Yuanyuan
(University of California at San Diego, USA)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Functional Results Reproduced Article: oopslaa25main-p266-p doi:10.1145/3720499

Scaling Optimization over Uncertainty via Compilation
Minsung Cho, John Gouwar, and Steven Holtzen
(Northeastern University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Results Reproduced Article: oopslaa25main-p271-p doi:10.1145/3720500

A Unifying Approach to Product Constructions for Quantitative Temporal Inference
Kazuki Watanabe, Sebastian Junges, Jurriaan Rot, and Ichiro Hasuo
(National Institute of Informatics, Japan; SOKENDAI, Japan; Radboud University Nijmegen, Netherlands)

Publisher's Version Article: oopslaa25main-p275-p doi:10.1145/3720501

Bolt-On Strong Consistency: Specification, Implementation, and Verification
Nicholas V. Lewchenko, Gowtham Kaki, and Bor-Yuh Evan Chang
(University of Colorado Boulder, USA; Amazon, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced Article: oopslaa25main-p287-p doi:10.1145/3720502

SPLAT: A Framework for Optimised GPU Code-Generation for SParse reguLar ATtention
Ahan Gupta, Yueming Yuan, Devansh Jain, Yuhao Ge, David Aponte, Yanqi Zhou, and Charith Mendis
(University of Illinois at Urbana-Champaign, USA; Microsoft, USA; Google DeepMind, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Results Reproduced Article: oopslaa25main-p289-p doi:10.1145/3720503

Checking Observational Correctness of Database Systems
Lauren Pick, Amanda Xu, Ankush Desai, Sanjit A. Seshia, and Aws Albarghouthi
(Chinese University of Hong Kong, Hong Kong; University of Wisconsin-Madison, USA; Amazon Web Services, USA; University of California at Berkeley, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced Article: oopslaa25main-p293-p doi:10.1145/3720504

Counterexample-Guided Inference of Modular Specifications
William T. Hallahan, Ranjit Jhala, and Ruzica Piskac
(Binghamton University, USA; University of California at San Diego, USA; Yale University, USA)

Publisher's Version Article: oopslaa25main-p295-p doi:10.1145/3720505

Compressed and Parallelized Structured Tensor Algebra
Mahdi Ghorbani, Emilien Bauer, Tobias Grosser, and Amir Shaikhha
(University of Edinburgh, UK; University of Cambridge, UK)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslaa25main-p297-p doi:10.1145/3720506

Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation
Philipp Schuster, Marius Müller, Klaus Ostermann, and Jonathan Immanuel Brachthäuser
(University of Tübingen, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced Article: oopslaa25main-p299-p doi:10.1145/3720507

Combining Formal and Informal Information in Bayesian Program Analysis via Soft Evidences
Tianchi Li and Xin Zhang
(Peking University, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced Article: oopslaa25main-p382-p doi:10.1145/3720508

Automated Verification of Soundness of DNN Certifiers
Avaljot Singh, Yasmin Chandini Sarita, Charith Mendis, and Gagandeep Singh
(University of Illinois at Urbana-Champaign, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: oopslaa25main-p425-p doi:10.1145/3720509

Show Me Why It’s Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison
Ruixin Wang, Zhongkai Zhao, Le Fang, Nan Jiang, Yiling Lou, Lin Tan, and Tianyi Zhang
(Purdue University, USA; National University of Singapore, Singapore; Fudan University, China)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable Results Reproduced Article: oopslaa25main-p443-p doi:10.1145/3720510

Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice
Jay Richards, Daniel Wright, Simon Cooksey, and Mark Batty
(University of Kent, UK; University of Surrey, UK; NVIDIA, UK)

Publisher's Version Article: oopslaa25main-p329-p doi:10.1145/3721089