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

Title Page

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

Sponsors

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

Editorial Message
Manu Sridharan
(University of California at Riverside, USA)

Publisher's Version Article: pldi26editorial-fm001-p (type: Editorial) doi:10.1145/3818664

FlexHeap: Dynamic I/O-Aware Heap Resizing for Managed Applications
Iacovos G. Kolokasis, Shoaib Akram, Foivos S. Zakkak, Polyvios Pratikakis, and Angelos Bilas
(Foundation for Research and Technology Hellas, Greece; University of Crete, Greece; Australian National University, Australia; Red Hat, Ireland)

Publisher's Version Published Artifact Artifacts Available Article: pldi26main-p2-p (type: Full Paper) doi:10.1145/3808247

FlexHeap: Dynamic I/O-Aware Heap Resizing for Managed Applications (doi:10.5281/zenodo.19183591): This artifact provides the setup, build, and runtime-support infrastructure for FlexHeap, a modified JVM for dynamic I/O-aware heap resizing in managed applications. The artifact is intended to help users reproduce the FlexHeap environment by installing the required dependencies, compiling the supporting eBPF ...

Fast Atomicity Monitoring
Hünkar Can Tunç, Yifan Dong, and Andreas Pavlogiannis
(Uber, Netherlands; Aarhus University, Denmark)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p10-p (type: Full Paper) doi:10.1145/3808248

AtomSanitizer (doi:10.5281/zenodo.19615809): Artifact of Fast Atomicity Monitoring

Versioned E-Graphs
Jahrim Gabriele Cesario, George Zakhour, Pascal Weisenburger, and Guido Salvaneschi
(University of St. Gallen, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p12-p (type: Full Paper) doi:10.1145/3808249

Versioned E-Graphs (doi:10.5281/zenodo.18769553): The artifact contains: - The mechanized formalism of versioned union-find in Lean4; - The implementation of versioned e-graphs and the parameter analysis; - The implementation of the EUF solver and its case study; - The implementation of the TheSy solver and its case study; - A Docker image for reproducing the results ...

Towards Removing Undef Values from LLVM IR
Pedro Lobo, John McIver, George Mitenkov, Juneyoung Lee, Kirshanthan Sundararajah, and Nuno P. Lopes
(INESC-ID, Portugal; Instituto Superior Técnico - University of Lisbon, Portugal; Virginia Tech, USA; Aptos Labs, UK; AWS, USA)

Publisher's Version ACM SIGPLAN Distinguished Paper Award Article: pldi26main-p14-p (type: Full Paper) doi:10.1145/3808250

A Deductive System for Contract Satisfaction Proofs
Arthur Correnson, Haoyi Zeng, and Jana Hofmann
(CISPA Helmholtz Center for Information Security, Germany; Harvard University, USA; MPI-SP, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p15-p (type: Full Paper) doi:10.1145/3808251

A Deductive System for Contract Satisfaction Proofs (doi:10.5281/zenodo.19054166): This artifact contains the Rocq development accompanying the PLDI submission "A Deductive System for Contract Satisfaction Proofs"

Path-Sensitive Abstract Interpretation for WCET Estimation
Shangshang Xiao, Mengxia Sun, Wei Zhang, Naijun Zhan, and Lei Ju
(Shandong University, China; Peking University, China; Zhongguancun Laboratory, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: pldi26main-p17-p (type: Full Paper) doi:10.1145/3808252

Path-Sensitive Abstract Interpretation for WCET Estimation (doi:10.5281/zenodo.19045049): This archive contains the artifact for the PLDI 2026 paper

Decoupling Data Layouts from Bounding Volume Hierarchies
Christophe Gyurgyik, Alexander J Root, and Fredrik Kjolstad
(Stanford University, USA)

Publisher's Version Published Artifact Artifacts Available Article: pldi26main-p19-p (type: Full Paper) doi:10.1145/3808253

	Appendix: Appendix for 'Decoupling Data Layouts from Bounding Volume Hierarchies'.
	Dataset for Design Space Exploration (9.2): Dataset for the Design Space Exploration evaluation described in Section 9.2.
	Reproduction Package for Article 'Decoupling Data Layouts from Bounding Volume Hierarchies' (doi:10.5281/zenodo.19009103): This artifact contains Scion, a domain-specific language and compiler for recursive geometric queries on bounding volume hierarchies (BVHs). Scion enables independent specification and optimization of data layouts separately from traversal algorithms, allowing systematic design space exploration across layout choices.

Equality Saturation for Quantum Circuit Optimization
Ganxiang Yang, Paige Raun, Runzhou Tao, and Ronghui Gu
(Columbia University, USA; University of Maryland, USA; CertiK, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p23-p (type: Full Paper) doi:10.1145/3808254

Equality Saturation for Quantum Circuit Optimization (Artifact) (doi:10.5281/zenodo.19571754): Artifact for PLDI '26 paper "Equality Saturation for Quantum Circuit Optimization".

Cobble: Compiling Block Encodings for Quantum Computational Linear Algebra
Charles Yuan
(University of Wisconsin-Madison, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable ACM SIGPLAN Distinguished Paper Award Article: pldi26main-p24-p (type: Full Paper) doi:10.1145/3808255

Reproduction Package for "Cobble: Compiling Block Encodings for Quantum Computational Linear Algebra" (doi:10.5281/zenodo.18898778): Source code, benchmark programs, and evaluation scripts for paper.

Bonsai: Compiling Queries to Pruned Tree Traversals
Alexander J Root, Christophe Gyurgyik, Purvi Goel, Kayvon Fatahalian, Jonathan Ragan-Kelley, Andrew Adams, and Fredrik Kjolstad
(Stanford University, USA; Massachusetts Institute of Technology, USA; Adobe Research, USA)

Publisher's Version Published Artifact Artifacts Available ACM SIGPLAN Distinguished Paper Award Article: pldi26main-p25-p (type: Full Paper) doi:10.1145/3808256

	Appendix: Scalar Symbolic Interval Analysis: Appendix for Bonsai: Compiling Queries to Pruned Tree Traversals. Background on symbolic interval analysis for scalars.
	Artifact for PLDI 2026 Paper: Bonsai: Compiling Queries into Work-Efficient Tree Traversals (doi:10.5281/zenodo.19091467): The Bonsai compiler, as well as benchmarks and either data or data generators for the evaluation performed in the paper. A Docker image is provided that installs all dependencies.

A Hierarchy of Supermartingales for ω-Regular Verification
Satoshi Kura and Hiroshi Unno
(Waseda University, Japan; Tohoku University, Japan)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p28-p (type: Full Paper) doi:10.1145/3808257

A Hierarchy of Supermartingales for ω-Regular Verification -- Artifact (doi:10.5281/zenodo.19396030): PLDI 2026 artifact

Solvable Tuple Patterns and Their Applications to Program Verification
Naoki Kobayashi, Ryosuke Sato, Ayumi Shinohara, and Ryo Yoshinaka
(University of Tokyo, Japan; Tokyo University of Agriculture and Technology, Japan; Tohoku University, Japan)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: pldi26main-p33-p (type: Full Paper) doi:10.1145/3808258

Reproduction Package for Article "Solvable Tuple Patterns and Their Applications to Program Verification" (doi:10.5281/zenodo.19907200): This artifact includes the CHC solver "CHoCoL", the scripts, and the benchmark set for reproducing the experimental results described in the paper. The artifact consists of a README file, the original benchmark results, and a Docker image built on an x86-64 machine, which includes all the tools required for the ...

Pure Borrow: Linear Haskell Meets Rust-Style Borrowing
Yusuke Matsushita and Hiromi Ishii
(Kyoto University, Japan; JIJ, Japan)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p38-p (type: Full Paper) doi:10.1145/3808259

Artifact for PLDI 2026 "Pure Borrow: Linear Haskell Meets Rust-Style Borrowing" (doi:10.5281/zenodo.19622061): The artifact for the paper "Pure Borrow: Linear Haskell Meets Rust-Style Borrowing" by Yusuke Matsushita and Hiromi Ishii, published at PLDI 2026. It includes the Haskell implementation of Pure Borrow and the benchmark suite.

The Downgrading Semantics of Memory Safety
René Rydhof Hansen, Andreas Stenbæk Larsen, and Aslan Askarov
(Aalborg University, Denmark; Aarhus University, Denmark)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p49-p (type: Full Paper) doi:10.1145/3808260

Notac interpreter and examples (doi:10.5281/zenodo.19076610): This is in the artifact for the paper "The downgrading semantics of memory safety". See included README.md

A Mechanized Algebra of Verified Data Structures for Optimizing Sparse Tensor Programs
Amanda Liu, Gilbert Louis Bernstein, Shoaib Kamil, Adam Chlipala, and Jonathan Ragan-Kelley
(Massachusetts Institute of Technology, USA; University of Washington, USA; Adobe, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p53-p (type: Full Paper) doi:10.1145/3808261

Artifact for A Mechanized Algebra of Verified Data Structures for Optimizing Sparse Tensor Programs (doi:10.5281/zenodo.19657283): This artifact contains a virtual machine with the source code implementing the framework described in the paper, as well as the code for running the evaluation and benchmarks.

Flow-Analysis-Based Closure Optimization
John Reppy, Olin Shivers, and Byron Zhong
(University of Chicago, USA; Northeastern University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p54-p (type: Full Paper) doi:10.1145/3808262

Supplemental Material for "Flow-Analysis-Based Closure Optimization': This document contains appendices to the main paper. It provides the semantics of our intermediate representation, the full closure-conversion transformation, an additional example from Section 5.3, and the complete evaluation tables.

Artifact for "Flow-analysis-based Closure Optimizations" (doi:10.5281/zenodo.19616287): The artifact includes the source code of a modified Standard ML of New Jersey compiler (version 2025.2). It contains the implementation of the analysis and the new closure conversion algorithms. It is set up to run a set of benchmark programs to compare the runtimes, the memory allocation statisitics, and the ...

Let It Flow: A Formally Verified Compilation Framework for Asynchronous Dataflow
Zhengyao Lin, Yi Cai, and Milijana Surbatovich
(Carnegie Mellon University, USA; University of Maryland at College Park, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p56-p (type: Full Paper) doi:10.1145/3808263

	Appendix: The appendix of the paper with full typing rules.
	Let It Flow: A Formally Verified Compilation Framework for Asynchronous Dataflow (doi:10.5281/zenodo.19393250): This is the artifact Docker image accompanying the paper Let It Flow: A Formally Verified Compilation Framework for Asynchronous Dataflow.

Trace-Guided Synthesis of Effectful Test Generators
Zhe Zhou, Ankush Desai, Benjamin Delaware, and Suresh Jagannathan
(Purdue University, USA; Snowflake, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p68-p (type: Full Paper) doi:10.1145/3808264

PLDI26 Artifact: Trace-Guided Synthesis of Effectful Test Generators (doi:10.5281/zenodo.19076511): This is the artifact for the PLDI 2026 paper Trace-Guided Synthesis of Effectful Test Generators. The tool is called Clouseau and is implemented in approximately 10K lines of OCaml. It automatically synthesizes effectful test generators (schedulers) for property-based testing, guided by traces that witness property ...

Contextual Refinement of Higher-Order Concurrent Probabilistic Programs
Kwing Hei Li, Alejandro Aguirre, Joseph Tassarotti, and Lars Birkedal
(Aarhus University, Denmark; New York University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p77-p (type: Full Paper) doi:10.1145/3808265

Artifact of Contextual Refinement for Higher-Order Concurrent Probabilistic Programs (doi:10.5281/zenodo.18924289): This repository contains the development of the Foxtrot logic, in the PLDI 2026 paper "Contextual Refinement of Higher-Order Concurrent Probabilistic Programs".

Cpp2Rust: Automatic Translation of C++ to Safe Rust
Lucian Popescu, Francisco Gouveia, Henrique Preto, João Silveira, Dmytro Hrybenko, José Fragoso Santos, and Nuno P. Lopes
(INESC-ID, Portugal; Instituto Superior Técnico - University of Lisbon, Portugal; Google, Germany)

Publisher's Version Article: pldi26main-p91-p (type: Full Paper) doi:10.1145/3808266

Compiling Strassen-like Matrix Multiplication Algorithms to Fast CUDA Kernels
Abhinav Jangda
(Microsoft Research, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p97-p (type: Full Paper) doi:10.1145/3808267

Artifact for "Compiling Strassen-like Matrix Multiplication Algorithms to Fast CUDA Kernels Abhinav Jangda" (doi:10.5281/zenodo.19390024): This artifact contains source code for SubCuber that generates efficient CUDA kernels for Strassen algorithm based Matrix Multiplication

Semantic Reification: A New Paradigm for Random Program Generation
Kavya Chopra, Cong Li, Thodoris Sotiropoulos, and Zhendong Su
(ETH Zurich, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p100-p (type: Full Paper) doi:10.1145/3808268

	Supplementary Material: This supplementary material provides an extended illustrative example, complete constraint-encoding rules, and additional experimental results referenced to as Sections A–C in the main paper.
	Artifact for Reify: Semantic Reification: A New Paradigm for Random Program Generation (doi:10.5281/zenodo.19880827): The research artifact made for PLDI 2026 paper: "Semantic Reification: A New Paradigm for Random Program Generation". It contains instructions and scripts to demonstrate the functionality and usage of Reify.

Contextual Embeddings: Implementing Bound Variables through Instance Resolution
Samantha Frohlich, Jessica Foster, G. A. Kavvos, and Meng Wang
(University of Bristol, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p102-p (type: Full Paper) doi:10.1145/3808269

Contextual Embeddings: Appendices: Appendices for "Contextual Embeddings: Implementing Bound Variables through Instance Resolution".

Contextual Embeddings: Implementing Bound Variables through Instance Resolution (Artifact) (doi:10.5281/zenodo.19432864): The artifact contains the Haskell code used in the paper (as well as some extra examples and benchmarking code), the Lean4 isomorphism proofs, an Agda implementation, and the R code used to generate the graphs in the paper. It also contains a bash script for running/testing all of the different components, a detailed ...

&inator: Correct, Precise C-to-Rust Interface Translation
Victor Chen, Ayden Coughlin, and Michael D. Bond
(Ohio State University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p110-p (type: Full Paper) doi:10.1145/3808270

&inator artifact (doi:10.5281/zenodo.19650358): This artifact contains Docker images that contain a build of the &inator tool, the source code for the &inator tool, and the non-scalability benchmarks used in our evaluation, as described by the paper.

Iris-WasmFX: Modular Reasoning for Wasm Stack Switching
Maxime Legoupil, Mathias Pedersen, Lars Birkedal, Sam Lindley, and Jean Pichon-Pharabod
(Nanyang Technological University, Singapore; Aarhus University, Denmark; University of Edinburgh, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p111-p (type: Full Paper) doi:10.1145/3808271

	Appendix: This pdf includes our camera-ready paper together with its appendices
	Rocq Development for Iris-WasmFX: Modular Reasoning for Wasm Stack Switching (doi:10.5281/zenodo.19095849): Rocq definitions, proofs and examples for the paper Iris-WasmFX: Modular Reasoning for Wasm Stack Switching. The readme contains information on how to build the artefact.

CoTenN: Constrained Optimization with Tensor Networks
Ritvik Sharma, Cheng Peng, Siddharth Dangwal, and Sara Achour
(Stanford University, USA; SLAC National Accelerator Laboratory, USA; University of Chicago, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p126-p (type: Full Paper) doi:10.1145/3808272

Supplementary Material: This contains the Supplementary Material for the paper "CoTenN: Constrained Optimization with Tensor Networks". It contains proofs for the projection MPOs implemented by CoTenN for various constraints. We also provide different Masq constraints for different problem encodings.

Code for CoTenN: Constrained Optimization with Tensor Networks (doi:10.5281/zenodo.19410701): This artifact provides a complete reproducible environment for the experiments presented in our paper on efficient tensor network algorithms using compressed orthogonal projections. It contains the following: Artifact Components: 1. Pre-built Docker image (cotenn_artifact.tar) with Ubuntu 22.04, Python 3.12.2, Julia ...

Verification of Recursively Defined Quantum Circuits
Mingsheng Ying and Zhicheng Zhang
(University of Technology Sydney, Australia)

Publisher's Version ACM SIGPLAN Distinguished Paper Award Article: pldi26main-p130-p (type: Full Paper) doi:10.1145/3808273

Causality and Semantic Separation
Anna Zhang, Qinglan Luo, London Bielicke, Eunice Jun, and Adam Chlipala
(Massachusetts Institute of Technology, USA; Wellesley College, USA; University of California at Los Angeles, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p135-p (type: Full Paper) doi:10.1145/3808274

Causality and Semantic Separation (doi:10.5281/zenodo.19985589): This artifact accompanies the paper Causality and Semantic Separation, accepted to PLDI 2026. The full version of the paper, including appendices, is on arXiv. It contains a mechanized formalization of causal models in the Rocq Prover, together with a proof of the paper's main result: that semantic separation is ...

Diagramming Program Values by Spatial Refinement
Siddhartha Prasad, Michael Tu, Karan Kashyap, Tim Nelson, and Shriram Krishnamurthi
(Brown University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p141-p (type: Full Paper) doi:10.1145/3808275

Artifact For: Diagramming Program Values by Spatial Refinement (doi:10.5281/zenodo.19401958): This artifact supports the claims in Diagramming Program Values by Spatial Refinement. It contains: - Language integrations: Spytial implementations for Python, Rust, and Pyret, each packaged as a Docker image with working examples and interactive visualizations. - Lean 4 mechanization: Formalization of the spatial ...

Hayroll: A Modular Wrapper for Translating C Macros and Conditional Compilation to Rust
Haoran Peng, Baris Kasikci, Gilbert Louis Bernstein, and Michael D. Ernst
(University of Washington, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p150-p (type: Full Paper) doi:10.1145/3808276

Artifact Evaluation Package for Hayroll: A Modular Wrapper for Translating C Macros and Conditional Compilation to Rust (doi:10.5281/zenodo.19674690): This artifact package is provided as a Docker image `hayroll-eval.tar.gz`. Please run the following command to load the image, and then follow `README.md` for futher instructions. ```bash sudo docker load -i hayroll-eval.tar.gz ``` The source repository is available at https://github.com/UW-HARVEST/hayroll-eval.

MatchBox: A Semantic Foundation for Data Plane Portability
Eric Hayden Campbell, Robert Zhang, Divyanshu Saxena, Aditya Akella, and Işıl Dillig
(University of Texas at Austin, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable ACM SIGPLAN Distinguished Paper Award Article: pldi26main-p153-p (type: Full Paper) doi:10.1145/3808277

	Appendix for MatchBox: A Semantic Foundation for Data Plane Portability: Supplementary proofs, definitions, and examples for MatchBox
	Software Artifact for Matchbox: A Semantic Foundation for Data Plane Portability (doi:10.5281/zenodo.19618587): This artifact contains the MatchBox implementation for specifying, type checking, and compiling match-action table translations across heterogeneous data-plane environments, together with the benchmarks and evaluation materials used in the paper’s case studies.

Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows
Zain K Aamer, Rini Banerjee, Hiroyuki Katsura, David Kaloper-Meršinjak, Dimitrios J. Economou, Kayvan Memarian, Dhruv Makwana, Neel Krishnaswami, Benjamin C. Pierce, Christopher Pulte, and Peter Sewell
(University of Pennsylvania, USA; University of Cambridge, UK; University of Oxford, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p155-p (type: Full Paper) doi:10.1145/3808278

	Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows (With Supplementary Material): Paper pdf with Supplementary Material Appendix
	Artifact: Code-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into Conventional Workflows (doi:10.5281/zenodo.19577402): This artifact (the Docker Image) contains the following components: our tools (CN, Fulminate, and Darcy), verification results for the pKVM hyp allocator, and an Android Linux with the instrumented hyp allocator.

Choose, Don’t Label: Multiple-Choice Query Synthesis for Program Disambiguation
Celeste Barnaby, Danny Ding, Osbert Bastani, and Işıl Dillig
(University of Texas at Austin, USA; University of Pennsylvania, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p161-p (type: Full Paper) doi:10.1145/3808279

Artifact for "Choose, Don't Label: Multiple-Choice Query Synthesis for Program Disambiguation" (doi:10.5281/zenodo.19052770): This artifact supports the experiments presented in our paper, Choose, Don't Label: Multiple-Choice Query Synthesis for Program Disambiguation." Our paper makes the following key contributions: - We introduce a new interactive synthesis framework in which users answer multiple-choice questions about high-level program ...

Kuiper: Correct and Efficient GPU Programming with Dependent Types and Separation Logic
Guido Martínez, Bastian Köpcke, Jonáš Fiala, Gabriel Ebner, Tahina Ramananandro, Michel Steuwer, Tyler Sorensen, and Nikhil Swamy
(Microsoft Research, USA; TU Berlin, Germany; ETH Zurich, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p173-p (type: Full Paper) doi:10.1145/3808280

Kuiper: Correct and Efficient GPU Programming with Dependent Types and Separation Logic - PLDI 2026 Artifact (doi:10.5281/zenodo.19626534): This contains the artifact for the PLDI 2026 paper "Kuiper: Correct and Efficient GPU Programming with Dependent Types and Separation Logic".

Towards Efficient Matching of Regexes with Backreferences using Register Set Automata
Vojtěch Havlena, Lukáš Holík, Ondřej Lengál, Jan Vašák, and Sabína Gulčíková
(Brno University of Technology, Czech Republic; Aalborg University, Denmark)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p181-p (type: Full Paper) doi:10.1145/3808281

Artifact for the PLDI'26 paper "Towards Efficient Matching of Regexes with Backreferences using Register Set Automata" (doi:10.5281/zenodo.19223981): This is an artifact reproducing the experimental results of the PLDI'26 paper "Towards Efficient Matching of Regexes with Backreferences using Register Set Automata." It is distributed as a virtual machine in .ova file. The experiments compare the performances of multiple regex matching tools on simulated ReDoS ...

Parameterized Algorithms and Complexity for Function Merging with Branch Reordering
Amir K. Goharshady, Kerim Kochekov, Tian Shu, and Ahmed Khaled Zaher
(University of Oxford, UK; Hong Kong University of Science and Technology, Hong Kong)

Publisher's Version Article: pldi26main-p183-p (type: Full Paper) doi:10.1145/3808282

A Compiler for Fused Relational Operations on Multisets
James Dong and Fredrik Kjolstad
(Stanford University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: pldi26main-p219-p (type: Full Paper) doi:10.1145/3808283

	Appendices: Appendices (A--F) for paper
	Artifact for A Compiler for Fused Relational Operations on Multisets (doi:10.5281/zenodo.19635976): Source code, benchmark scripts, Docker images to reproduce results in evaluation and claims in paper

SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits
Nengkun Yu, Jens Palsberg, and Thomas Reps
(Stony Brook University, USA; University of California at Los Angeles, USA; University of Wisconsin-Madison, USA)

Publisher's Version Article: pldi26main-p228-p (type: Full Paper) doi:10.1145/3808284

NEURA: A Unified and Retargetable Compilation Framework for Coarse-Grained Reconfigurable Architectures
Shangkun Li, Jinming Ge, Diyuan Tao, Zeyu Li, Jiawei Liang, Linfeng Du, Jiang Xu, Wei Zhang, and Cheng Tan
(Hong Kong University of Science and Technology, Hong Kong; Independent Researcher, China; Hong Kong University of Science and Technology, Guangzhou, China; Google, USA; Arizona State University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p234-p (type: Full Paper) doi:10.1145/3808285

NEURA: A Unified and Retargetable Compilation Framework for Coarse-Grained Reconfigurable Architectures (doi:10.5281/zenodo.18982337): Coarse-Grained Reconfigurable Architectures (CGRAs) are a promising and versatile accelerator platform, offering a balance between the performance and efficiency of specialized accelerators and the software programmability. However, their full potential is severely hindered by control flow in accelerated kernels, as ...

SSA without Dominance for Higher-Order Programs
Roland Leißa and Johannes Max Griebler
(University of Göttingen, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p239-p (type: Full Paper) doi:10.1145/3808286

SSA without Dominance for Higher-Order Programs (doi:10.5281/zenodo.19069679): The artifact consists of two parts: 1. The research compiler IR MimIR that we used to create the numbers in the Evaluation section of the paper. 2. A Lean development "lambda-graph" that verifies all lemmas and theorems in the paper.

Cerisier: A Program Logic for Attestation in a Capability Machine
June Rousseau, Denis Carnier, Thomas Van Strydonck, Steven Keuchel, Dominique Devriese, and Lars Birkedal
(Aarhus University, Denmark; KU Leuven, Belgium; Fortanix, Netherlands)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p266-p (type: Full Paper) doi:10.1145/3808287

Cerisier: A Program Logic for Attestation in a Capability Machine (Artifact) (doi:10.5281/zenodo.19062990): This is the artifact accompanying the article "Cerisier: A Program Logic for Attestation in a Capability Machine" at PLDI'26. The artifact contains the Rocq proofs accompanying the paper, built using the Iris framework. We provide - The Rocq sources themselves under cerisier.tar.gz; - A virtual machine cerisier.ova ...

Presynthesis: Towards Scaling Up Program Synthesis with Finer-Grained Abstract Semantics
Rui Dong, Qingyue Wu, Danny Ding, Zheng Guo, Ruyi Ji, and Xinyu Wang
(University of Michigan, USA; University of Texas at Austin, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p272-p (type: Full Paper) doi:10.1145/3808288

Foresighter (Presynthesis: Towards Scaling Up Program Synthesis with Finer-Grained Abstract Semantics) (doi:10.5281/zenodo.19078478): Artifact for the PLDI 2026 paper: "Presynthesis: Towards Scaling Up Program Synthesis with Finer-Grained Abstract Semantics."

Virtualizing Continuations
Cong Ma, Jonghyun Jung, and Yizhou Zhang
(University of Waterloo, Canada)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p273-p (type: Full Paper) doi:10.1145/3808289

Virtualizing Continuations (Artifact) (doi:10.5281/zenodo.19963144): This artifact accompanies the PLDI 2026 submission "Virtualized Continuation".

Modular GPU Programming with Typed Perspectives
Manya Bansal, Daniel Sainati, Joseph W. Cutler, Saman Amarasinghe, and Jonathan Ragan-Kelley
(Massachusetts Institute of Technology, USA; University of Pennsylvania, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable ACM SIGPLAN Distinguished Paper Award Article: pldi26main-p277-p (type: Full Paper) doi:10.1145/3808290

Reproduction Package for "Modular GPU Programming with Typed Perspectives" (doi:10.5281/zenodo.19079590): This artifact describes how to reproduce the quantitative GPU benchmark results presented in "Modular GPU Programming with Typed Perspective". The paper describes a language called Prism, which generates CUDA kernels from low-level specifications; this evaluation compiles and benchmarks those kernels on real hardware ...

State Space Estimation for DPOR-Based Model Checkers
A. R. Balasubramanian, Mohammad Hossein Khoshechin Jorshari, Rupak Majumdar, Umang Mathur, and Minjian Zhang
(MPI-SWS, Germany; National University of Singapore, Singapore; University of Illinois Urbana-Champaign, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p279-p (type: Full Paper) doi:10.1145/3808291

State Space Estimation for DPOR-based Model Checkers (Artifact) (doi:10.5281/zenodo.19625358): This artifact contains the implementation, benchmark data, and scripts needed to reproduce the main experimental results of the submitted version of paper State Space Estimation for DPOR-based Model Checkers.

Analyzing Bytes: Pre-Disassembly Static Binary Analysis
Huan Nguyen, Soumyakant Priyadarshan, Chencheng Jiang, and R. Sekar
(Google, USA; Stony Brook University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p284-p (type: Full Paper) doi:10.1145/3808292

Analyzing Bytes: Pre-Disassembly Static Binary Analysis (doi:10.5281/zenodo.19688632): This artifact includes source code, scripts, and detailed instructions to reproduce all the results in our paper.

SureDistrib: Verifying Almost-Sure Termination of Composite Asynchronous Byzantine Protocols
Longfei Qiu, Jingqi Xiao, Ji-Yong Shin, and Zhong Shao
(Yale University, USA; University of Hong Kong, China; Northeastern University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p304-p (type: Full Paper) doi:10.1145/3808293

Artifact For PLDI 2026 Paper #304 SureDistrib: Verifying Almost-sure Termination of Composite Asynchronous Byzantine Protocols (doi:10.5281/zenodo.19616610): This artifact contains mechanized safety and liveness proofs for an asynchronous byzantine binary agreement algorithm, which is a modified version of the binary agreement algorithm described by Mostefaoui et al. (PODC '14). The mechanization is based on the formal theory described in the paper "SureDistrib: Verifying ...

Fungible Memories for Automated Technology Mapping and Retargeting
Zachary D. Sisco, Sijie Kong, Daniel Ruelas-Petrisko, Jingtao Xia, Julian Springer, Varun Rao, Spencer Wang, Gus Henry Smith, Ben Hardekopf, and Jonathan Balkind
(Chinese University of Hong Kong, Shenzhen, China; University of California at Santa Barbara, USA; University of Washington, USA; TU Berlin, Germany; University of California at Berkeley, USA; Southmountain Research, USA)

Publisher's Version Published Artifact Artifacts Available Article: pldi26main-p315-p (type: Full Paper) doi:10.1145/3808294

Artifact for Fungible Memories for Automated Technology Mapping and Retargeting (doi:10.5281/zenodo.19090603): The artifact contains the implementation of the fungible memory compiler and decompiler, the Lean formalization of fungible memories, and all of the benchmarks to re-run the experiments.

Heterogeneous Dynamic Logic: Provability Modulo Program Theories
Samuel Teuber, Mattias Ulbrich, André Platzer, and Bernhard Beckert
(KIT, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p324-p (type: Full Paper) doi:10.1145/3808295

Artifact for "Heterogeneous Dynamic Logic: Provability Modulo Program Theories" Authors/Creators (doi:10.5281/zenodo.19551156): This artifact contains the Isabelle formalization of the paper "Heterogeneous Dynamic Logic: Provability Modulo Program Theories". We formalize dynamic theories and prove that three dynamic logics are instantiations of this concept.

SuperDP: Differential Privacy Refutation via Supermartingales
Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, and Đorđe Žikelić
(IST Austria, Austria; Singapore Management University, Singapore)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p328-p (type: Full Paper) doi:10.1145/3808296

SuperDP: Differential Privacy Refutation via Supermartingales (doi:10.5281/zenodo.19399862): This artifact provides the source code, benchmarks, and scripts necessary to build and reproduce the experimental results for `SuperDP` (Accepted at PLDI 2026). It also includes instructions for running the tool on user-provided inputs.

SIMT-Step Execution: A Flexible Operational Semantics for GPU Subgroup Behavior
Zheyuan Chen, Naomi Rehman, Guido Martínez, and Tyler Sorensen
(University of California at Santa Cruz, USA; University of California at Santa Barbara, USA; Microsoft Research, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p337-p (type: Full Paper) doi:10.1145/3808297

Reproduction package for `SIMT-Step Execution: A Flexible Operational Semantics for GPU Subgroup Behavior` (doi:10.5281/zenodo.19626183): This artifact accompanies SIMT-Step Execution: A Flexible Operational Semantics for GPU Subgroup Behavior. It packages: - an executable TLA+ model under `forward-progress/validation/` - a SPIR-V-to-TLA+ compiler under `Homunculus/` - example shaders under `example_shader_program/` - empirical Amber suites under ...

Neptune: Advanced ML Operator Fusion for Locality and Parallelism on GPUs
Yifan Zhao, Egan Johnson, Prasanth Chatarasi, Vikram Adve, and Sasa Misailovic
(University of Illinois Urbana-Champaign, USA; IBM Research, USA)

Publisher's Version Published Artifact Artifacts Available Article: pldi26main-p347-p (type: Full Paper) doi:10.1145/3808298

Artifact for "Neptune: Advanced ML Operator Fusion for Locality and Parallelism on GPUs" (doi:10.5281/zenodo.19293880): Docker image and readme instructions for the PLDI paper "Neptune: Advanced ML Operator Fusion for Locality and Parallelism on GPUs". The same code is available in the Neptune open-source repository (https://github.com/uiuc-arc/neptune).

Improving Equality Saturation for EDA via Semantic E-Graphs
Sijie Kong, Jingtao Xia, Daniel Ruelas-Petrisko, Zachary D. Sisco, Jonathan Balkind, and Gus Henry Smith
(University of California at Santa Barbara, USA; University of Washington, USA; Chinese University of Hong Kong, Shenzhen, China; Southmountain Research, USA)

Publisher's Version Published Artifact Artifacts Available Article: pldi26main-p348-p (type: Full Paper) doi:10.1145/3808299

	Appendices: Appendices for the paper "Improving Equality Saturation for EDA via Semantic E-Graphs", DOI 10.1145/3808299
	Nextmap Artifact for PLDI 2026 (doi:10.5281/zenodo.19080665): This artifact contains the `nextmap` tool and the evaluation materials used to reproduce the benchmark results. The artifact includes the implementation of `nextmap`, the evaluation workflow under `eval/`, and the benchmark suite used in the experiments. The `eval/` directory provides scripts and configurations for ...

Exploiting Sophisticated Static Analysis for Verilog
Qinlin Chen, Nairen Zhang, Jinpeng Wang, Jiacai Cui, Tian Tan, Xiaoxing Ma, Chang Xu, Jian Lu, and Yue Li
(Nanjing University, China)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p362-p (type: Full Paper) doi:10.1145/3808300

Exploiting Sophisticated Static Analysis for Verilog (Artifact) (doi:10.5281/zenodo.19486343): This artifact accompanies the paper "Exploiting Sophisticated Static Analysis for Verilog". The paper introduces Qihe, a static analysis framework for Verilog. This artifact is provided solely to reproduce the Qihe results reported in the paper. For any use of Qihe beyond artifact reproduction, please obtain its ...

Bridging Coverage and Confidence: Reliable Static False Alarm Elimination via Input-Agnosticity
Jiayi Wang, Yu Wang, Linzhang Wang, and Ke Wang
(Nanjing University, China)

Publisher's Version Published Artifact Artifacts Available Article: pldi26main-p363-p (type: Full Paper) doi:10.1145/3808301

Supplemental Material for `Bridging Coverage and Confidence: Reliable Static False Alarm Elimination via Input-Agnosticity': Supplemental material for the paper “Bridging Coverage and Confidence: Reliable Static False Alarm Elimination via Input-Agnosticity”. It contains additional technical details, proofs, experimental results, and supporting materials that complement the main paper.

Bridging Coverage and Confidence: Reliable Static False Alarm Elimination via Input-Agnosticity (doi:10.5281/zenodo.19064325): Artifact for the paper `Bridging Coverage and Confidence: Reliable Static False Alarm Elimination via Input-Agnosticity'. It contains the implementation of Rican, built on SVF/Saber, together with scripts and materials for reproducing the input-agnosticity analysis and path coverage analysis.

Optimism in Equality Saturation
Russel Arbore, Alvin Cheung, and Max Willsey
(University of California at Berkeley, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p376-p (type: Full Paper) doi:10.1145/3808302

Artifact for "Optimism in Equality Saturation" (PLDI 2026) (doi:10.5281/zenodo.19581777): This archive is a self-contained Docker image for the artifact evaluation of "Optimism in Equality Saturation". Please refer to the README.md file for directions to evaluate the artifact.

Backwards-Compatible Row-Based Exceptions in ML
Simcha van Collem, Paulo Emílio de Vilhena, and Robbert Krebbers
(Radboud University Nijmegen, Netherlands; Imperial College London, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p378-p (type: Full Paper) doi:10.1145/3808303

Rocq Formalization for `Backwards-Compatible Row-Based Exceptions in ML' (doi:10.5281/zenodo.19494181): The Rocq formalization of the paper Backwards-Compatible Row-Based Exceptions in ML.

Verifying Array Properties in Pure Data-Parallel Programs
Nikolaj Hey Hinnerskov, Robert Schenck, and Cosmin Oancea
(University of Copenhagen, Denmark; Northeastern University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p388-p (type: Full Paper) doi:10.1145/3808304

	Appendix: Appendix
	Artifact for the paper "Verifying Array Properties in Pure Data-Parallel Programs" (doi:10.5281/zenodo.19610644): The artifact includes an implementation of PropProp in the Futhark compiler, reproduces Table 1 from the paper (modulo hardware-dependent timing values) and provides the Dafny programs discussed in Section 2.

Verification Modulo Tested Library Contracts
Abhishek Uppar, Omar Muhammad, Sumanth Prabhu S, Deepak D'Souza, P. Madhusudan, and Adithya Murali
(IISc Bangalore, India; Relyance AI, India; University of Illinois Urbana-Champaign, USA; University of Wisconsin-Madison, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p396-p (type: Full Paper) doi:10.1145/3808305

	Supplement Material for Article `Verification Modulo Tested Library Contracts`: Supplementary appendices for the article `Verification Modulo Tested Library Contracts' containing detailed benchmark descriptions, full results of the mutation study, and the complete LLM prompts used for contract generation.
	Verification Modulo Tested Library Contracts (Dualis) (doi:10.5281/zenodo.19519743): This artifact contains Dualis, a verification framework implementing the Verification Modulo Tested Library Contracts (VMTLC) approach. It includes the tool's complete source code, 43 C++ benchmarks, automated fuzzer harnesses (AFL++), and the evaluation scripts necessary to reproduce the experimental results ...

Soteria: Efficient Symbolic Execution as a Functional Library: Perhaps You Should Write Your Own Symbolic Execution Engine!
Sacha-Élie Ayoun, Opale Sjöstedt, and Azalea Raad
(Imperial College London, UK; Soteria Tools, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p402-p (type: Full Paper) doi:10.1145/3808306

Artifact - Soteria: Efficient Symbolic Execution as a Functional Library (doi:10.5281/zenodo.19856235): Accompanying artifact for the PLDI'26 paper Soteria: Efficient Symbolic Execution as a Functional Library

A Categorical Basis for Robust Program Analysis
Zachary Kincaid and Shaowei Zhu
(Princeton University, USA)

Publisher's Version Article: pldi26main-p410-p (type: Full Paper) doi:10.1145/3808307

SAIL: Sound Abstract Interpreters with LLMs
Qiuhan Gu, Avaljot Singh, and Gagandeep Singh
(University of Illinois Urbana-Champaign, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p429-p (type: Full Paper) doi:10.1145/3808308

	Appendix: Additional Details and Experimental Results: This appendix provides additional technical details, extended experimental results, and supplementary figures that support the main paper (SAIL: Sound Abstract Interpreters with LLMs). These materials complement the main paper by providing deeper insights into the methodology and empirical performance of SAIL.
	Reproduction package for "SAIL: Sound Abstract Interpreters with LLMs" (doi:10.5281/zenodo.19591287): This repo is the artifact associated with the PLDI 2026 submission#429 "SAIL: Sound Abstract Interpreters with LLMs".

Intrinsically Correct Algorithms and Recursive Coalgebras
Cass Alexandru, Henning Urbat, and Thorsten Wißmann
(RPTU Kaiserslautern-Landau, Germany; Radboud University Nijmegen, Netherlands; Friedrich-Alexander University Erlangen-Nürnberg, Germany)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p434-p (type: Full Paper) doi:10.1145/3808309

	Appendices to "Intrinsically Correct Algorithms and Recursive Coalgebras": The appendices, including omitted proofs and an index of formalized results
	Agda Formalization of "Intrinsically Correct Algorithms and Recursive Coalgebras" (doi:10.5281/zenodo.19628996): A reproducible build environment in which to check the formalization accompanying the paper "Intrinsically Correct Algorithms and Recursive Coalgebras"

Revisiting Partial Tracing for Safe, Efficient, and Concurrent Garbage Collection in Unmanaged Languages
Jeonghyeon Kim, Jongse Park, Youngjin Kwon, and Jeehoon Kang
(KAIST, Republic of Korea; FuriosaAI, Republic of Korea)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p438-p (type: Full Paper) doi:10.1145/3808310

Artifact and Appendix for "Revisiting Partial Tracing for Safe, Efficient, and Concurrent Garbage Collection in Unmanaged Languages" (doi:10.5281/zenodo.19597312): This is the artifact and appendix for PLDI 2026 paper: "Revisiting Partial Tracing for Safe, Efficient, and Concurrent Garbage Collection in Unmanaged Languages". This artifact comprises the following files: * `cdpt-benchmark.zip`: This archive mainly contains a benchmark suite used to produce the results presented in ...

Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic
Philipp G. Haselwarter, Alejandro Aguirre, Simon Oddershede Gregersen, Kwing Hei Li, Joseph Tassarotti, and Lars Birkedal
(Aarhus University, Denmark; New York University, USA; AWS, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p444-p (type: Full Paper) doi:10.1145/3808311

Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Extended Version): Extended version of the paper including the Appendix.

Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic - Artifact (doi:10.5281/zenodo.19089094): This is the artifact accompanying the PLDI 2026 submission "Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic". Scope: The primary purpose of this artifact is to formalize the main results in the paper in Rocq. To aid evaluation of our results, we provide our formalization ...

Optimal Predicate Pushdown Synthesis
Robert Zhang, Eric Hayden Campbell, Dixin Tang, and Işıl Dillig
(University of Texas at Austin, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p463-p (type: Full Paper) doi:10.1145/3808312

	Supplementary Material for Optimal Predicate Pushdown Synthesis: Proofs, implementation details, and case studies.
	Software Artifact for "Optimal Predicate Pushdown Synthesis" (doi:10.5281/zenodo.19688701): This artifact contains the implementation of Pusharoo, the benchmark suite of 150 pandas and Spark pipelines, and scripts to reproduce the evaluation results in Section 6 of the article.

SparseZETA: Intelligent Auto-tuner for Designing High-Performance SpMV Programs
Zhen Du, Ying Liu, Xionghui Chen, Yanbo Zhao, Xiaobing Feng, Huimin Cui, and Jiajia Li
(Institute of Computing Technology at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; Nanjing University, China; North Carolina State University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p473-p (type: Full Paper) doi:10.1145/3808313

SparseZETA: Intelligent Auto-Tuner for Designing High-Performance SpMV Programs (doi:10.5281/zenodo.19724191): Implementation of SparseZETA and baselines for comparison.

Hybrid Path-Sums for Hybrid Quantum Programs
Christophe Chareton, Jad Issa, Mathieu Nguyen, Nicolas Blanco, and Sébastien Bardin
(CEA List - Université Paris-Saclay, France; Université de Lorraine - CNRS - Inria - LORIA, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p478-p (type: Full Paper) doi:10.1145/3808314

	Supplementary material for the article “Hybrid Path-Sums for Hybrid Quantum Programs”: This document completes the article “Hybrid Path-Sums for Hybrid Quantum Programs” with additional technical materials : proofs and typing and rewriting rules.
	HQbricks (doi:10.5281/zenodo.19080602): Reproduction package for the article "Hybrid Path-Sums for Hybrid Quantum Programs". The HQbricks library is a symbolic execution and specification verification tool for hybrid circuits (classical/quantum), it includes benchmarks to reproduce the article's results, along with a getting started guide and documentation. ...

Fixed Parameter Tractable Linearizability Monitoring
Zheng Han Lee and Umang Mathur
(National University of Singapore, Singapore)

Publisher's Version Published Artifact Artifacts Available Article: pldi26main-p482-p (type: Full Paper) doi:10.1145/3808315

Artifact for "Fixed Parameter Tractable Linearizability Monitoring" (doi:10.5281/zenodo.19472780): This artifact provides a reproducible environment for evaluating linearizability monitoring algorithms, including FPTLin (the primary tool), LinP, Limo, and Verilin. It includes implementations of linearizable and non-linearizable concurrent data structures (stacks and queues) based on Scal, along with scripts for ...

Incremental Computation for Efficient Programmable Inference in Probabilistic Programs
Fabian Zaiser, Jack Czenszak, Martin C. Rinard, Vikash K. Mansinghka, and Alexander K. Lew
(Massachusetts Institute of Technology, USA; Yale University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p491-p (type: Full Paper) doi:10.1145/3808316

	Supplementary Material (Appendices): Full version including appendices of "Incremental Computation for Efficient Programmable Inference in Probabilistic Programs" (PLDI 2026)
	Artifact for: "Incremental Computation for Efficient Programmable Inference in Probabilistic Programs" (PLDI 2026) (doi:10.5281/zenodo.19080766): This is the artifact for "Incremental Computation for Efficient Programmable Inference in Probabilistic Programs" (PLDI 2026). To get started, download the README.md file and follow the instructions.

CRIS: The Power of Imagination in Hybrid Verification
Yonghee Kim, Taeyoung Yoon, Sanghyun Yi, Jaehyung Lee, Soonwon Moon, Yeji Han, Seonho Lee, Taeyoung Rhee, Yujin Im, Donghyun Nam, Jieung Kim, and Chung-Kil Hur
(Seoul National University, Republic of Korea; Yonsei University, Republic of Korea)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p498-p (type: Full Paper) doi:10.1145/3808317

CRIS: The Power of Imagination in Hybrid Verification (Artifact) (doi:10.5281/zenodo.19491861): This artifact accompanies the paper “CRIS: The Power of Imagination in Hybrid Verification” accepted at PLDI 2026. It contains the full Rocq mechanization of the CRIS framework, including the core development, library, and example proofs, packaged as a .zip archive.

Weighted NetKAT: A Programming Language for Quantitative Network Verification
Emmanuel Suárez Acevedo, Tiago Ferreira, Kevin Batz, Oliver Bøving, Nate Foster, and Alexandra Silva
(Cornell University, USA; University College London, UK; Technical University of Denmark, Denmark; EPFL, Switzerland; Jane Street, USA)

Publisher's Version Article: pldi26main-p501-p (type: Full Paper) doi:10.1145/3808318

Implementability of Global Distributed Protocols Modulo Network Architectures
Elaine Li and Thomas Wies
(New York University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p510-p (type: Full Paper) doi:10.1145/3808319

Sprout(A): A Network-Parametric Verifier for Global Distributed Protocols (doi:10.5281/zenodo.19600644): Sprout(A) is the first network-parametric tool for deciding implementability of symbolic global protocols. Global protocols specify distributed, message-passing protocols from a birds-eye view, and are used as a specification for synthesizing local implementations. Implementability asks whether a given global protocol ...

Enumerating Ill-Typed Programs for Testing Type Analyzers
Thodoris Sotiropoulos and Zhendong Su
(ETH Zurich, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable ACM SIGPLAN Distinguished Paper Award Article: pldi26main-p517-p (type: Full Paper) doi:10.1145/3808320

	Supplementary Materials for "Enumerating Ill-Typed Programs for Testing Type Analyzers": This supplementary materials contain the proofs and the full definitions of the formalization used in the main paper.
	Reproduction Package for Article "Enumerating Ill-Typed Programs for Testing Type Analyzers" (doi:10.5281/zenodo.19033618): The research artifact made for PLDI 2026 paper: "Enumerating Ill-Typed Programs for Testing Type Analyzers". It contains instructions and scripts to demonstrate the functionality and usage of the tool that accompanies our paper.

GradInf: Gradient Estimation as Probabilistic Inference
Gaurav Arya, Mathieu Huot, Moritz Schauer, Alexander K. Lew, and Feras A. Saad
(Carnegie Mellon University, USA; Massachusetts Institute of Technology, USA; Chalmers University of Technology - University of Gothenburg, Sweden; Yale University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p518-p (type: Full Paper) doi:10.1145/3808321

Full Manuscript: Full version of the manuscript including appendices.

Artifact for "GradInf: Gradient Estimation as Probabilistic Inference" (doi:10.5281/zenodo.19673572): GradInf is an open-source Haskell library for gradient inference, a new approach to gradient estimation. It is released under the Apache-2.0 license. The methods implemented in GradInf are described in the following publication. Gaurav Arya, Mathieu Huot, Moritz Schauer, Alexander K. Lew, and Feras A. Saad. 2026. ...

Nested Inductive Types: Justified and Usable Nested Inductive Types in Lean and Rocq
Thomas Lamiaux, Yannick Forster, Matthieu Sozeau, and Nicolas Tabareau
(Nantes Université, France; Inria, France)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p530-p (type: Full Paper) doi:10.1145/3808322

	Appendices: Appendices for the paper "Nested Inductive Types: Justified and Usable Nested Inductive Types in Lean and Rocq"
	Nested Inductive Types: Justified and Usable Nested Inductive Types in Lean and Rocq (doi:10.5281/zenodo.19643714): Source code for the implementation accompanying the paper titled "Nested Inductive Types: Justified and Usable Nested Inductive Types in Lean and Rocq".

Typestate via Revocable Capabilities
Songlin Jia, Craig Liu, Siyuan He, Haotian Deng, Yuyan Bao, and Tiark Rompf
(Purdue University, USA; Augusta University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p532-p (type: Full Paper) doi:10.1145/3808323

Artifact for "Typestate via Revocable Capabilities" (doi:10.5281/zenodo.19614655): This artifact is for the paper "Typestate via Revocable Capabilities". The file scala3.tar.gz contains the implementation of our Scala 3 compiler prototype as described in Section 4.

Persistent Iterators with Value Semantics
Yihe Li and Gregory J. Duck
(National University of Singapore, Singapore)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p537-p (type: Full Paper) doi:10.1145/3808324

Artifact for the paper "Persistent Iterators with Value Semantics" - Version 2 (doi:10.5281/zenodo.19392634): The version of the artifact reviewed by PLDI 2026 AEC (with first round of reviewer comments applied), including Docker images for libfpp in linux/amd64 and linux/arm64 architectures, together with a README that details the Getting Started Guide and the Step-by-Step Instructions for artifact evaluation. It also ...

VerusBelt: A Semantic Foundation for Verus’s Proof-Oriented Extensions to the Rust Type System
Travis Hance, Laila Elbeheiry, Yusuke Matsushita, and Derek Dreyer
(MPI-SWS, Germany; Kyoto University, Japan)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable ACM SIGPLAN Distinguished Paper Award Article: pldi26main-p559-p (type: Full Paper) doi:10.1145/3808325

VerusBelt: A Semantic Foundation for Verus's Proof-Oriented Extensions to the Rust Type System (Artifact) (doi:10.5281/zenodo.19613067): This contains the Rocq development validating the contributions of _VerusBelt: A Semantic Foundation for Verus's Proof-Oriented Extensions to the Rust Type System_.

Restart and Refine: Scalable IFDS Taint Analysis across Memory Budgets
Yujiang Gui, Yonggang Tao, and Jingling Xue
(UNSW, Australia)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p561-p (type: Full Paper) doi:10.1145/3808326

Restart and Refine: Scalable IFDS Taint Analysis across Memory Budgets (Artifact) (doi:10.5281/zenodo.19642733): This artifact accompanies the paper titled "Restart and Refine: Scalable IFDS Taint Analysis across Memory Budgets." It includes a Docker image and a README file. The Docker image contains the source code, execution scripts, and scripts for generating the figures and tables reported in the paper.

Redundant Array Computation Elimination
Zixuan Wang, Liang Yuan, Xianmeng Jiang, Kun Li, Junmin Xiao, and Yunquan Zhang
(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 Reusable Article: pldi26main-p566-p (type: Full Paper) doi:10.1145/3808327

Appendix to "Redundant Array Computation Elimination": This appendix contains the full proof of Theorem 7.1 in "Redundant Array Computation Elimination".

Reproduction Package (Docker container) for Article `Redundant Array Computation Elimination` (doi:10.5281/zenodo.19563382): This record contains the artifact for the paper "Redundant Array Computation Elimination". The artifact is provided as a Docker image. The image is intended to run on an x86_64 platform and contains the software environment required for reproduction. Inside the container, the working directory contains a README.md ...

Hyper Separation Logic
Trayan Gospodinov, Peter Müller, and Thibault Dardinier
(INSAIT at Sofia University St. Kliment Ohridski, Bulgaria; ETH Zurich, Switzerland)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p595-p (type: Full Paper) doi:10.1145/3808328

Hyper Separation Logic (Artifact) (doi:10.5281/zenodo.19091148): This artifact supports the PLDI 2026 paper “Hyper Separation Logic.” It consists of an Isabelle/HOL mechanization that fully supports the formal claims made in the paper and a VirtualBox VM image with Ubuntu 24.04 that contains Isabelle 2025 and our mechanization.

The Search for Constrained Random Generators
Harrison Goldstein, Hila Peleg, Cassia Torczon, Daniel Sainati, Leonidas Lampropoulos, and Benjamin C. Pierce
(SUNY Buffalo, USA; Technion, Israel; University of Pennsylvania, USA; University of Maryland at College Park, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p622-p (type: Full Paper) doi:10.1145/3808329

	The Search for Constrained Random Generators: Appendix: Appendix.
	The Search for Constrained Random Generators (artifact) (doi:10.5281/zenodo.19073206): Docker image containing the artifact for The Search for Constrained Random Generators (PLDI'26).

An Efficient Algorithm for Streaming BPE Tokenization
Konstantinos Mamouras, Angela W. Li, and Yudi Yang
(Rice University, USA)

Publisher's Version Artifacts Functional Article: pldi26main-p647-p (type: Full Paper) doi:10.1145/3808330

Uniformity Analysis in the WebGPU Shading Language
James Lee-Jones, John Wickerson, and Alastair F. Donaldson
(Imperial College London, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p659-p (type: Full Paper) doi:10.1145/3808331

Artifact for "Uniformity Analysis in the WebGPU Shading Language", PLDI 2026 (doi:10.5281/zenodo.19556935): The artifact contains the Alloy model described in the paper, the tools and scripts necessary for recreating the experiment in Section 6 the paper, as well as the experimental data produced during this experimental run. The artifact also includes a number of additional tools to support the conducting of the experiment ...

Expecto: Extracting Formal Specifications from Natural Language Description for Trustworthy Oracles
Dongjae Lee and Kihong Heo
(KAIST, Republic of Korea)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p660-p (type: Full Paper) doi:10.1145/3808332

Expecto: Extracting Formal Specifications from Natural Language Description for Trustworthy Oracles (doi:10.5281/zenodo.19450217): This artifact is the reproducibility package for the paper "Expecto: Extracting Formal Specifications from Natural Language Description for Trustworthy Oracles,". It includes the core Expecto implementation, the NL2Postcond baseline, benchmark datasets for APPS, HumanEval+, and Defects4J, experiment scripts, and ...

Synthesizing Backward Error Bounds, Backward
Laura Zielinski and Justin Hsu
(Cornell University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable ACM SIGPLAN Distinguished Paper Award Article: pldi26main-p665-p (type: Full Paper) doi:10.1145/3808333

	'Synthesizing Backward Error Bounds, Backward' Appendices: Appendices of paper
	eggshel: A Floating-Point Backward Error Analysis Tool (doi:10.5281/zenodo.19391349): A tool for statically bounding the backward error of floating-point programs.

Responsive Parallelism with Dynamic and First-Class Priorities
Marelle León, My Dinh, and Stefan K. Muller
(Illinois Institute of Technology, USA; University of Connecticut, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p701-p (type: Full Paper) doi:10.1145/3808334

	Appendix for "Responsive Parallelism with Dynamic and First-Class Priorities": Appendix containing full figures, proofs, and additional text.
	Artifact for "Responsive Parallelism with Dynamic and First-class Priorities" (doi:10.5281/zenodo.19074795): This artifact consists of the source code for the PriML compiler, extended with implementations of the paper's theory of dynamic and first-class priorities. The artifact also includes the benchmarks described in the paper and experiment scripts for running the compiler on them.

Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for Reachability Types
Songlin Jia, Guannan Wei, Siyuan He, Yuyan Bao, and Tiark Rompf
(Purdue University, USA; Tufts University, USA; Augusta University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p703-p (type: Full Paper) doi:10.1145/3808335

Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for Reachability Types (Artifact) (doi:10.5281/zenodo.19340767): This artifact requires Lean for proofs and examples, and Python 3 for figures.

Syntactic Implicit Parameters with Static Overloading
Daan Leijen and Tim Whiting
(Microsoft Research, USA; Brigham Young University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p717-p (type: Full Paper) doi:10.1145/3808336

Syntactic Implicits with Static Overloading (doi:10.5281/zenodo.19057777): Contains a docker image with the full implementation of syntactic implicits with static overloading in Koka.

A Verified Parallel Scheduler for OCaml 5
Clément Allain and Gabriel Scherer
(Inria, France; Université Paris Cité, France)

Publisher's Version Published Artifact Artifacts Available Article: pldi26main-p742-p (type: Full Paper) doi:10.1145/3808337

Artifact for "A verified parallel scheduler for OCaml 5" (doi:10.5281/zenodo.19128679): The artifact is located at https://zenodo.org/records/19128679/files/pldi26-artifact.zip

Neuro-symbolic Hierarchical Learning for Long-Horizon Robotic Tasks
Yu Huang, Ziji Wu, Zhengyi Ma, Kexin Ma, and Ji Wang
(National University of Defense Technology, China)

Publisher's Version Published Artifact Artifacts Available Article: pldi26main-p772-p (type: Full Paper) doi:10.1145/3808338

Artifact for #772<Neuro-Symbolic Hierarchical Learning for Long-Horizon Robotic Tasks> (doi:10.5281/zenodo.19652694): v1.0: Implementation code and readme.md v2.0: updated prebuilt conda environment, added GUIDE.md, and other scripts v3.0: updated with appendix and experimental gifs. v4.0: updated with prebuilt image and GUIDE2.md. v5.0: updated with repaired files

SuperCollider: Scalable and Effective Data Race Detection for CUDA
Mark Stephenson, Sana Damani, Mohamed Tarek Ibn Ziad, Anis Ladram, and Michael Garland
(NVIDIA, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Functional Article: pldi26main-p774-p (type: Full Paper) doi:10.1145/3808339

	Appendix: An appendix that includes a proof of soundness of the SuperCollider technique.
	Reproduction Package for PLDI 2026 Article 'SuperCollider: Scalable and Effective Data Race Detection for CUDA' (doi:10.5281/zenodo.19058944): This artifact accompanies the PLDI 2026 paper "SuperCollider: Scalable and Effective Data Race Detection for CUDA."

Pantomime: Constructive Leakage Proofs via Simulation
Robin Webbers, Robert Schenck, Wind Wong, Kristina Sojakova, and Klaus von Gleissenthall
(Vrije Universiteit Amsterdam, Netherlands; Northeastern University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p785-p (type: Full Paper) doi:10.1145/3808340

Appendix of the paper "Pantomime: Constructive Leakage Proofs via Simulation": The appendix for the paper "Pantomime: Constructive Leakage Proofs via Simulation". Contains more detailed proofs, figures, code and data that were left out the main text in the interest of space.

Artifact for the paper "Pantomime: Constructive Leakage Proofs via Simulation" (doi:10.5281/zenodo.19080639): This artifact reproduces Table 1 from Section 6 of the paper. We verify the standard and secure versions of AIMCore using Pantomime and report on the verification time. We also reproduce verification results from Table 1 of the LeaVe paper to compare against---see the paper for a discussion. The artifact is composed ...

Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy
Eden Frenkel, Kenneth L. McMillan, Oded Padon, and Sharon Shoham
(Tel Aviv University, Israel; University of Texas at Austin, USA; Weizmann Institute of Science, Israel)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p807-p (type: Full Paper) doi:10.1145/3808341

Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy (Artifact) (doi:10.5281/zenodo.19071811): This artifact accompanies the paper "Simplifying Safety Proofs with Forward-Backward Reasoning and Prophecy". The artifact contains a mechanized implementation of the forward-backward incremental induction (FBII) proof system described in the paper, built on top of the mypyvy tool. It includes the proof files for all ...

Scalable Floating-Point Satisfiability via Staged Optimization
Yuanzhuo Zhang, Zhoulai Fu, and Binoy Ravindran
(Virginia Tech, USA; SUNY Korea, Republic of Korea; Stony Brook University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p828-p (type: Full Paper) doi:10.1145/3808342

Artifact for [Scalable Floating-Point Satisfiability via Staged Optimization] (doi:10.5281/zenodo.19573062): Software artifact for the paper "[Scalable Floating-Point Satisfiability via Staged Optimization]," including all benchmarks and scripts for reproducibility and reusability.

Categorical Semantics of Probabilistic Symbolic Execution
John M. Li, Jack Czenszak, and Steven Holtzen
(Northeastern University, USA; Yale University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable ACM SIGPLAN Distinguished Paper Award Article: pldi26main-p831-p (type: Full Paper) doi:10.1145/3808343

Artifact for "Categorical Semantics of Probabilistic Symbolic Execution" (doi:10.5281/zenodo.19485098): Haskell implementation of the symbolic executor described in the paper.

Navigating AND–OR Graph Modifications to Debug Failing Proof Search
Justin Lubin, Marlena Preigh, Max Willsey, and Sarah E. Chasins
(University of California at Berkeley, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p879-p (type: Full Paper) doi:10.1145/3808344

	Appendices: Appendices for "Navigating AND–OR Graph Modifications to Debug Failing Proof Search"
	Reproduction Package for Article "Navigating AND–OR Graph Modifications to Debug Failing Proof Search" (doi:10.5281/zenodo.19665844): A self-contained Docker image for the artifact evaluation of PLDI 2026 paper "Navigating AND–OR Graph Modifications to Debug Failing Proof Search"

Compiling to Recurrent Neurons
Joey Velez-Ginorio, Nada Amin, Konrad Kording, and Steve Zdancewic
(University of Pennsylvania, USA; Harvard University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p881-p (type: Full Paper) doi:10.1145/3808345

	Appendix: Appendix to "Compiling to Recurrent Neurons"
	Compiling to recurrent neurons (doi:10.5281/zenodo.18963154): Demos the main results of paper.

Evolving Abstract Transformers for Gradient-Guided, Adaptable Abstract Interpretation
Shaurya Gomber, Debangshu Banerjee, and Gagandeep Singh
(University of Illinois Urbana-Champaign, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p887-p (type: Full Paper) doi:10.1145/3808346

	Appendix: Appendix of the paper.
	Artifact for "Evolving Abstract Transformers for Gradient-Guided, Adaptable Abstract Interpretation" (doi:10.5281/zenodo.19586617): The artifact contains the entire source code (with benchmark data), pre-built docker image with all dependencies setup already for easy reproduction of results and a README file with all the instructions.

TreeCoder: Systematic Exploration and Optimisation of Decoding and Constraints for LLM Code Generation
Henrijs Princis, Arindam Sharma, and Cristina David
(University of Bristol, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p906-p (type: Full Paper) doi:10.1145/3808347

	Appendix: This is the appendix for the paper TreeCoder: Systematic Exploration and Optimisation of Decoding and Constraints for LLM Code Generation
	TreeCoder (doi:10.5281/zenodo.19440194): Code for TreeCoder: Graph-based decoding framework for constrained code generation with multiple decoding strategies (beam search, simple sampling, sequential Monte Carlo, Monte Carlo Tree Search) and ASAp (Approximate Sampling with Anticipated future grammaticality).

Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification
Satoshi Kura, Hiroshi Unno, and Takeshi Tsukada
(Waseda University, Japan; Tohoku University, Japan; Chiba University, Japan)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p950-p (type: Full Paper) doi:10.1145/3808348

Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification -- Artifact (doi:10.5281/zenodo.19690009): PLDI 2026 Artifact

EREQ: Regular Expressions with Quantifiers and Incremental Quantifier Elimination
Ekaterina Zhuchko, Ian Erik Varatalu, Margus Veanes, and Nikolaj Bjørner
(Tallinn University of Technology, Estonia; Microsoft Research, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p993-p (type: Full Paper) doi:10.1145/3808349

EREQ: Regular Expressions with Quantifiers and Incremental Quantifier Elimination (PLDI26 Version) (doi:10.5281/zenodo.19915486): Includes: The tool and benchmarks: https://doi.org/10.5281/zenodo.19072417 The Lean formalisation: https://doi.org/10.5281/zenodo.19067931

A Formally Verified Foundation for Compositional Heterogeneous Coherence
An Qi Zhang, Andrés Goens, Daniel Sorin, and Vijay Nagarajan
(University of Utah, USA; TU Darmstadt, Germany; Duke University, USA)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p1012-p (type: Full Paper) doi:10.1145/3808350

A Formally Verified Foundation for Compositional Heterogeneous Coherence (doi:10.5281/zenodo.19087136): Artifact for evaluation of "A Formally Verified Foundation for Compositional Heterogeneous Coherence". It contains -- a README.md with instructions on using the docker image to evaluate the artifact -- an Artifact-Instructions.pdf with instructions on running and evaluating the artifact

Abstract Interpretation with Confidence: Quantifying the Precision of Dataflow Analysis with Probabilities
Yuanfeng Shi, Ziyue Jin, and Xin Zhang
(Peking University, China)

Publisher's Version Article: pldi26main-p1066-p (type: Full Paper) doi:10.1145/3808351

Appendix of Abstract Interpretation with Confidence: It's the appendix of the paper: Abstract Interpretation with Confidence

Dynamically Checked Deep Immutability in Python
Fridtjof Stoldt, Sylvan Clebsch, Matthew A. Johnson, Matthew J. Parkinson, and Tobias Wrigstad
(Uppsala University, Sweden; Microsoft Azure Research, USA; Microsoft Azure Research, UK)

Publisher's Version Published Artifact Artifacts Available Artifacts Reusable Article: pldi26main-p1129-p (type: Full Paper) doi:10.1145/3808352

Artifact: Dynamically Checked Deep Immutability in Python (doi:10.5281/zenodo.19486173): This artifact holds a snapshot of CPython and a patched CPython version with the modifications described in the paper. Differences between the paper and the implementation are documented in DIFFERENCES.md The GUIDE.md file contains links to examples, benchmarks and implementation details that are part of this ...

Corrigendum: Falcon: A Scalable Analytical Cache Model
Arjun Pitchanathan, Kunwar Grover, and Tobias Grosser
(University of Edinburgh, UK; Advanced Micro Devices, UK; University of Cambridge, UK)

Publisher's Version Article: pldi24main-p644-p-CR (type: Corrigendum) doi:10.1145/3820287