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

Title Page

Article: oopslab26foreword-fm000-p doi:

Sponsors

Article: oopslab26foreword-fm003-p doi:

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

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

Probabilistic Floating-Point Round-Off Analysis via Concentration Inequalities
Yichen Tao, Hongfei Fu, Jiawei Chen, and Jean-Baptiste Jeannin
(University of Michigan, USA; Shanghai 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)

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)

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)

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

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)

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)

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)

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

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)

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)

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)

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)

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)

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

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

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