OOPSLA2 2024
Proceedings of the ACM on Programming Languages, Volume 8, Number OOPSLA2

Title Page

Article: oopslab24foreword-fm000-p (type: Frontmatter) doi:

Editorial Message

Article: oopslab24foreword-fm001-p (type: Frontmatter) doi:

OOPSLA 2024 Sponsors and Supporters

Article: oopslab24foreword-fm003-p (type: Frontmatter) doi:

VarLifter: Recovering Variables and Types from Bytecode of Solidity Smart Contracts
Yichuan Li, Wei Song, and Jeff Huang
(Nanjing University of Science and Technology, China; Texas A&M University, USA)

Publisher's Version Artifacts Functional Article: oopslab24main-p55-p (type: Full Paper) doi:10.1145/3689711

A Dependent Nominal Physical Type System for Static Analysis of Memory in Low Level Code
Julien Simonnet, Matthieu Lemerre, and Mihaela Sighireanu
(University Paris-Saclay - CEA - List, France; University Paris-Saclay - ENS Paris-Saclay - CNRS - LMF, France)

Publisher's Version Artifacts Reusable Article: oopslab24main-p115-p (type: Full Paper) doi:10.1145/3689712

Object-Oriented Fixpoint Programming with Datalog
David Klopp, Sebastian Erdweg, and André Pacak
(JGU Mainz, Germany)

Publisher's Version Article: oopslab24main-p130-p (type: Full Paper) doi:10.1145/3689713

Intensional Functions
Zachary Palmer, Nathaniel Wesley Filardo, and Ke Wu
(Swarthmore College, USA; Microsoft, Canada; Johns Hopkins University, USA)

Publisher's Version Artifacts Functional Results Reproduced Article: oopslab24main-p138-p (type: Full Paper) doi:10.1145/3689714

Intensional Functions: Appendices: The appendices accompanying the paper Intensional Functions from OOPSLA '24.

Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs
Shaan Nagy, Jinwoo Kim, Thomas Reps, and Loris D’Antoni
(University of Wisconsin-Madison, USA; Seoul National University, South Korea; University of California at San Diego, USA)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p155-p (type: Full Paper) doi:10.1145/3689715

Statistical Testing of Quantum Programs via Fixed-Point Amplitude Amplification
Chan Gu Kang, Joonghoon Lee, and Hakjoo Oh
(Korea University, South Korea)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p157-p (type: Full Paper) doi:10.1145/3689716

A Low-Level Look at A-Normal Form
William J. Bowman
(University of British Columbia, Canada)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p159-p (type: Full Paper) doi:10.1145/3689717

Full Iso-Recursive Types
Litao Zhou, Qianyong Wan, and Bruno C. d. S. Oliveira
(University of Hong Kong, China)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p161-p (type: Full Paper) doi:10.1145/3689718

SMT2Test: From SMT Formulas to Effective Test Cases
Chengyu Zhang and Zhendong Su
(ETH Zurich, Switzerland)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p166-p (type: Full Paper) doi:10.1145/3689719

Non-termination Proving at Scale
Azalea Raad, Julien Vanegue, and Peter O’Hearn
(Imperial College London, United Kingdom; Bloomberg, USA; University College London, United Kingdom)

Publisher's Version Artifacts Reusable Article: oopslab24main-p173-p (type: Full Paper) doi:10.1145/3689720

Compiler Support for Sparse Tensor Convolutions
Peiming Liu, Alexander J Root, Anlun Xu, Yinying Li, Fredrik Kjolstad, and Aart J.C. Bik
(Google Research, USA; Stanford University, USA; Google Cloud, USA)

Publisher's Version Artifacts Functional Article: oopslab24main-p178-p (type: Full Paper) doi:10.1145/3689721

Iris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssembly
Maxime Legoupil, June Rousseau, Aïna Linn Georges, Jean Pichon-Pharabod, and Lars Birkedal
(Aarhus University, Denmark; MPI-SWS, Germany)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p189-p (type: Full Paper) doi:10.1145/3689722

libLISA: Instruction Discovery and Analysis on x86-64
Jos Craaijo, Freek Verbeek, and Binoy Ravindran
(Open Universiteit, Netherlands; Virginia Tech, USA)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p204-p (type: Full Paper) doi:10.1145/3689723

Synthesizing Formal Semantics from Executable Interpreters
Jiangyi Liu, Charlie Murphy, Anvay Grover, Keith J.C. Johnson, Thomas Reps, and Loris D’Antoni
(University of Wisconsin-Madison, USA; University of California at San Diego, USA)

Publisher's Version Artifacts Functional Results Reproduced Article: oopslab24main-p208-p (type: Full Paper) doi:10.1145/3689724

A Modal Type Theory of Expected Cost in Higher-Order Probabilistic Programs
Vineet Rajani, Gilles Barthe, and Deepak Garg
(University of Kent, United Kingdom; MPI-SP, Germany; IMDEA Software Institute, Spain; MPI-SWS, Germany)

Publisher's Version Article: oopslab24main-p256-p (type: Full Paper) doi:10.1145/3689725

Sensitivity by Parametricity
Elisabet Lobo-Vesga, Alejandro Russo, Marco Gaboardi, and Carlos Tomé Cortiñas
(DPella, Sweden; Chalmers University of Technology, Sweden; Boston University, USA)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p262-p (type: Full Paper) doi:10.1145/3689726

Accompanying Material: This document contains the examples, formalizations, and discussions that were not included in the manuscript due to space constraints.

Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics Implementations
Luke Geeson, James Brotherston, Wilco Dijkstra, Alastair F. Donaldson, Lee Smith, Tyler Sorensen, and John Wickerson
(University College London, United Kingdom; Arm, United Kingdom; Imperial College London, United Kingdom; University of California at Santa Cruz, USA)

Publisher's Version Artifacts Functional Article: oopslab24main-p264-p (type: Full Paper) doi:10.1145/3689727

Statically Contextualizing Large Language Models with Typed Holes
Andrew Blinn, Xiang Li, June Hyung Kim, and Cyrus Omar
(University of Michigan, USA)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p278-p (type: Full Paper) doi:10.1145/3689728

FlowCert: Translation Validation for Asynchronous Dataflow via Dynamic Fractional Permissions
Zhengyao Lin, Joshua Gancher, and Bryan Parno
(Carnegie Mellon University, USA)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p282-p (type: Full Paper) doi:10.1145/3689729

SparseAuto: An Auto-scheduler for Sparse Tensor Computations using Recursive Loop Nest Restructuring
Adhitha Dias, Logan Anderson, Kirshanthan Sundararajah, Artem Pelenitsyn, and Milind Kulkarni
(Purdue University, USA; Virginia Tech, USA)

Publisher's Version Article: oopslab24main-p286-p (type: Full Paper) doi:10.1145/3689730

Quantum Probabilistic Model Checking for Time-Bounded Properties
Seungmin Jeon, Kyeongmin Cho, Chan Gu Kang, Janggun Lee, Hakjoo Oh, and Jeehoon Kang
(KAIST, South Korea; Korea University, South Korea)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p288-p (type: Full Paper) doi:10.1145/3689731

Verified Lock-Free Session Channels with Linking
Thomas Somers and Robbert Krebbers
(Radboud University Nijmegen, Netherlands)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p289-p (type: Full Paper) doi:10.1145/3689732

Crabtree: Rust API Test Synthesis Guided by Coverage and Type
Yoshiki Takashima, Chanhee Cho, Ruben Martins, Limin Jia, and Corina S. Păsăreanu
(Carnegie Mellon University, USA)

Publisher's Version Article: oopslab24main-p295-p (type: Full Paper) doi:10.1145/3689733

Merging Gradual Typing
Wenjia Ye, Bruno C. d. S. Oliveira, and Matías Toro
(University of Hong Kong, China; University of Chile, Chile)

Publisher's Version Artifacts Functional Article: oopslab24main-p296-p (type: Full Paper) doi:10.1145/3689734

Knowledge Transfer from High-Resource to Low-Resource Programming Languages for Code LLMs
Federico Cassano, John Gouwar, Francesca Lucchetti, Claire Schlesinger, Anders Freeman, Carolyn Jane Anderson, Molly Q Feldman, Michael Greenberg, Abhinav Jangda, and Arjun Guha
(Northeastern University, USA; Wellesley College, USA; Oberlin College, USA; Stevens Institute of Technology, USA; Microsoft Research, USA; Roblox, USA)

Publisher's Version Artifacts Functional Results Reproduced Article: oopslab24main-p302-p (type: Full Paper) doi:10.1145/3689735

WhiteFox: White-Box Compiler Fuzzing Empowered by Large Language Models
Chenyuan Yang, Yinlin Deng, Runyu Lu, Jiayi Yao, Jiawei Liu, Reyhaneh Jabbarvand, and Lingming Zhang
(University of Illinois at Urbana-Champaign, USA; Huazhong University of Science and Technology, China; Chinese University of Hong Kong, Shenzhen, China)

Publisher's Version Article: oopslab24main-p305-p (type: Full Paper) doi:10.1145/3689736

HiPy: Extracting High-Level Semantics from Python Code for Data Processing
Michael Jungmair, Alexis Engelke, and Jana Giceva
(TU Munich, Germany)

Publisher's Version Artifacts Functional Results Reproduced Article: oopslab24main-p306-p (type: Full Paper) doi:10.1145/3689737

Automatically Reducing Privilege for Access Control Policies
Loris D’Antoni, Shuo Ding, Amit Goel, Mathangi Ramesh, Neha Rungta, and Chungha Sung
(Amazon Web Services, USA; Georgia Institute of Technology, USA)

Publisher's Version Article: oopslab24main-p307-p (type: Full Paper) doi:10.1145/3689738

Fully Verified Instruction Scheduling
Ziteng Yang, Jun Shirako, and Vivek Sarkar
(Georgia Institute of Technology, USA)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p343-p (type: Full Paper) doi:10.1145/3689739

Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate Transformers
Linpeng Zhang, Noam Zilberstein, Benjamin Lucien Kaminski, and Alexandra Silva
(University College London, United Kingdom; Cornell University, USA; Saarland University, Germany)

Publisher's Version Article: oopslab24main-p346-p (type: Full Paper) doi:10.1145/3689740

CoolerSpace: A Language for Physically Correct and Computationally Efficient Color Programming
Ethan Chen, Jiwon Chang, and Yuhao Zhu
(University of Rochester, USA)

Publisher's Version Article: oopslab24main-p354-p (type: Full Paper) doi:10.1145/3689741

CoolerSpace Supplementary Materials: Contains a comprehensive list of syntax and type rules for CoolerSpace. Also contains proofs of translational and type soundness, the equality saturation rules used in CoolerSpace, and a copy of the benchmarking programs.

Plume: Efficient and Complete Black-Box Checking of Weak Isolation Levels
Si Liu, Long Gu, Hengfeng Wei, and David Basin
(ETH Zurich, Switzerland; Nanjing University, China)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p362-p (type: Full Paper) doi:10.1145/3689742

Computing Precise Control Interface Specifications
Eric Hayden Campbell, Hossein Hojjat, and Nate Foster
(Cornell University, USA; Tehran Institute for Advanced Studies, Iran)

Publisher's Version Artifacts Reusable Article: oopslab24main-p369-p (type: Full Paper) doi:10.1145/3689743

Automating Pruning in Top-Down Enumeration for Program Synthesis Problems with Monotonic Semantics
Keith J.C. Johnson, Rahul Krishnan, Thomas Reps, and Loris D’Antoni
(University of Wisconsin-Madison, USA; University of California at San Diego, USA)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p377-p (type: Full Paper) doi:10.1145/3689744

Refinement Type Refutations
Robin Webbers, Klaus von Gleissenthall, and Ranjit Jhala
(Vrije Universiteit Amsterdam, Netherlands; University of California at San Diego, USA)

Publisher's Version Article: oopslab24main-p378-p (type: Full Paper) doi:10.1145/3689745

	Soundness and Completeness Proof: This document contains the soundness and correctness proof which was mentioned in the paper. The typing rules used in the proof may be found in another appendix of this paper.
	Typing Judgements: Lists the typing judgements used in the paper. Additionally contains the typing judgements used to prove soundness and correctness as mentioned in the paper. The proof itself is contained in another appendix.

The Ultimate Conditional Syntax
Luyu Cheng and Lionel Parreaux
(Hong Kong University of Science and Technology, Hong Kong)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p386-p (type: Full Paper) doi:10.1145/3689746

On the Expressive Power of Languages for Static Variability
Paul Maximilian Bittner, Alexander Schultheiß, Benjamin Moosherr, Jeffrey M. Young, Leopoldo Teixeira, Eric Walkingshaw, Parisa Ataei, and Thomas Thüm
(University of Paderborn, Germany; Ulm University, Germany; University of Bern, Switzerland; IOHK, USA; Federal University of Pernambuco, Brazil; Unaffiliated, USA; TU Braunschweig, Germany)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p390-p (type: Full Paper) doi:10.1145/3689747

Programmable MCMC with Soundly Composed Guide Programs
Long Pham, Di Wang, Feras A. Saad, and Jan Hoffmann
(Carnegie Mellon University, USA; Peking University, China)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p391-p (type: Full Paper) doi:10.1145/3689748

Appendix to the paper: Appendix to the paper

Extending the C/C++ Memory Model with Inline Assembly
Paulo Emílio de Vilhena, Ori Lahav, Viktor Vafeiadis, and Azalea Raad
(Imperial College London, United Kingdom; Tel Aviv University, Israel; MPI-SWS, Germany)

Publisher's Version Article: oopslab24main-p392-p (type: Full Paper) doi:10.1145/3689749

Effects and Coeffects in Call-by-Push-Value
Cassia Torczon, Emmanuel Suárez Acevedo, Shubh Agrawal, Joey Velez-Ginorio, and Stephanie Weirich
(University of Pennsylvania, USA; University of Michigan, USA)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p398-p (type: Full Paper) doi:10.1145/3689750

Gradient: Gradual Compartmentalization via Object Capabilities Tracked in Types
Aleksander Boruch-Gruszecki, Adrien Ghosn, Mathias Payer, and Clément Pit-Claudel
(Charles University, Czechia; Microsoft Research, United Kingdom; EPFL, Switzerland)

Publisher's Version Article: oopslab24main-p402-p (type: Full Paper) doi:10.1145/3689751

Compilation of Shape Operators on Sparse Arrays
Alexander J Root, Bobby Yan, Peiming Liu, Christophe Gyurgyik, Aart J.C. Bik, and Fredrik Kjolstad
(Stanford University, USA; Google Research, USA)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p404-p (type: Full Paper) doi:10.1145/3689752

Tachis: Higher-Order Separation Logic with Credits for Expected Costs
Philipp G. Haselwarter, Kwing Hei Li, Markus de Medeiros, Simon Oddershede Gregersen, Alejandro Aguirre, Joseph Tassarotti, and Lars Birkedal
(Aarhus University, Denmark; New York University, USA)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p414-p (type: Full Paper) doi:10.1145/3689753

Making Formulog Fast: An Argument for Unconventional Datalog Evaluation
Aaron Bembenek, Michael Greenberg, and Stephen Chong
(University of Melbourne, Australia; Stevens Institute of Technology, USA; Harvard University, USA)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p434-p (type: Full Paper) doi:10.1145/3689754

Realistic Realizability: Specifying ABIs You Can Count On
Andrew Wagner, Zachary Eisbach, and Amal Ahmed
(Northeastern University, USA)

Publisher's Version Article: oopslab24main-p440-p (type: Full Paper) doi:10.1145/3689755

Technical Appendix: The technical appendix includes supporting definitions and proofs.

Hypra: A Deductive Program Verifier for Hyper Hoare Logic
Thibault Dardinier, Anqi Li, and Peter Müller
(ETH Zurich, Switzerland)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p468-p (type: Full Paper) doi:10.1145/3689756

PolyJuice: Detecting Mis-compilation Bugs in Tensor Compilers with Equality Saturation Based Rewriting
Chijin Zhou, Bingzhou Qian, Gwihwan Go, Quan Zhang, Shanshan Li, and Yu Jiang
(Tsinghua University, China; National University of Defense Technology, China)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p473-p (type: Full Paper) doi:10.1145/3689757

Semantics Lifting for Syntactic Sugar
Zhichao Guan, Yiyuan Cao, Tailai Yu, Ziheng Wang, Di Wang, and Zhenjiang Hu
(Peking University, China; Tsinghua University, China)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p481-p (type: Full Paper) doi:10.1145/3689758

MEA2: A Lightweight Field-Sensitive Escape Analysis with Points-to Calculation for Golang
Boyao Ding, Qingwei Li, Yu Zhang, Fugen Tang, and Jinbao Chen
(University of Science and Technology of China, China; Institute of Artificial Intelligence at Hefei Comprehensive National Science Center, China)

Publisher's Version Article: oopslab24main-p484-p (type: Full Paper) doi:10.1145/3689759

Weighted Context-Free-Language Ordered Binary Decision Diagrams
Meghana Sistla, Swarat Chaudhuri, and Thomas Reps
(University of Texas at Austin, USA; University of Wisconsin, USA)

Publisher's Version Artifacts Functional Results Reproduced Article: oopslab24main-p486-p (type: Full Paper) doi:10.1145/3689760

Finding ∀∃ Hyperbugs using Symbolic Execution
Arthur Correnson, Tobias Nießen, Bernd Finkbeiner, and Georg Weissenbacher
(CISPA Helmholtz Center for Information Security, Germany; TU Wien, Austria)

Publisher's Version Article: oopslab24main-p490-p (type: Full Paper) doi:10.1145/3689761

Multris: Functional Verification of Multiparty Message Passing in Separation Logic
Jonas Kastberg Hinrichsen, Jules Jacobs, and Robbert Krebbers
(Aarhus University, Denmark; Cornell University, USA; Radboud University Nijmegen, Netherlands)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p497-p (type: Full Paper) doi:10.1145/3689762

Law and Order for Typestate with Borrowing
Hannes Saffrich, Yuki Nishida, and Peter Thiemann
(University of Freiburg, Germany; Kyoto University, Japan)

Publisher's Version Article: oopslab24main-p498-p (type: Full Paper) doi:10.1145/3689763

FPCC: Detecting Floating-Point Errors via Chain Conditions
Xin Yi, Hengbiao Yu, Liqian Chen, Xiaoguang Mao, and Ji Wang
(National University of Defense Technology, China; National University of Defense Technology, Changsha, China)

Publisher's Version Artifacts Functional Results Reproduced Article: oopslab24main-p513-p (type: Full Paper) doi:10.1145/3689764

Scaling Abstraction Refinement for Program Analyses in Datalog using Graph Neural Networks
Zhenyu Yan, Xin Zhang, and Peng Di
(Peking University, China; Ant Group, China)

Publisher's Version Artifacts Functional Article: oopslab24main-p514-p (type: Full Paper) doi:10.1145/3689765

Minotaur: A SIMD-Oriented Synthesizing Superoptimizer
Zhengyang Liu, Stefan Mada, and John Regehr
(University of Utah, USA)

Publisher's Version Article: oopslab24main-p515-p (type: Full Paper) doi:10.1145/3689766

A Typed Multi-level Datalog IR and Its Compiler Framework
David Klopp, Sebastian Erdweg, and André Pacak
(JGU Mainz, Germany)

Publisher's Version Article: oopslab24main-p536-p (type: Full Paper) doi:10.1145/3689767

HardTaint: Production-Run Dynamic Taint Analysis via Selective Hardware Tracing
Yiyu Zhang, Tianyi Liu, Yueyang Wang, Yun Qi, Kai Ji, Jian Tang, Xiaoliang Wang, Xuandong Li, and Zhiqiang Zuo
(Nanjing University, China)

Publisher's Version Article: oopslab24main-p537-p (type: Full Paper) doi:10.1145/3689768

Jmvx: Fast Multi-threaded Multi-version Execution and Record-Replay for Managed Languages
David Schwartz, Ankith Kowshik, and Luís Pina
(University of Illinois, Chicago, USA)

Publisher's Version Article: oopslab24main-p540-p (type: Full Paper) doi:10.1145/3689769

Lexical Effect Handlers, Directly
Cong Ma, Zhaoyi Ge, Edward Lee, and Yizhou Zhang
(University of Waterloo, Canada)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p541-p (type: Full Paper) doi:10.1145/3689770

HybridSA: GPU Acceleration of Multi-pattern Regex Matching using Bit Parallelism
Alexis Le Glaunec, Lingkun Kong, and Konstantinos Mamouras
(Rice University, USA)

Publisher's Version Article: oopslab24main-p549-p (type: Full Paper) doi:10.1145/3689771

A Runtime System for Interruptible Query Processing: When Incremental Computing Meets Fine-Grained Parallelism
Jeff Eymer, Philip Dexter, Joseph Raskind, and Yu David Liu
(SUNY Binghamton, USA)

Publisher's Version Article: oopslab24main-p571-p (type: Full Paper) doi:10.1145/3689772

StarMalloc: Verifying a Modern, Hardened Memory Allocator
Antonin Reitz, Aymeric Fromherz, and Jonathan Protzenko
(Inria, France; Microsoft Research, USA)

Publisher's Version Artifacts Reusable Article: oopslab24main-p590-p (type: Full Paper) doi:10.1145/3689773

AUTOMAP: Inferring Rank-Polymorphic Function Applications with Integer Linear Programming
Robert Schenck, Nikolaj Hey Hinnerskov, Troels Henriksen, Magnus Madsen, and Martin Elsman
(University of Copenhagen, Denmark; Aarhus University, Denmark)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p607-p (type: Full Paper) doi:10.1145/3689774

Concurrent Data Structures Made Easy
Callista Le, Kiran Gopinathan, Koon Wen Lee, Seth Gilbert, and Ilya Sergey
(Yale-NUS College, Singapore; National University of Singapore, Singapore; Ahrefs, Singapore)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p608-p (type: Full Paper) doi:10.1145/3689775

Drowzee: Metamorphic Testing for Fact-Conflicting Hallucination Detection in Large Language Models
Ningke Li, Yuekang Li, Yi Liu, Ling Shi, Kailong Wang, and Haoyu Wang
(Huazhong University of Science and Technology, China; UNSW, Australia; Nanyang Technological University, Singapore)

Publisher's Version Article: oopslab24main-p613-p (type: Full Paper) doi:10.1145/3689776

Monotone Procedure Summarization via Vector Addition Systems and Inductive Potentials
Nikhil Pimpalkhare and Zachary Kincaid
(Princeton University, USA)

Publisher's Version Article: oopslab24main-p621-p (type: Full Paper) doi:10.1145/3689777

Model Checking Distributed Protocols in Must
Constantin Enea, Dimitra Giannakopoulou, Michalis Kokologiannakis, and Rupak Majumdar
(Amazon Web Services, France; École Polytechnique, France; Amazon Web Services, USA; ETH Zurich, Switzerland; Amazon Web Services, Germany; MPI-SWS, Germany)

Publisher's Version Article: oopslab24main-p646-p (type: Full Paper) doi:10.1145/3689778

Reward Augmentation in Reinforcement Learning for Testing Distributed Systems
Andrea Borgarelli, Constantin Enea, Rupak Majumdar, and Srinidhi Nagendra
(MPI-SWS, Germany; LIX - CNRS - École Polytechnique, France; IRIF - CNRS - Université Paris Cité, France; Chennai Mathematical Institute, India)

Publisher's Version Artifacts Functional Results Reproduced Article: oopslab24main-p657-p (type: Full Paper) doi:10.1145/3689779

Rustlantis: Randomized Differential Testing of the Rust Compiler
Qian Wang and Ralf Jung
(ETH Zurich, Switzerland; Imperial College London, United Kingdom)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p687-p (type: Full Paper) doi:10.1145/3689780

Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO Architectures
Guillaume Ambal, Brijesh Dongol, Haggai Eran, Vasileios Klimis, Ori Lahav, and Azalea Raad
(Imperial College London, United Kingdom; University of Surrey, United Kingdom; NVIDIA, Israel; Queen Mary University of London, United Kingdom; Tel Aviv University, Israel)

Publisher's Version Article: oopslab24main-p718-p (type: Full Paper) doi:10.1145/3689781

Imperative Compositional Programming: Type Sound Distributive Intersection Subtyping with References via Bidirectional Typing
Wenjia Ye, Yaozhu Sun, and Bruno C. d. S. Oliveira
(University of Hong Kong, China)

Publisher's Version Artifacts Functional Results Reproduced Article: oopslab24main-p723-p (type: Full Paper) doi:10.1145/3689782

QuAC: Quick Attribute-Centric Type Inference for Python
Jifeng Wu and Caroline Lemieux
(University of British Columbia, Canada)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p724-p (type: Full Paper) doi:10.1145/3689783

Automated Verification of Parametric Channel-Based Process Communication
Georgian-Vlad Saioc, Julien Lange, and Anders Møller
(Aarhus University, Denmark; Royal Holloway University of London, United Kingdom)

Publisher's Version Artifacts Reusable Article: oopslab24main-p731-p (type: Full Paper) doi:10.1145/3689784

Modular Synthesis of Efficient Quantum Uncomputation
Hristo Venev, Timon Gehr, Dimitar Dimitrov, and Martin Vechev
(Sofia University St. Kliment Ohridski, Bulgaria; ETH Zurich, Switzerland)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p732-p (type: Full Paper) doi:10.1145/3689785

Type Inference Logics
Denis Carnier, François Pottier, and Steven Keuchel
(KU Leuven, Belgium; Inria, France; Vrije Universiteit Brussel, Belgium)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p733-p (type: Full Paper) doi:10.1145/3689786

Wasm-R3: Record-Reduce-Replay for Realistic and Standalone WebAssembly Benchmarks
Doehyun Baek, Jakob Getz, Yusung Sim, Daniel Lehmann, Ben L. Titzer, Sukyoung Ryu, and Michael Pradel
(KAIST, South Korea; University of Stuttgart, Germany; Google, Germany; Carnegie Mellon University, USA)

Publisher's Version Article: oopslab24main-p738-p (type: Full Paper) doi:10.1145/3689787

Semantic-Type-Guided Bug Finding
Kelvin Qian, Scott Smith, Brandon Stride, Shiwei Weng, and Ke Wu
(Johns Hopkins University, USA)

Publisher's Version Artifacts Functional Article: oopslab24main-p743-p (type: Full Paper) doi:10.1145/3689788

Appendices of Semantic-Type-Guided Bug Finding: Included are appendices of the paper, Semantic-Type-Guided Bug Finding. The appendices contain proofs, additional operational semantics rules, and implementation details that are not covered fully in the paper.

Control-Flow Deobfuscation using Trace-Informed Compositional Program Synthesis
Benjamin Mariano, Ziteng Wang, Shankara Pailoor, Christian Collberg, and Işil Dillig
(University of Texas at Austin, USA; University of Arizona, USA)

Publisher's Version Artifacts Functional Article: oopslab24main-p746-p (type: Full Paper) doi:10.1145/3689789

Unifying Static and Dynamic Intermediate Languages for Accelerator Generators
Caleb Kim, Pai Li, Anshuman Mohan, Andrew Butt, Adrian Sampson, and Rachit Nigam
(Cornell University, USA)

Publisher's Version Artifacts Functional Results Reproduced Article: oopslab24main-p755-p (type: Full Paper) doi:10.1145/3689790

Mark–Scavenge: Waiting for Trash to Take Itself Out
Jonas Norlinder, Erik Österlund, David Black-Schaffer, and Tobias Wrigstad
(Uppsala University, Sweden; Oracle, Sweden)

Publisher's Version Article: oopslab24main-p774-p (type: Full Paper) doi:10.1145/3689791

Supplemental material: Supplemental tables for Mark-Scavenge

Compositionality and Observational Refinement for Linearizability with Crashes
Arthur Oliveira Vale, Zhongye Wang, Yixuan Chen, Peixin You, and Zhong Shao
(Yale University, USA)

Publisher's Version Article: oopslab24main-p794-p (type: Full Paper) doi:10.1145/3689792

Making Sense of Multi-threaded Application Performance at Scale with NonSequitur
Augustine Wong, Paul Bucci, Ivan Beschastnikh, and Alexandra Fedorova
(University of British Columbia, Canada)

Publisher's Version Artifacts Functional Results Reproduced Article: oopslab24main-p802-p (type: Full Paper) doi:10.1145/3689793

Dependency-Aware Code Naturalness
Chen Yang, Junjie Chen, Jiajun Jiang, and Yuliang Huang
(Tianjin University, China)

Publisher's Version Artifacts Functional Article: oopslab24main-p812-p (type: Full Paper) doi:10.1145/3689794

Validating SMT Solvers for Correctness and Performance via Grammar-Based Enumeration
Dominik Winterer and Zhendong Su
(ETH Zurich, Switzerland)

Publisher's Version Article: oopslab24main-p813-p (type: Full Paper) doi:10.1145/3689795

Practical Verification of Smart Contracts using Memory Splitting
Shelly Grossman, John Toman, Alexander Bakst, Sameer Arora, Mooly Sagiv, and Chandrakana Nandi
(Tel Aviv University, Israel; Certora, USA; Certora, Israel)

Publisher's Version Published Artifact Article: oopslab24main-p814-p (type: Full Paper) doi:10.1145/3689796

Appendix: Full paper with appendix

Sound and Partially-Complete Static Analysis of Data-Races in GPU Programs
Dennis Liew, Tiago Cogumbreiro, and Julien Lange
(University of Massachusetts, Boston, USA; Royal Holloway University of London, United Kingdom)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p855-p (type: Full Paper) doi:10.1145/3689797

Effect Handlers for C via Coroutines
Mario Alvarez-Picallo, Teodoro Freund, Dan R. Ghica, and Sam Lindley
(Huawei Research Centre, United Kingdom; University of Birmingham, United Kingdom; University of Edinburgh, United Kingdom)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p896-p (type: Full Paper) doi:10.1145/3689798

Effect Handlers for C via Coroutines - Extended: Extended version of Effect Handlers for C via Coroutines

When Your Infrastructure Is a Buggy Program: Understanding Faults in Infrastructure as Code Ecosystems
Georgios-Petros Drosos, Thodoris Sotiropoulos, Georgios Alexopoulos, Dimitris Mitropoulos, and Zhendong Su
(ETH Zurich, Switzerland; University of Athens, Greece)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p898-p (type: Full Paper) doi:10.1145/3689799

A Case for First-Class Environments
Jinhao Tan and Bruno C. d. S. Oliveira
(University of Hong Kong, China)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p903-p (type: Full Paper) doi:10.1145/3689800

Fast and Optimal Extraction for Sparse Equality Graphs
Amir Kafshdar Goharshady, Chun Kit Lam, and Lionel Parreaux
(Hong Kong University of Science and Technology, China)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p976-p (type: Full Paper) doi:10.1145/3689801

Automated Robustness Verification of Concurrent Data Structure Libraries against Relaxed Memory Models
Kartik Nagar, Anmol Sahoo, Romit Roy Chowdhury, and Suresh Jagannathan
(IIT Madras, India; Purdue University, USA; Chennai Mathematical Institute, India)

Publisher's Version Artifacts Reusable Results Reproduced Article: oopslab24main-p1014-p (type: Full Paper) doi:10.1145/3689802

The ART of Sharing Points-to Analysis: Reusing Points-to Analysis Results Safely and Efficiently
Shashin Halalingaiah, Vijay Sundaresan, Daryl Maier, and V. Krishna Nandivada
(IIT Madras, India; University of Texas at Austin, USA; IBM, Canada)

Publisher's Version Article: oopslab24main-p1030-p (type: Full Paper) doi:10.1145/3689803

Boosting the Performance of Alias-Aware IFDS Analysis with CFL-Based Environment Transformers
Haofeng Li, Chenghang Shi, Jie Lu, Lian Li, and Jingling Xue
(Institute of Computing Technology at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; Zhongguancun Laboratory, China; UNSW, Australia)

Publisher's Version Artifacts Functional Results Reproduced Article: oopslab24main-p1050-p (type: Full Paper) doi:10.1145/3689804

Higher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification
Taro Sekiyama and Hiroshi Unno
(National Institute of Informatics, Japan; SOKENDAI, Japan; Tohoku University, Japan)

Publisher's Version Article: oopslab24main-p1119-p (type: Full Paper) doi:10.1145/3689805

Supplementary Material for "Higher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification": This is the supplementary material of the paper titled "Higher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification" published at OOPSLA'24, including all the definitions, lemmas, theorems, and proofs mentioned in the paper.