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

Title Page

Editorial Message

OOPSLA 2024 Sponsors and Supporters

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 Published Artifact Artifacts Available Artifacts Functional

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 Published Artifact Info Artifacts Available Artifacts Reusable

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

Publisher's Version

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

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

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 Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

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 Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

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

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

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

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

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

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

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 Published Artifact Info Artifacts Available Artifacts Reusable

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

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 Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

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

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

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 Published Artifact Artifacts Available Artifacts Functional Results Reproduced

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

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 Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

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 Published Artifact Video Info Artifacts Available Artifacts Functional

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 Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

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

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

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 Published Artifact Artifacts Available

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 Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

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

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

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 Published Artifact Artifacts Available

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 Published Artifact Artifacts Available Artifacts Functional

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 Published Artifact Info Artifacts Available Artifacts Functional Results Reproduced

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

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

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

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

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

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

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

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 Published Artifact Artifacts Available

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 Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

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 Published Artifact Artifacts Available Artifacts Reusable

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 Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

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 Info

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

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

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 Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

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 Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

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

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 Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

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

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 Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

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 Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

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 Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

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

Publisher's Version

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

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

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 Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

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 Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

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

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 Published Artifact Artifacts Available Artifacts Functional Results Reproduced

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

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 Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

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

Publisher's Version

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 Published Artifact Artifacts Available Artifacts Functional Results Reproduced

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 Published Artifact Artifacts Available Artifacts Functional

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

Publisher's Version

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

Publisher's Version

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 Published Artifact Artifacts Available

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 Published Artifact Artifacts Available

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

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

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

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 Published Artifact Artifacts Available

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

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable

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 Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

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 Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

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

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

Publisher's Version Published Artifact Artifacts Available

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

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 Published Artifact Artifacts Available Artifacts Functional Results Reproduced

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

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

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 Info

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 Published Artifact Artifacts Available Artifacts Functional Results Reproduced

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

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

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 Published Artifact Artifacts Available Artifacts Reusable

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 Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

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

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

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 Published Artifact Artifacts Available

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

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

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 Published Artifact Artifacts Available Artifacts Functional

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 Published Artifact Artifacts Available Artifacts Functional Results Reproduced

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 Published Artifact Artifacts Available

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

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 Published Artifact Video Info Artifacts Available Artifacts Functional Results Reproduced

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

Publisher's Version Published Artifact Artifacts Available Artifacts Functional

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

Publisher's Version

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 Artifacts Available

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 Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

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 Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

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 Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

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

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

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 Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

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 Published Artifact Artifacts Available Artifacts Reusable Results Reproduced

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

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 Published Artifact Artifacts Available Artifacts Functional Results Reproduced

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 Info