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

Title Page

Editorial Message

Sponsors

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)

Article Search Artifacts Available Artifacts Reusable Results Reproduced

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; Hong Kong University of Science and Technology, China)

Article Search Artifacts Available

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

Article Search

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)

Article Search Info

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)

Article Search

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)

Article Search

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

Article Search Artifacts Available

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

Article Search

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

Article Search

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

Article Search Artifacts Available Artifacts Functional Results Reproduced

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

Preprint

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)

Article Search

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)

Article Search Artifacts Available

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

Article Search Artifacts Available Artifacts Reusable

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

Article Search Artifacts Available

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)

Preprint Artifacts Available

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

Article Search Artifacts Available Artifacts Reusable Results Reproduced

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)

Article Search

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

Article Search Artifacts Available Artifacts Reusable Results Reproduced

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

Article Search

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

Article Search

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

Article Search

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

Preprint Artifacts Available Artifacts Reusable Results Reproduced

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)

Preprint Artifacts Available Artifacts Reusable Results Reproduced

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)

Article Search Artifacts Available Artifacts Functional

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)

Article Search Artifacts Available Artifacts Reusable Results Reproduced

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)

Article Search Artifacts Available Artifacts Reusable

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

Article Search Artifacts Available Artifacts Reusable Results Reproduced

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; Hong Kong University of Science and Technology, Hong Kong; ETH Zurich, Switzerland)

Preprint

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

Article Search Artifacts Available Artifacts Reusable Results Reproduced

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)

Article Search

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

Article Search Artifacts Available Artifacts Reusable Results Reproduced

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

Article Search Artifacts Available Artifacts Reusable Results Reproduced

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

Article Search

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

Article Search Artifacts Available

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)

Preprint Info

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

Article Search Artifacts Available Artifacts Reusable Results Reproduced

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)

Article Search Artifacts Available Artifacts Reusable Results Reproduced

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

Article Search Artifacts Available Artifacts Reusable Results Reproduced

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)

Article Search

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

Article Search

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)

Article Search

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

Article Search

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)

Article Search Artifacts Available Artifacts Reusable Results Reproduced

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

Preprint Artifacts Available Artifacts Reusable Results Reproduced

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)

Article Search Artifacts Available Artifacts Reusable Results Reproduced

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

Article Search Artifacts Available Artifacts Reusable Results Reproduced

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

Article Search

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)

Article Search

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)

Article Search Artifacts Available Artifacts Reusable Results Reproduced

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

Article Search Artifacts Available Artifacts Reusable Results Reproduced

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)

Article Search

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

Article Search

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

Article Search Artifacts Reusable Results Reproduced

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)

Article Search Info Artifacts Available Artifacts Functional Results Reproduced

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

Preprint Artifacts Available Artifacts Functional Results Reproduced

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)

Preprint

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)

Article Search Artifacts Available Artifacts Reusable Results Reproduced

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)

Article Search Artifacts Functional Results Reproduced

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)

Article Search Artifacts Available Artifacts Reusable Results Reproduced

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)

Article Search

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

Article Search Artifacts Reusable Results Reproduced

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)

Preprint Artifacts Available Artifacts Reusable Results Reproduced

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

Article Search Artifacts Available Artifacts Reusable Results Reproduced

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

Article Search Artifacts Available Artifacts Reusable

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)

Article Search Info Artifacts Available Artifacts Reusable Results Reproduced

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)

Article Search