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

Title Page

Editorial Message

Sponsors

Exploring the Theory and Practice of Concurrency in the Entity-Component-System Pattern
Patrick Redmond, Jonathan Castello, José Manuel Calderón Trilla, and Lindsey Kuper
(University of California at Santa Cruz, USA; Haskell Foundation, Canada)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Quantified Underapproximation via Labeled Bunches
Lang Liu, Farzaneh Derakhshan, Limin Jia, Gabriel A. Moreno, and Mark Klein
(Illinois Institute of Technology, USA; Carnegie Mellon University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Pyrosome: Verified Compilation for Modular Metatheory
Dustin Jamner, Gabriel Kammer, Ritam Nag, and Adam Chlipala
(Massachusetts Institute of Technology, USA; Intel, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Results Reproduced

Boosting Program Reduction with the Missing Piece of Syntax-Guided Transformations
Zhenyang Xu, Yongqiang Tian, Mengxiao Zhang, and Chengnian Sun
(University of Waterloo, Canada; Monash University, Australia)

Publisher's Version

Static Inference of Regular Grammars for Ad Hoc Parsers
Michael Schröder and Jürgen Cito
(TU Wien, Austria)

Publisher's Version Published Artifact Artifacts Available

RestPi: Path-Sensitive Type Inference for REST APIs
Mark W. Aldrich, Kyla H. Levin, Michael Coblenz, and Jeffrey S. Foster
(Tufts University, USA; University of Massachusetts at Amherst, USA; University of California at San Diego, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Compositional Quantum Control Flow with Efficient Compilation in Qunity
Mikhail Mints, Finn Voichick, Leonidas Lampropoulos, and Robert Rand
(California Institute of Technology, Pasadena, USA; University of Maryland, College Park, USA; University of Chicago, Chicago, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Liberating Merges via Apartness and Guarded Subtyping
Han Xu, Xuejing Huang, and Bruno C. d. S. Oliveira
(Princeton University, USA; University of Hong Kong, China; IRIF - Université Paris Cité, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Probabilistic Inference for Datalog with Correlated Inputs
Jingbo Wang, Shashin Halalingaiah, Weiyi Chen, Chao Wang, and Işıl Dillig
(Purdue University, USA; University of Texas at Austin, USA; University of Southern California, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

im2im: Automatically Converting In-Memory Image Representations using a Knowledge Graph Approach
Fei Chen, Sunita Saha, Manuela Schuler, Philipp Slusallek, and Tim Dahmen
(German Research Center for Artificial Intelligence (DFKI), Saarbrücken, Germany; Saarland University, Saarbrücken, Germany; Aalen University, Aalen, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Model-Guided Fuzzing of Distributed Systems
Ege Berkay Gulcan, Burcu Kulahcioglu Ozkan, Rupak Majumdar, and Srinidhi Nagendra
(Delft University of Technology, Netherlands; MPI-SWS, Germany; IRIF - CNRS - Université Paris Cité, France; Chennai Mathematical Institute, India)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Flexible and Expressive Typed Path Patterns for GQL
Wenjia Ye, Matías Toro, Tomás Díaz, Bruno C. d. S. Oliveira, Manuel Rigger, Claudio Gutierrez, and Domagoj Vrgoč
(National University of Singapore, Singapore; University of Chile, Chile; IMFD, Chile; University of Hong Kong, China; Pontificia Universidad Católica de Chile, Chile)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Mind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers
Arya Vohra, Leo Seojun Lee, Jakub Bachurski, Oleksandr Zinenko, Phitchaya Mangpo Phothilimthana, Albert Cohen, and William S. Moses
(University of Chicago, USA; University of Oxford, UK; University of Cambridge, UK; Brium, France; OpenAI, USA; Google, France; University of Illinois at Urbana-Champaign, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge
John C. Kolesar, Shan Ali, Timos Antonopoulos, and Ruzica Piskac
(Yale University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Reasoning about External Calls
Sophia Drossopoulou, Julian Mackay, Susan Eisenbach, and James Noble
(Imperial College London, UK; Kry10, New Zealand; Victoria University of Wellington, New Zealand; Creative Research & Programming, New Zealand)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification
Chenghang Shi, Dongjie He, Haofeng Li, Jie Lu, Lian Li, and Jingling Xue
(Institute of Computing Technology at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; Chongqing University, China; Zhongguancun Laboratory, China; UNSW, Australia)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

qblaze: An Efficient and Scalable Sparse Quantum Simulator
Hristo Venev, Thien Udomsrirungruang, Dimitar Dimitrov, Timon Gehr, and Martin Vechev
(INSAIT at Sofia University St. Kliment Ohridski, Bulgaria; University of Oxford, UK; ETH Zurich, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

React-tRace: A Semantics for Understanding React Hooks: An Operational Semantics and a Visualizer for Clarifying React Hooks
Jay Lee, Joongwon Ahn, and Kwangkeun Yi
(Seoul National University, Republic of Korea)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable Results Reproduced

Incremental Certified Programming
Tomás Díaz, Kenji Maillard, Nicolas Tabareau, and Éric Tanter
(University of Chile, Chile; Inria, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Correct Black-Box Monitors for Distributed Deadlock Detection: Formalisation and Implementation
Radosław Jan Rowicki, Adrian Francalanza, and Alceste Scalas
(DTU, Denmark; University of Malta, Malta)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Abstraction Refinement-Guided Program Synthesis for Robot Learning from Demonstrations
Guofeng Cui, Yuning Wang, Wensen Mao, Yuanlin Duan, and He Zhu
(Rutgers University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

A Sound Static Analysis Approach to I/O API Migration
Shangyu Li, Zhaoyang Zhang, Sizhe Zhong, Diyu Zhou, and Jiasi Shen
(Hong Kong University of Science and Technology, China; Peking University, China)

Publisher's Version

Homomorphism Calculus for User-Defined Aggregations
Ziteng Wang, Ruijie Fang, Linus Zheng, Dixin Tang, and Işıl Dillig
(University of Texas at Austin, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Synthesizing DSLs for Few-Shot Learning
Paul Krogmeier and P. Madhusudan
(University of Illinois at Urbana-Champaign, USA)

Publisher's Version

REPTILE: Performant Tiling of Recurrences
Muhammad Usman Tariq, Shiv Sundram, and Fredrik Kjolstad
(Stanford University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Results Reproduced

SafeRace: Assessing and Addressing WebGPU Memory Safety in the Presence of Data Races
Reese Levine, Ashley Lee, Neha Abbas, Kyle Little, and Tyler Sorensen
(University of California at Santa Cruz, USA; Microsoft, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

HEMVM: A Heterogeneous Blockchain Framework for Interoperable Virtual Machines
Vladyslav Nekriach, Sidi Mohamed Beillahi, Chenxing Li, Peilun Li, Ming Wu, Andreas Veneris, and Fan Long
(University of Toronto, Canada; Shanghai Tree-Graph Blockchain Research Institute, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Towards Verifying Crash Consistency
Keonho Lee, Conan Truong, and Brian Demsky
(University of California at Irvine, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

A Domain-Specific Probabilistic Programming Language for Reasoning about Reasoning (Or: A Memo on memo)
Kartik Chandra, Tony Chen, Joshua B. Tenenbaum, and Jonathan Ragan-Kelley
(Massachusetts Institute of Technology, USA)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable Results Reproduced ACM SIGPLAN Distinguished Paper Award

Interleaving Large Language Models for Compiler Testing
Yunbo Ni and Shaohua Li
(Chinese University of Hong Kong, Hong Kong)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

A Hoare Logic for Symmetry Properties
Vaibhav Mehta and Justin Hsu
(Cornell University, USA)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Functional Results Reproduced

Two Approaches to Fast Bytecode Frontend for Static Analysis
Chenxi Li, Haoran Lin, Tian Tan, and Yue Li
(Nanjing University, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Tuning Random Generators: Property-Based Testing as Probabilistic Programming
Ryan Tjoa, Poorva Garg, Harrison Goldstein, Todd Millstein, Benjamin C. Pierce, and Guy Van den Broeck
(University of Washington, USA; University of California at Los Angeles, USA; University of Maryland, USA; University of Pennsylvania, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Efficient Abstract Interpretation via Selective Widening
Jiawei Wang, Xiao Cheng, and Yulei Sui
(UNSW, Australia; Macquarie University, Australia)

Publisher's Version

Revamping Verilog Semantics for Foundational Verification
Joonwon Choi, Jaewoo Kim, and Jeehoon Kang
(Amazon Web Services, USA; KAIST, Republic of Korea; FuriosaAI, Republic of Korea)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Results Reproduced ACM SIGPLAN Distinguished Paper Award

Tracing Just-in-Time Compilation for Effects and Handlers
Marcial Gaißert, CF Bolz-Tereick, and Jonathan Immanuel Brachthäuser
(University of Tübingen, Germany; Heinrich-Heine-Universität Düsseldorf, Germany)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable Results Reproduced

Convex Hull Approximation for Activation Functions
Zhongkui Ma, Zihan Wang, and Guangdong Bai
(University of Queensland, Australia; CSIRO’s Data61, Australia)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Results Reproduced

Statically Analyzing the Dataflow of R Programs
Florian Sihler and Matthias Tichy
(Ulm University, Germany)

Publisher's Version

Synthesizing Sound and Precise Abstract Transformers for Nonlinear Hyperbolic PDE Solvers
Jacob Laurel, Ignacio Laguna, and Jan Hückelheim
(Georgia Institute of Technology, USA; Lawrence Livermore National Laboratory, USA; Argonne National Laboratory, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

HybridPersist: A Compiler Support for User-Friendly and Efficient PM Programming
Yiyu Zhang, Yongzhi Wang, Yanfeng Gao, Xuandong Li, and Zhiqiang Zuo
(Nanjing University, China)

Publisher's Version Published Artifact Artifacts Available

Memory-Safety Verification of Open Programs with Angelic Assumptions
Gourav Takhar, Baldip Bijlani, Prantik Chatterjee, Akash Lal, and Subhajit Roy
(IIT Kanpur, India; Microsoft Research, India)

Publisher's Version Published Artifact Artifacts Available

Structural Temporal Logic for Mechanized Program Verification
Eleftherios Ioannidis, Yannick Zakowski, Steve Zdancewic, and Sebastian Angel
(University of Pennsylvania, USA; Inria, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
Jayanaka L. Dantanarayana, Yiping Kang, Kugesan Sivasothynathan, Christopher Clarke, Baichuan Li, Savini Kashmira, Krisztian Flautner, Lingjia Tang, and Jason Mars
(University of Michigan, USA; Jaseci Labs, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Validating SMT Rewriters via Rewrite Space Exploration Supported by Generative Equality Saturation
Maolin Sun, Yibiao Yang, Jiangchang Wu, and Yuming Zhou
(Nanjing University, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Fuzzing C++ Compilers via Type-Driven Mutation
Bo Wang, Chong Chen, Ming Deng, Junjie Chen, Xing Zhang, Youfang Lin, Dan Hao, and Jun Sun
(Beijing Jiaotong University, China; Beijing Key Laboratory of Traffic Data Mining and Embodied Intelligence, China; Tianjin University, China; Peking University, China; Singapore Management University, Singapore)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Results Reproduced

MetaKernel: Enabling Efficient Encrypted Neural Network Inference through Unified MVM and Convolution
Peng Yuan, Yan Liu, JianXin Lai, Long Li, Tianxiang Sui, Linjie Xiao, Xiaojing Zhang, Qing Zhu, and Jingling Xue
(Ant Group, China; UNSW, Australia)

Publisher's Version Published Artifact Artifacts Available

Qualified Types with Boolean Algebras
Edward Lee, Jonathan Lindegaard Starup, Ondřej Lhoták, and Magnus Madsen
(University of Waterloo, Canada; Aarhus University, Denmark)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

PReMM: LLM-Based Program Repair for Multi-method Bugs via Divide and Conquer
Linna Xie, Zhong Li, Yu Pei, Zhongzhen Wen, Kui Liu, Tian Zhang, and Xuandong Li
(Nanjing University, China; Hong Kong Polytechnic University, China; Huawei, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Understanding and Improving Flaky Test Classification
Shanto Rahman, Saikat Dutta, and August Shi
(University of Texas at Austin, USA; Cornell University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Agora: Trust Less and Open More in Verification for Confidential Computing
Hongbo Chen, Quan Zhou, Sen Yang, Sixuan Dang, Xing Han, Danfeng Zhang, Fan Zhang, and XiaoFeng Wang
(Indiana University at Bloomington, USA; Pennsylvania State University, USA; Yale University, USA; Duke University, USA; Hong Kong University of Science and Technology, China; Nanyang Technological University, Singapore)

Publisher's Version Published Artifact Artifacts Available

Shaking Up Quantum Simulators with Fuzzing and Rigour
Vasileios Klimis, Avner Bensoussan, Elena Chachkarova, Karine Even-Mendoza, Sophie Fortz, and Connor Lenihan
(Queen Mary University of London, UK; King’s College London, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Non-interference Preserving Optimising Compilation
Julian Rosemann, Sebastian Hack, and Deepak Garg
(Saarland University, Germany; MPI-SWS, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Active Learning for Neurosymbolic Program Synthesis
Celeste Barnaby, Qiaochu Chen, Ramya Ramalingam, Osbert Bastani, and Işıl Dillig
(University of Texas at Austin, USA; New York University, USA; University of Pennsylvania, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Heap-Snapshot Matching and Ordering using CAHPs: A Context-Augmented Heap-Path Representation for Exact and Partial Path Matching using Prefix Trees
Matteo Basso, Aleksandar Prokopec, Andrea Rosà, and Walter Binder
(USI Lugano, Switzerland; Oracle Labs, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

ABC: Towards a Universal Code Styler through Model Merging
Yitong Chen, Zhiqiang Gao, Chuanqi Shi, Baixuan Li, and Miao Gao
(Southeast University, China)

Publisher's Version Published Artifact Artifacts Available

Synchronized Behavior Checking: A Method for Finding Missed Compiler Optimizations
Yi Zhang, Yu Wang, Linzhang Wang, and Ke Wang
(Nanjing University, China)

Publisher's Version

Formalizing Linear Motion G-Code for Invariant Checking and Differential Testing of Fabrication Tools
Yumeng He, Chandrakana Nandi, and Sreepathi Pai
(University of Utah, USA; Certora, USA; University of Washington at Seattle, USA; University of Rochester, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Results Reproduced

Correct-by-Construction: Certified Individual Fairness through Neural Network Training
Ruihan Zhang and Jun Sun
(Singapore Management University, Singapore)

Publisher's Version

Float Self-Tagging
Olivier Melançon, Manuel Serrano, and Marc Feeley
(Université de Montréal, Canada; Inria, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

TailTracer: Continuous Tail Tracing for Production Use
Tianyi Liu, Yi Li, Yiyu Zhang, Zhuangda Wang, Rongxin Wu, Xuandong Li, and Zhiqiang Zuo
(Nanjing University, China; Xiamen University, China)

Publisher's Version Published Artifact Artifacts Available

Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
Junrui Liu, Jiaxin Song, Yanning Chen, Hanzhi Liu, Hongbo Wen, Luke Pearson, Yanju Chen, and Yu Feng
(University of California at Santa Barbara, USA; University of Illinois at Urbana-Champaign, USA; University of Toronto, Canada; Polychain Capital, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Results Reproduced

Towards a Theoretically-Backed and Practical Framework for Selective Object-Sensitive Pointer Analysis
Chaoyue Zhang, Longlong Lu, Yifei Lu, Minxue Pan, and Xuandong Li
(Nanjing University, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

What’s in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures
Yichen Xu, Oliver Bračevac, Cao Nguyen Pham, and Martin Odersky
(EPFL, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

GALA: A High Performance Graph Neural Network Acceleration LAnguage and Compiler
Damitha Lenadora, Nikhil Jayakumar, Chamika Sudusinghe, and Charith Mendis
(University of Illinois at Urbana-Champaign, USA; University of Texas at Austin, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Choreographic Quick Changes: First-Class Location (Set) Polymorphism
Ashley Samuelson, Andrew K. Hirsch, and Ethan Cecchetti
(University of Wisconsin-Madison, USA; SUNY Buffalo, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Structural Abstraction and Refinement for Probabilistic Programs
Guanyan Li, Juanen Li, Zhilei Han, Peixin Wang, Hongfei Fu, and Fei He
(Tsinghua University, China; University of Oxford, UK; Beijing Normal University, China; East China Normal University, China; Shanghai Jiao Tong University, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Modeling Reachability Types with Logical Relations: Semantic Type Soundness, Termination, Effect Safety, and Equational Theory
Yuyan Bao, Songlin Jia, Guannan Wei, Oliver Bračevac, and Tiark Rompf
(Augusta University, USA; Purdue University, USA; Tufts University, USA; EPFL, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Incremental Bidirectional Typing via Order Maintenance
Thomas J. Porter, Marisa Kirisame, Ivan Wei, Pavel Panchekha, and Cyrus Omar
(University of Michigan, USA; University of Utah, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced ACM SIGPLAN Distinguished Paper Award

Quantization with Guaranteed Floating-Point Neural Network Classifications
Anan Kabaha and Dana Drachsler Cohen
(Technion, Israel)

Publisher's Version

A Refinement Methodology for Distributed Programs in Rust
Aurel Bílý, João Pereira, and Peter Müller
(ETH Zurich, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Divide and Conquer: A Compositional Approach to Game-Theoretic Security
Ivana Bocevska, Anja Petković Komel, Laura Kovács, Sophie Rain, and Michael Rawson
(TU Wien, Austria; Argot Collective, Switzerland; University of Southampton, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Automated Discovery of Tactic Libraries for Interactive Theorem Proving
Yutong Xin, Jimmy Xin, Gabriel Poesia, Noah D. Goodman, Qiaochu Chen, and Işıl Dillig
(University of Texas at Austin, USA; Stanford University, USA; New York University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Place Capability Graphs: A General-Purpose Model of Rust’s Ownership and Borrowing Guarantees
Zachary Grannan, Aurel Bílý, Jonáš Fiala, Jasper Geer, Markus de Medeiros, Peter Müller, and Alexander J. Summers
(University of British Columbia, Canada; ETH Zurich, Switzerland; New York University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Efficient Decrease-and-Conquer Linearizability Monitoring
Zheng Han Lee and Umang Mathur
(National University of Singapore, Singapore)

Publisher's Version Published Artifact Artifacts Available

Debugging WebAssembly? Put Some Whamm on It!
Elizabeth Gilbert, Matthew Schneider, Zixi An, Suhas Thalanki, Wavid Bowman, Alexander Y. Bai, Ben L. Titzer, and Heather Miller
(Carnegie Mellon University, USA; University of Florida, USA; New York University, USA)

Publisher's Version Published Artifact Artifacts Available

Sound and Modular Activity Analysis for Automatic Differentiation in MLIR
Mai Jacob Peng, William S. Moses, Oleksandr Zinenko, and Christophe Dubach
(McGill University, Canada; University of Illinois at Urbana-Champaign, USA; Brium, France; Mila, Canada)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Flix: A Design for Language-Integrated Datalog
Magnus Madsen and Ondřej Lhoták
(Aarhus University, Denmark; University of Waterloo, Canada)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

SafeTree: Expressive Tree Policies for Microservices
Karuna Grewal, Brighten Godfrey, and Justin Hsu
(Cornell University, USA; University of Illinois at Urbana-Champaign, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

TraceLinking Implementations with Their Verified Designs
Finn Hackett and Ivan Beschastnikh
(University of British Columbia, Canada)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Universal Scalability in Declarative Program Analysis (with Choice-Based Combination Pruning)
Anastasios Antoniadis, Ilias Tsatiris, Neville Grech, and Yannis Smaragdakis
(University of Athens, Greece; Dedaub, Greece; University of Malta, Malta; Dedaub, Malta)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Results Reproduced

Verifying Asynchronous Hyperproperties in Reactive Systems
Raven Beutner and Bernd Finkbeiner
(CISPA Helmholtz Center for Information Security, Germany)

Publisher's Version

Synthesizing Implication Lemmas for Interactive Theorem Proving
Ana Brendel, Aishwarya Sivaraman, and Todd Millstein
(University of California at Los Angeles, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

AccelerQ: Accelerating Quantum Eigensolvers with Machine Learning on Quantum Simulators
Avner Bensoussan, Elena Chachkarova, Karine Even-Mendoza, Sophie Fortz, and Connor Lenihan
(King’s College London, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Modular Reasoning about Global Variables and Their Initialization
João Pereira, Isaac van Bakel, Patricia Firlejczyk, Marco Eilers, and Peter Müller
(ETH Zurich, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Modal Abstractions for Virtualizing Memory Addresses
Ismail Kuru and Colin S. Gordon
(Drexel University, USA)

Publisher's Version

A Language for Quantifying Quantum Network Behavior
Anita Buckley, Pavel Chuprikov, Rodrigo Otoni, Robert Soulé, Robert Rand, and Patrick Eugster
(USI Lugano, Switzerland; Télécom Paris, France; Institut Polytechnique de Paris, France; Yale University, USA; University of Chicago, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

MIO: Multiverse Debugging in the Face of Input/Output
Tom Lauwaerts, Maarten Steevens, and Christophe Scholliers
(Universiteit Gent, Belgium)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Cost of Soundness in Mixed-Precision Tuning
Anastasia Isychev and Debasmita Lohar
(TU Wien, Austria; KIT, Germany)

Publisher's Version Published Artifact Artifacts Available

Encode the ∀∃ Relational Hoare Logic into Standard Hoare Logic
Shushu Wu, Xiwei Wu, and Qinxiang Cao
(Shanghai Jiao Tong University, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Work Packets: A New Abstraction for GC Software Engineering, Optimization, and Innovation
Wenyu Zhao, Stephen M. Blackburn, and Kathryn S. McKinley
(Australian National University, Australia; Google, Australia; Google, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Abstract Interpretation of Temporal Safety Effects of Higher Order Programs
Mihai Nicola, Chaitanya Agarwal, Eric Koskinen, and Thomas Wies
(Stevens Institute of Technology, USA; New York University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

ApkDiffer: Accurate and Scalable Cross-Version Diffing Analysis for Android Applications
Jiarun Dai, Mingyuan Luo, Yuan Zhang, Min Yang, and Minghui Yang
(Fudan University, China; OPPO, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Software Model Checking via Summary-Guided Search
Ruijie Fang, Zachary Kincaid, and Thomas Reps
(University of Texas at Austin, USA; Princeton University, USA; University of Wisconsin, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Opportunistically Parallel Lambda Calculus
Stephen Mell, Konstantinos Kallas, Steve Zdancewic, and Osbert Bastani
(University of Pennsylvania, USA; University of California at Los Angeles, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

A Lightweight Type-and-Effect System for Invalidation Safety: Tracking Permanent and Temporary Invalidation with Constraint-Based Subtype Inference
Cunyuan Gao and Lionel Parreaux
(Hong Kong University of Science and Technology, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

P³: Reasoning about Patches via Product Programs
Arindam Sharma, Daniel Schemmel, and Cristian Cadar
(Imperial College London, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

The Continuous Tensor Abstraction: Where Indices Are Real
Jaeyeon Won, Willow Ahrens, Teodoro Fields Collin, Joel S. Emer, and Saman Amarasinghe
(Massachusetts Institute of Technology, USA; Georgia Institute of Technology, USA; NVIDIA, USA)

Publisher's Version

Translation Validation for LLVM’s AArch64 Backend
Ryan Berger, Mitch Briles, Nader Boushehrinejad Moradi, Nicholas Coughlin, Kait Lam, Nuno P. Lopes, Stefan Mada, Tanmay Tirpankar, and John Regehr
(NVIDIA, USA; University of Utah, USA; Defence Science and Technology Group, Australia; University of Queensland, Australia; INESC-ID, Portugal; Instituto Superior Técnico - University of Lisbon, Portugal)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Certified Decision Procedures for Width-Independent Bitvector Predicates
Siddharth Bhat, Léo Stefanesco, Chris Hughes, and Tobias Grosser
(University of Cambridge, UK; Independent Researcher, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

CoSSJIT: Combining Static Analysis and Speculation in JIT Compilers
Aditya Anand, Vijay Sundaresan, Daryl Maier, and Manas Thakur
(IIT Bombay, India; IBM, Canada)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Mini-Batch Robustness Verification of Deep Neural Networks
Saar Tzour-Shaday and Dana Drachsler-Cohen
(Technion, Israel)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Compositional Symbolic Execution for the Next 700 Memory Models
Andreas Lööw, Seung Hoon Park, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Opale Sjöstedt, and Philippa Gardner
(Imperial College London, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing
Qiong Feng, Xiaotian Ma, Ziyuan Feng, Marat Akhin, Wei Song, and Peng Liang
(Nanjing University of Science and Technology, China; JetBrains, Netherlands; Wuhan University, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Scalable Equivalence Checking and Verification of Shallow Quantum Circuits
Nengkun Yu, Xuan Du Trinh, and Thomas Reps
(Stony Brook University, USA; University of Wisconsin, USA)

Publisher's Version

Extraction and Mutation at a High Level: Template-Based Fuzzing for JavaScript Engines
Wai Kin Wong, Dongwei Xiao, Cheuk Tung Lai, Yiteng Peng, Daoyuan Wu, and Shuai Wang
(Hong Kong University of Science and Technology, Hong Kong; VX Research, UK; Lingnan University, Hong Kong)

Publisher's Version

Dynamic Wind for Effect Handlers
David Voigt, Philipp Schuster, and Jonathan Immanuel Brachthäuser
(University of Tübingen, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Detecting and Explaining (In-)equivalence of Context-Free Grammars
Marko Schmellenkamp, Thomas Zeume, Sven Argo, Sandra Kiefer, Cedric Siems, and Fynn Stebel
(Ruhr University Bochum, Germany; University of Oxford, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Embedding Quantum Program Verification into Dafny
Feifei Cheng, Sushen Vangeepuram, Henry Allard, Seyed Mohammad Reza Jafari, Alex Potanin, and Liyi Li
(Iowa State University, USA; Australian National University, Australia)

Publisher's Version Info

We’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators
Patrick LaFontaine, Zhe Zhou, Ashish Mishra, Suresh Jagannathan, and Benjamin Delaware
(Purdue University, USA; IIT Hyderabad, India)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes
Mingyi Li, Junmin Xiao, Siyan Chen, Hui Ma, Xi Chen, Peihua Bao, Liang Yuan, and Guangming Tan
(Institute of Computing Technology at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Products of Recursive Programs for Hypersafety Verification
Ruotong Cheng and Azadeh Farzan
(University of Toronto, Canada)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

DESIL: Detecting Silent Bugs in MLIR Compiler Infrastructure
Chenyao Suo, Jianrong Wang, Yongjia Wang, Jiajun Jiang, Qingchao Shen, and Junjie Chen
(Tianjin University, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Results Reproduced

HieraSynth: A Parallel Framework for Complete Super-Optimization with Hierarchical Space Decomposition
Sirui Lu and Rastislav Bodík
(University of Washington, USA; Google DeepMind, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Large Language Model Powered Symbolic Execution
Yihe Li, Ruijie Meng, and Gregory J. Duck
(National University of Singapore, Singapore)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

Proof Repair across Quotient Type Equivalences
Cosmo Viola, Max Fan, and Talia Ringer
(University of Illinois at Urbana-Champaign, USA; Cornell University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

The Power of Regular Constraint Propagation
Matthew Hague, Artur Jeż, Anthony Widjaja Lin, Oliver Markgraf, and Philipp Rümmer
(Royal Holloway University of London, UK; University of Wrocław, Poland; RPTU Kaiserslautern-Landau, Germany; MPI-SWS, Germany; University of Regensburg, Germany; Uppsala University, Sweden)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

On Abstraction Refinement for Bayesian Program Analysis
Yuanfeng Shi, Yifan Zhang, and Xin Zhang
(Peking University, China)

Publisher's Version Published Artifact Artifacts Available

Interactive Bitvector Reasoning using Verified Bit-Blasting
Henrik Böving, Siddharth Bhat, Luisa Cicolini, Alex Keizer, Léon Frenot, Abdalrhman Mohamed, Léo Stefanesco, Harun Khan, Joshua Clune, Clark Barrett, and Tobias Grosser
(Lean FRO, Germany; University of Cambridge, UK; ENS Lyon, France; Stanford University, USA; Carnegie Mellon University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

The Simple Essence of Overloading: Making Ad-Hoc Polymorphism More Algebraic with Flow-Based Variational Type-Checking
Jiří Beneš and Jonathan Immanuel Brachthäuser
(University of Tübingen, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

ROSpec: A Domain-Specific Language for ROS-Based Robot Software
Paulo Canelas, Bradley Schmerl, Alcides Fonseca, and Christopher S. Timperley
(Carnegie Mellon University, USA; University of Lisbon, Portugal)

Publisher's Version Published Artifact Info Artifacts Available Artifacts Reusable Results Reproduced

Enhancing APR with PRISM: A Semantic-Based Approach to Overfitting Patch Detection
Dowon Song and Hakjoo Oh
(Korea University, Republic of Korea)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Results Reproduced

Validating Soundness and Completeness in Pattern-Match Coverage Analyzers
Cyril Flurin Moser, Thodoris Sotiropoulos, Chengyu Zhang, and Zhendong Su
(ETH Zurich, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Complete the Cycle: Reachability Types with Expressive Cyclic References
Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, and Tiark Rompf
(Purdue University, USA; Augusta University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Borrowing from Session Types
Hannes Saffrich, Janek Spaderna, Peter Thiemann, and Vasco T. Vasconcelos
(University of Freiburg, Germany; University of Lisbon, Portugal)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

AutoVerus: Automated Proof Generation for Rust Code
Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jacob R. Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, and Shan Lu
(University of Illinois at Urbana-Champaign, USA; Columbia University, USA; University of California at Irvine, USA; University of Toronto, Canada; Microsoft Research, USA; Microsoft Research, China; University of Chicago, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

HeapBuffers: Why Not Just Using a Binary Serialization Format for Your Managed Memory?
Daniele Bonetta, Júnior Löff, Matteo Basso, and Walter Binder
(Vrije Universiteit Amsterdam, Netherlands; USI Lugano, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced ACM SIGPLAN Distinguished Paper Award

Tunneling through the Hill: Multi-way Intersection for Version-Space Algebras in Program Synthesis
Guanlin Chen, Ruyi Ji, Shuhao Zhang, and Yingfei Xiong
(Peking University, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Results Reproduced

Zero-Overhead Lexical Effect Handlers
Cong Ma, Zhaoyi Ge, Max Jung, and Yizhou Zhang
(University of Waterloo, Canada)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Multi-modal Sketch-Based Behavior Tree Synthesis
Wenmeng Zhang, Zhenbang Chen, and Weijiang Hong
(National University of Defense Technology, Changsha, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Results Reproduced

Garbage Collection for Rust: The Finalizer Frontier
Jacob Hughes and Laurence Tratt
(King’s College London, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Divining Profiler Accuracy: An Approach to Approximate Profiler Accuracy through Machine Code-Level Slowdown
Humphrey Burchell and Stefan Marr
(University of Kent, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

On the Impact of Formal Verification on Software Development
Eric Mugnier, Yuanyuan Zhou, Ranjit Jhala, and Michael Coblenz
(University of California at San Diego, USA)

Publisher's Version Published Artifact Artifacts Available

Syntactic Completions with Material Obligations
David Moon, Andrew Blinn, Thomas J. Porter, and Cyrus Omar
(University of Michigan, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Faster Explicit-Trace Monitoring-Oriented Programming for Runtime Verification of Software Tests
Kevin Guan, Marcelo d'Amorim, and Owolabi Legunsen
(Cornell University, USA; North Carolina State University, USA)

Publisher's Version

On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs
Taro Sekiyama, Ugo Dal Lago, and Hiroshi Unno
(National Institute of Informatics, Japan; SOKENDAI, Japan; University of Bologna, Italy; Inria, France; Tohoku University, Japan)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Results Reproduced

DepFuzz: Efficient Smart Contract Fuzzing with Function Dependence Guidance
Chenyang Ma, Wei Song, and Jeff Huang
(Nanjing University of Science and Technology, China; Texas A&M University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Type-Outference with Label-Listeners: Foundations for Decidable Type-Consistency for Nominal Object-Oriented Generics
Ross Tate
(Independent Researcher and Consultant, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Integrating Resource Analyses via Resource Decomposition
Long Pham, Yue Niu, Nathan Glover, Feras Saad, and Jan Hoffmann
(Carnegie Mellon University, USA; National Institute of Informatics, Japan)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

A Flow-Sensitive Refinement Type System for Verifying eBPF Programs
Ameer Hamza, Lucas Zavalía, Arie Gurfinkel, Jorge A. Navas, and Grigory Fedyukovich
(Florida State University, USA; University of Waterloo, Canada; Certora, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

An Empirical Study of Bugs in the rustc Compiler
Zixi Liu, Yang Feng, Yunbo Ni, Shaohua Li, Xizhe Yin, Qingkai Shi, Baowen Xu, and Zhendong Su
(Nanjing University, China; Chinese University of Hong Kong, China; ETH Zurich, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

An Empirical Evaluation of Property-Based Testing in Python
Savitha Ravi and Michael Coblenz
(University of California at San Diego, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Bennet: Randomized Specification Testing for Heap-Manipulating Programs
Zain K Aamer and Benjamin C. Pierce
(University of Pennsylvania, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Structural Information Flow: A Fresh Look at Types for Non-interference
Hemant Gouni, Frank Pfenning, and Jonathan Aldrich
(Carnegie Mellon University, USA)

Publisher's Version Published Artifact Artifacts Available

From Linearity to Borrowing
Andrew Wagner, Olek Gierczak, Brianna Marshall, John M. Li, and Amal Ahmed
(Northeastern University, USA)

Publisher's Version ACM SIGPLAN Distinguished Paper Award

Advancing Performance via a Systematic Application of Research and Industrial Best Practice
Wenyu Zhao, Stephen M. Blackburn, Kathryn S. McKinley, Man Cao, and Sara S. Hamouda
(Australian National University, Australia; Google, Australia; Google, USA; Canva, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM
Ao Li, Byeongjee Kang, Vasudev Vikram, Isabella Laybourn, Samvid Dharanikota, Shrey Tiwari, and Rohan Padhye
(Carnegie Mellon University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

Scaling Instruction-Selection Verification against Authoritative ISA Semantics
Michael McLoughlin, Ashley Sheng, Chris Fallin, Bryan Parno, Fraser Brown, and Alexa VanHattum
(Carnegie Mellon University, USA; Wellesley College, USA; F5, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

Contract System Metatheories à la Carte: A Transition-System View of Contracts
Shu-Hung You, Christos Dimoulas, and Robert Bruce Findler
(Northwestern University, USA)

Publisher's Version Info

Corrigendum: 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