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

Title Page

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

Editorial Message

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

PLDI 2024 Sponsors and Supporters

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

Input-Relational Verification of Deep Neural Networks
Debangshu Banerjee, Changming Xu, and Gagandeep Singh
(University of Illinois at Urbana-Champaign, USA; VMware Research, USA)

Publisher's Version Artifacts Reusable Article: pldi24main-p2-p (type: Full Paper) doi:10.1145/3656377

Modular Hardware Design of Pipelined Circuits with Hazards
Minseong Jang, Jungin Rhee, Woojin Lee, Shuangshuang Zhao, and Jeehoon Kang
(KAIST, South Korea)

Publisher's Version Artifacts Reusable Article: pldi24main-p12-p (type: Full Paper) doi:10.1145/3656378

Verified Extraction from Coq to OCaml
Yannick Forster, Matthieu Sozeau, and Nicolas Tabareau
(Inria, France)

Publisher's Version Article: pldi24main-p22-p (type: Full Paper) doi:10.1145/3656379

Robust Resource Bounds with Static Analysis and Bayesian Inference
Long Pham, Feras A. Saad, and Jan Hoffmann
(Carnegie Mellon University, USA)

Publisher's Version Archive submitted (4.3 MB) Artifacts Reusable Article: pldi24main-p24-p (type: Full Paper) doi:10.1145/3656380

Recursive Program Synthesis using Paramorphisms
Qiantan Hong and Alex Aiken
(Stanford University, USA)

Publisher's Version Article: pldi24main-p29-p (type: Full Paper) doi:10.1145/3656381

A Tensor Compiler with Automatic Data Packing for Simple and Efficient Fully Homomorphic Encryption
Aleksandar Krastev, Nikola Samardzic, Simon Langowski, Srinivas Devadas, and Daniel Sanchez
(Massachusetts Institute of Technology, USA)

Publisher's Version Article: pldi24main-p33-p (type: Full Paper) doi:10.1145/3656382

Concurrent Immediate Reference Counting
Jaehwang Jung, Jeonghyeon Kim, Matthew J. Parkinson, and Jeehoon Kang
(KAIST, South Korea; Microsoft Azure, United Kingdom)

Publisher's Version Artifacts Reusable Article: pldi24main-p34-p (type: Full Paper) doi:10.1145/3656383

A Proof Recipe for Linearizability in Relaxed Memory Separation Logic
Sunho Park, Jaewoo Kim, Ike Mulder, Jaehwang Jung, Janggun Lee, Robbert Krebbers, and Jeehoon Kang
(KAIST, South Korea; Radboud University Nijmegen, Netherlands)

Publisher's Version Artifacts Reusable Article: pldi24main-p36-p (type: Full Paper) doi:10.1145/3656384

Diffy: Data-Driven Bug Finding for Configurations
Siva Kesava Reddy Kakarla, Francis Y. Yan, and Ryan Beckett
(Microsoft Research, USA)

Publisher's Version Archive submitted (850 kB) Article: pldi24main-p42-p (type: Full Paper) doi:10.1145/3656385

Boosting Compiler Testing by Injecting Real-World Code
Shaohua Li, Theodoros Theodoridis, and Zhendong Su
(ETH Zurich, Switzerland)

Publisher's Version Artifacts Reusable Article: pldi24main-p45-p (type: Full Paper) doi:10.1145/3656386

SMT Theory Arbitrage: Approximating Unbounded Constraints using Bounded Theories
Benjamin Mikek and Qirun Zhang
(Georgia Institute of Technology, USA)

Publisher's Version Artifacts Reusable Article: pldi24main-p49-p (type: Full Paper) doi:10.1145/3656387

Compilation of Qubit Circuits to Optimized Qutrit Circuits
Ritvik Sharma and Sara Achour
(Stanford University, USA)

Publisher's Version Archive submitted (260 kB) Artifacts Reusable Article: pldi24main-p50-p (type: Full Paper) doi:10.1145/3656388

Optimistic Stack Allocation and Dynamic Heapification for Managed Runtimes
Aditya Anand, Solai Adithya, Swapnil Rustagi, Priyam Seth, Vijay Sundaresan, Daryl Maier, V. Krishna Nandivada, and Manas Thakur
(IIT Bombay, India; IIT Mandi, India; IBM, Canada; IIT Madras, India)

Publisher's Version Artifacts Functional Article: pldi24main-p53-p (type: Full Paper) doi:10.1145/3656389

A Verified Compiler for a Functional Tensor Language
Amanda Liu, Gilbert Bernstein, Adam Chlipala, and Jonathan Ragan-Kelley
(Massachusetts Institute of Technology, USA; University of Washington, USA)

Publisher's Version Archive submitted (330 kB) Artifacts Reusable Article: pldi24main-p55-p (type: Full Paper) doi:10.1145/3656390

IsoPredict: Dynamic Predictive Analysis for Detecting Unserializable Behaviors in Weakly Isolated Data Store Applications
Chujun Geng, Spyros Blanas, Michael D. Bond, and Yang Wang
(Ohio State University, USA)

Publisher's Version Artifacts Reusable Article: pldi24main-p59-p (type: Full Paper) doi:10.1145/3656391

Compiling with Abstract Interpretation
Dorian Lesbre and Matthieu Lemerre
(Université Paris-Saclay - CEA LIST, France)

Publisher's Version Artifacts Reusable Article: pldi24main-p70-p (type: Full Paper) doi:10.1145/3656392

Associated Effects: Flexible Abstractions for Effectful Programming
Matthew Lutze and Magnus Madsen
(Aarhus University, Denmark)

Publisher's Version Artifacts Reusable Article: pldi24main-p75-p (type: Full Paper) doi:10.1145/3656393

Efficient Static Vulnerability Analysis for JavaScript with Multiversion Dependency Graphs
Mafalda Ferreira, Miguel Monteiro, Tiago Brito, Miguel E. Coimbra, Nuno Santos, Limin Jia, and José Fragoso Santos
(INESC-ID, Portugal; Universidade de Lisboa, Portugal; Carnegie Mellon University, USA)

Publisher's Version Artifacts Reusable Article: pldi24main-p79-p (type: Full Paper) doi:10.1145/3656394

Floating-Point TVPI Abstract Domain
Joao Rivera, Franz Franchetti, and Markus Püschel
(ETH Zurich, Switzerland; Carnegie Mellon University, USA)

Publisher's Version Archive submitted (490 kB) Artifacts Reusable Article: pldi24main-p97-p (type: Full Paper) doi:10.1145/3656395

NetBlocks: Staging Layouts for High-Performance Custom Host Network Stacks
Ajay Brahmakshatriya, Chris Rinard, Manya Ghobadi, and Saman Amarasinghe
(Massachusetts Institute of Technology, USA)

Publisher's Version Artifacts Reusable Article: pldi24main-p99-p (type: Full Paper) doi:10.1145/3656396

The T-Complexity Costs of Error Correction for Control Flow in Quantum Computation
Charles Yuan and Michael Carbin
(Massachusetts Institute of Technology, USA)

Publisher's Version Archive submitted (520 kB) Artifacts Reusable Article: pldi24main-p115-p (type: Full Paper) doi:10.1145/3656397

The Functional Essence of Imperative Binary Search Trees
Anton Lorenzen, Daan Leijen, Wouter Swierstra, and Sam Lindley
(University of Edinburgh, United Kingdom; Microsoft Research, Redmond, USA; Utrecht University, Netherlands)

Publisher's Version Artifacts Reusable Article: pldi24main-p116-p (type: Full Paper) doi:10.1145/3656398

Compositional Semantics for Shared-Variable Concurrency
Mikhail Svyatlovskiy, Shai Mermelstein, and Ori Lahav
(Tel Aviv University, Israel)

Publisher's Version Artifacts Reusable Article: pldi24main-p120-p (type: Full Paper) doi:10.1145/3656399

Falcon: A Fused Approach to Path-Sensitive Sparse Data Dependence Analysis
Peisen Yao, Jinguo Zhou, Xiao Xiao, Qingkai Shi, Rongxin Wu, and Charles Zhang
(Zhejiang University, China; Ant Group, China; Nanjing University, China; Xiamen University, China; Hong Kong University of Science and Technology, China)

Publisher's Version Article: pldi24main-p125-p (type: Full Paper) doi:10.1145/3656400

Allo: A Programming Model for Composable Accelerator Design
Hongzheng Chen, Niansong Zhang, Shaojie Xiang, Zhichen Zeng, Mengjia Dai, and Zhiru Zhang
(Cornell University, USA; University of Science and Technology of China, China)

Publisher's Version Archive submitted (870 kB) Artifacts Reusable Article: pldi24main-p130-p (type: Full Paper) doi:10.1145/3656401

VESTA: Power Modeling with Language Runtime Events
Joseph Raskind, Timur Babakol, Khaled Mahmoud, and Yu David Liu
(SUNY Binghamton, USA)

Publisher's Version Artifacts Reusable Article: pldi24main-p138-p (type: Full Paper) doi:10.1145/3656402

Mechanised Hypersafety Proofs about Structured Data
Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman Amarasinghe, and Ilya Sergey
(National University of Singapore, Singapore; Massachusetts Institute of Technology, USA)

Publisher's Version Artifacts Reusable Article: pldi24main-p146-p (type: Full Paper) doi:10.1145/3656403

Refined Input, Degraded Output: The Counterintuitive World of Compiler Behavior
Theodoros Theodoridis and Zhendong Su
(ETH Zurich, Switzerland)

Publisher's Version Artifacts Reusable Article: pldi24main-p148-p (type: Full Paper) doi:10.1145/3656404

Jacdac: Service-Based Prototyping of Embedded Systems
Thomas Ball, Peli de Halleux, James Devine, Steve Hodges, and Michał Moskal
(Microsoft, USA; Microsoft, United Kingdom; Lancaster University, United Kingdom)

Publisher's Version Artifacts Reusable Article: pldi24main-p153-p (type: Full Paper) doi:10.1145/3656405

Don’t Write, but Return: Replacing Output Parameters with Algebraic Data Types in C-to-Rust Translation
Jaemin Hong and Sukyoung Ryu
(KAIST, South Korea)

Publisher's Version Artifacts Reusable Article: pldi24main-p169-p (type: Full Paper) doi:10.1145/3656406

Quantitative Robustness for Vulnerability Assessment
Guillaume Girol, Guilhem Lacombe, and Sébastien Bardin
(CEA LIST, France; Université Paris-Saclay, France)

Publisher's Version Archive submitted (540 kB) Artifacts Reusable Article: pldi24main-p171-p (type: Full Paper) doi:10.1145/3656407

Automated Verification of Fundamental Algebraic Laws
George Zakhour, Pascal Weisenburger, and Guido Salvaneschi
(University of St. Gallen, Switzerland)

Publisher's Version Artifacts Reusable Article: pldi24main-p174-p (type: Full Paper) doi:10.1145/3656408

GenSQL: A Probabilistic Programming System for Querying Generative Models of Database Tables
Mathieu Huot, Matin Ghavami, Alexander K. Lew, Ulrich Schaechtle, Cameron E. Freer, Zane Shelby, Martin C. Rinard, Feras A. Saad, and Vikash K. Mansinghka
(Massachusetts Institute of Technology, USA; Digital Garage, Japan; Carnegie Mellon University, USA)

Publisher's Version Artifacts Reusable Article: pldi24main-p182-p (type: Full Paper) doi:10.1145/3656409

Daedalus: Safer Document Parsing
Iavor S. Diatchki, Mike Dodds, Harrison Goldstein, Bill Harris, David A. Holland, Benoit Razet, Cole Schlesinger, and Simon Winwood
(Galois, USA; University of Pennsylvania, USA)

Publisher's Version Artifacts Reusable Article: pldi24main-p185-p (type: Full Paper) doi:10.1145/3656410

Descend: A Safe GPU Systems Programming Language
Bastian Köpcke, Sergei Gorlatch, and Michel Steuwer
(University of Münster, Germany; TU Berlin, Germany)

Publisher's Version Article: pldi24main-p187-p (type: Full Paper) doi:10.1145/3656411

Bit Blasting Probabilistic Programs
Poorva Garg, Steven Holtzen, Guy Van den Broeck, and Todd Millstein
(University of California at Los Angeles, Los Angeles, USA; Northeastern University, USA)

Publisher's Version Artifacts Functional Article: pldi24main-p188-p (type: Full Paper) doi:10.1145/3656412

Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq
Simon Spies, Lennard Gäher, Michael Sammler, and Derek Dreyer
(MPI-SWS, Germany)

Publisher's Version Artifacts Reusable Article: pldi24main-p189-p (type: Full Paper) doi:10.1145/3656413

Program Analysis for Adaptive Data Analysis
Jiawen Liu, Weihao Qu, Marco Gaboardi, Deepak Garg, and Jonathan Ullman
(Boston University, USA; Monmouth University, USA; MPI-SWS, Germany; Northeastern University, USA)

Publisher's Version Artifacts Reusable Article: pldi24main-p195-p (type: Full Paper) doi:10.1145/3656414

Superfusion: Eliminating Intermediate Data Structures via Inductive Synthesis
Ruyi Ji, Yuwei Zhao, Nadia Polikarpova, Yingfei Xiong, and Zhenjiang Hu
(Peking University, China; University of California at San Diego, USA)

Publisher's Version Artifacts Reusable Article: pldi24main-p213-p (type: Full Paper) doi:10.1145/3656415

Consolidating Smart Contracts with Behavioral Contracts
Guannan Wei, Danning Xie, Wuqi Zhang, Yongwei Yuan, and Zhuo Zhang
(Purdue University, USA; Hong Kong University of Science and Technology, China)

Publisher's Version Article: pldi24main-p218-p (type: Full Paper) doi:10.1145/3656416

Scaling Type-Based Points-to Analysis with Saturation
Christian Wimmer, Codrut Stancu, David Kozak, and Thomas Würthinger
(Oracle Labs, USA; Oracle Labs, Switzerland; Brno University of Technology, Czechia; Oracle Labs, Czechia)

Publisher's Version Artifacts Reusable Article: pldi24main-p251-p (type: Full Paper) doi:10.1145/3656417

From Batch to Stream: Automatic Generation of Online Algorithms
Ziteng Wang, Shankara Pailoor, Aaryan Prakash, Yuepeng Wang, and Işıl Dillig
(University of Texas at Austin, USA; Simon Fraser University, Canada)

Publisher's Version Artifacts Reusable Article: pldi24main-p263-p (type: Full Paper) doi:10.1145/3656418

Symbolic Execution for Quantum Error Correction Programs
Wang Fang and Mingsheng Ying
(Institute of Software at Chinese Academy of Sciences, Beijing, China; University of Chinese Academy of Sciences, China; Tsinghua University, China)

Publisher's Version Artifacts Reusable Article: pldi24main-p276-p (type: Full Paper) doi:10.1145/3656419

Wavefront Threading Enables Effective High-Level Synthesis
Blake Pelton, Adam Sapek, Ken Eguro, Daniel Lo, Alessandro Forin, Matt Humphrey, Jinwen Xi, David Cox, Rajas Karandikar, Johannes de Fine Licht, Evgeny Babin, Adrian Caulfield, and Doug Burger
(Microsoft, USA; ETH Zurich, Switzerland)

Publisher's Version Article: pldi24main-p282-p (type: Full Paper) doi:10.1145/3656420

Decidable Subtyping of Existential Types for Julia
Julia Belyakova, Benjamin Chung, Ross Tate, and Jan Vitek
(Purdue University, USA; JuliaHub, USA; Independent Consultant, USA; Northeastern University, USA; Charles University, Czechia)

Publisher's Version Archive submitted (1.7 MB) Article: pldi24main-p283-p (type: Full Paper) doi:10.1145/3656421

RefinedRust: A Type System for High-Assurance Verification of Rust Programs
Lennard Gäher, Michael Sammler, Ralf Jung, Robbert Krebbers, and Derek Dreyer
(MPI-SWS, Germany; ETH Zurich, Switzerland; Radboud University Nijmegen, Netherlands)

Publisher's Version Artifacts Reusable Article: pldi24main-p289-p (type: Full Paper) doi:10.1145/3656422

LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs
Longfei Qiu, Yoonseung Kim, Ji-Yong Shin, Jieung Kim, Wolf Honoré, and Zhong Shao
(Yale University, USA; Northeastern University, USA; Inha University, South Korea)

Publisher's Version Artifacts Reusable Article: pldi24main-p290-p (type: Full Paper) doi:10.1145/3656423

Reducing Static Analysis Unsoundness with Approximate Interpretation
Mathias Rud Laursen, Wenyuan Xu, and Anders Møller
(Aarhus University, Denmark)

Publisher's Version Artifacts Reusable Article: pldi24main-p295-p (type: Full Paper) doi:10.1145/3656424

Verification under Intel-x86 with Persistency
Parosh Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan
(Uppsala University, Sweden; Université Paris Cité, France; Chennai Mathematical Institute, India; Institute of Mathematical Sciences, India)

Publisher's Version Article: pldi24main-p298-p (type: Full Paper) doi:10.1145/3656425

Compilation of Modular and General Sparse Workspaces
Genghan Zhang, Olivia Hsu, and Fredrik Kjolstad
(Stanford University, USA)

Publisher's Version Article: pldi24main-p300-p (type: Full Paper) doi:10.1145/3656426

Maximum Consensus Floating Point Solutions for Infeasible Low-Dimensional Linear Programs with Convex Hull as the Intermediate Representation
Mridul Aanjaneya and Santosh Nagarakatte
(Rutgers University, USA)

Publisher's Version Article: pldi24main-p309-p (type: Full Paper) doi:10.1145/3656427

Qubit Recycling Revisited
Hanru Jiang
(Beijing Institute of Mathematical Sciences and Applications, China)

Publisher's Version Artifacts Reusable Article: pldi24main-p350-p (type: Full Paper) doi:10.1145/3656428

A Lightweight Polyglot Code Transformation Language
Ameya Ketkar, Daniel Ramos, Lazaro Clapp, Raj Barik, and Murali Krishna Ramanathan
(Gitar, USA; Carnegie Mellon University, USA; INESC-ID, Portugal; Universidade de Lisboa, Portugal; Amazon Web Services, USA)

Publisher's Version Artifacts Functional Article: pldi24main-p359-p (type: Full Paper) doi:10.1145/3656429

An Algebraic Language for Specifying Quantum Networks
Anita Buckley, Pavel Chuprikov, Rodrigo Otoni, Robert Soulé, Robert Rand, and Patrick Eugster
(USI Lugano, Switzerland; Yale University, USA; University of Chicago, USA)

Publisher's Version Artifacts Reusable Article: pldi24main-p381-p (type: Full Paper) doi:10.1145/3656430

Linear Matching of JavaScript Regular Expressions
Aurèle Barrière and Clément Pit-Claudel
(EPFL, Switzerland)

Publisher's Version Archive submitted (350 kB) Artifacts Reusable Article: pldi24main-p400-p (type: Full Paper) doi:10.1145/3656431

Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving
Peixin Wang, Tengshun Yang, Hongfei Fu, Guanyan Li, and C.-H. Luke Ong
(Nanyang Technological University, Singapore; Institute of Software at Chinese Academy of Sciences, Beijing, China; University of Chinese Academy of Sciences, China; Shanghai Jiao Tong University, China; University of Oxford, United Kingdom)

Publisher's Version Artifacts Reusable Article: pldi24main-p403-p (type: Full Paper) doi:10.1145/3656432

A HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite Automata
Zhe Zhou, Qianchuan Ye, Benjamin Delaware, and Suresh Jagannathan
(Purdue University, USA)

Publisher's Version Artifacts Reusable Article: pldi24main-p404-p (type: Full Paper) doi:10.1145/3656433

Stream Types
Joseph W. Cutler, Christopher Watson, Emeka Nkurumeh, Phillip Hilliard, Harrison Goldstein, Caleb Stanford, and Benjamin C. Pierce
(University of Pennsylvania, USA; California Institute of Technology, USA; University of California at Davis, Davis, USA)

Publisher's Version Article: pldi24main-p407-p (type: Full Paper) doi:10.1145/3656434

SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT Techniques
Elvira Albert, Maria Garcia de la Banda, Alejandro Hernández-Cerezo, Alexey Ignatiev, Albert Rubio, and Peter J. Stuckey
(Complutense University of Madrid, Spain; Monash University, Australia)

Publisher's Version Artifacts Reusable Article: pldi24main-p416-p (type: Full Paper) doi:10.1145/3656435

Compiling Conditional Quantum Gates without Using Helper Qubits
Keli Huang and Jens Palsberg
(University of California at Los Angeles, Los Angeles, USA)

Publisher's Version Archive submitted (1.5 MB) Article: pldi24main-p424-p (type: Full Paper) doi:10.1145/3656436

Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties
Thibault Dardinier and Peter Müller
(ETH Zurich, Switzerland)

Publisher's Version Artifacts Reusable Article: pldi24main-p436-p (type: Full Paper) doi:10.1145/3656437

Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language
Gaurav Parthasarathy, Thibault Dardinier, Benjamin Bonneau, Peter Müller, and Alexander J. Summers
(ETH Zurich, Switzerland; Université Grenoble Alpes - CNRS - Grenoble INP - VERIMAG, France; University of British Columbia, Canada)

Publisher's Version Artifacts Reusable Article: pldi24main-p451-p (type: Full Paper) doi:10.1145/3656438

Live Verification in an Interactive Proof Assistant
Samuel Gruetter, Viktor Fukala, and Adam Chlipala
(Massachusetts Institute of Technology, USA)

Publisher's Version Archive submitted (440 kB) Artifacts Reusable Article: pldi24main-p457-p (type: Full Paper) doi:10.1145/3656439

Bringing the WebAssembly Standard up to Speed with SpecTec
Dongjun Youn, Wonho Shin, Jaehyun Lee, Sukyoung Ryu, Joachim Breitner, Philippa Gardner, Sam Lindley, Matija Pretnar, Xiaojia Rao, Conrad Watt, and Andreas Rossberg
(KAIST, South Korea; Independent, Germany; Imperial College London, United Kingdom; University of Edinburgh, United Kingdom; University of Ljubljana, Slovenia; University of Cambridge, United Kingdom)

Publisher's Version Artifacts Functional Article: pldi24main-p462-p (type: Full Paper) doi:10.1145/3656440

Space-Efficient Polymorphic Gradual Typing, Mostly Parametric
Atsushi Igarashi, Shota Ozaki, Taro Sekiyama, and Yudai Tanabe
(Kyoto University, Japan; National Institute of Informatics, Japan; SOKENDAI, Japan; Tokyo Institute of Technology, Japan)

Publisher's Version Archive submitted (930 kB) Article: pldi24main-p478-p (type: Full Paper) doi:10.1145/3656441

Quest Complete: The Holy Grail of Gradual Security
Tianyu Chen and Jeremy G. Siek
(Indiana University, USA)

Publisher's Version Archive submitted (360 kB) Artifacts Reusable Article: pldi24main-p494-p (type: Full Paper) doi:10.1145/3656442

Compatible Branch Coverage Driven Symbolic Execution for Efficient Bug Finding
Qiuping Yi, Yifan Yu, and Guowei Yang
(Beijing University of Posts and Telecommunications, China; University of Queensland, Australia)

Publisher's Version Artifacts Reusable Article: pldi24main-p508-p (type: Full Paper) doi:10.1145/3656443

RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly
Michael Fitzgibbons, Zoe Paraskevopoulou, Noble Mushtak, Michelle Thalakottur, Jose Sulaiman Manzur, and Amal Ahmed
(Northeastern University, USA; Ethereum Foundation, Germany)

Publisher's Version Artifacts Reusable Article: pldi24main-p517-p (type: Full Paper) doi:10.1145/3656444

SpEQ: Translation of Sparse Codes using Equivalences
Avery Laird, Bangtian Liu, Nikolaj Bjørner, and Maryam Mehri Dehnavi
(University of Toronto, Canada; Microsoft Research, USA)

Publisher's Version Artifacts Reusable Article: pldi24main-p521-p (type: Full Paper) doi:10.1145/3656445

Foundational Integration Verification of a Cryptographic Server
Andres Erbsen, Jade Philipoom, Dustin Jamner, Ashley Lin, Samuel Gruetter, Clément Pit-Claudel, and Adam Chlipala
(Google, USA; Google, Germany; Massachusetts Institute of Technology, USA; EPFL, Switzerland)

Publisher's Version Artifacts Reusable Article: pldi24main-p523-p (type: Full Paper) doi:10.1145/3656446

Reward-Guided Synthesis of Intelligent Agents with Control Structures
Guofeng Cui, Yuning Wang, Wenjie Qiu, and He Zhu
(Rutgers University, USA)

Publisher's Version Artifacts Reusable Article: pldi24main-p553-p (type: Full Paper) doi:10.1145/3656447

Compiling Probabilistic Programs for Variable Elimination with Information Flow
Jianlin Li, Eric Wang, and Yizhou Zhang
(University of Waterloo, Canada)

Publisher's Version Artifacts Reusable Article: pldi24main-p588-p (type: Full Paper) doi:10.1145/3656448

SPORE: Combining Symmetry and Partial Order Reduction
Michalis Kokologiannakis, Iason Marmanis, and Viktor Vafeiadis
(MPI-SWS, Germany)

Publisher's Version Artifacts Reusable Article: pldi24main-p601-p (type: Full Paper) doi:10.1145/3656449

Predictable Verification using Intrinsic Definitions
Adithya Murali, Cody Rivera, and P. Madhusudan
(University of Illinois at Urbana-Champaign, USA)

Publisher's Version Archive submitted (760 kB) Artifacts Reusable ACM SIGPLAN Best Paper Award Article: pldi24main-p621-p (type: Full Paper) doi:10.1145/3656450

Context-Free Language Reachability via Skewed Tabulation
Yuxiang Lei, Camille Bossut, Yulei Sui, and Qirun Zhang
(UNSW, Australia; Georgia Institute of Technology, USA)

Publisher's Version Archive submitted (810 kB) Artifacts Reusable Article: pldi24main-p632-p (type: Full Paper) doi:10.1145/3656451

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

Publisher's Version Artifacts Reusable Article: pldi24main-p644-p (type: Full Paper) doi:10.1145/3656452

Version of Record: Version of Record to “Falcon: A Scalable Analytical Cache Model” by Arjun Pitchanathan, Kunwar Grover, and Tobias Grosser, published in Proc. ACM Program. Lang. 8, PLDI, Article 222 (June 2024), https://doi.org/10.1145/3656452.

Equivalence by Canonicalization for Synthesis-Backed Refactoring
Justin Lubin, Jeremy Ferguson, Kevin Ye, Jacob Yim, and Sarah E. Chasins
(University of California at Berkeley, Berkeley, USA)

Publisher's Version Archive submitted (750 kB) Artifacts Reusable Article: pldi24main-p645-p (type: Full Paper) doi:10.1145/3656453

KATch: A Fast Symbolic Verifier for NetKAT
Mark Moeller, Jules Jacobs, Olivier Savary Belanger, David Darais, Cole Schlesinger, Steffen Smolka, Nate Foster, and Alexandra Silva
(Cornell University, USA; Galois, USA; Google, USA)

Publisher's Version Artifacts Reusable Article: pldi24main-p646-p (type: Full Paper) doi:10.1145/3656454

Hyperblock Scheduling for Verified High-Level Synthesis
Yann Herklotz and John Wickerson
(Imperial College London, United Kingdom)

Publisher's Version Artifacts Reusable Article: pldi24main-p654-p (type: Full Paper) doi:10.1145/3656455

Numerical Fuzz: A Type System for Rounding Error Analysis
Ariel E. Kellison and Justin Hsu
(Cornell University, USA)

Publisher's Version Artifacts Reusable Article: pldi24main-p666-p (type: Full Paper) doi:10.1145/3656456

Inductive Approach to Spacer
Takeshi Tsukada and Hiroshi Unno
(Chiba University, Japan; Tohoku University, Japan)

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

V-Star: Learning Visibly Pushdown Grammars from Program Inputs
Xiaodong Jia and Gang Tan
(Pennsylvania State University, USA)

Publisher's Version Archive submitted (800 kB) Artifacts Reusable Article: pldi24main-p779-p (type: Full Paper) doi:10.1145/3656458

Hashing Modulo Context-Sensitive 𝛼-Equivalence
Lasse Blaauwbroek, Miroslav Olšák, and Herman Geuvers
(Institut des Hautes Études Scientifiques, France; Radboud University Nijmegen, Netherlands)

Publisher's Version Artifacts Reusable Article: pldi24main-p796-p (type: Full Paper) doi:10.1145/3656459

Syntactic Code Search with Sequence-to-Tree Matching: Supporting Syntactic Search with Incomplete Code Fragments
Gabriel Matute, Wode Ni, Titus Barik, Alvin Cheung, and Sarah E. Chasins
(University of California at Berkeley, Berkeley, USA; Carnegie Mellon University, USA; Apple, USA)

Publisher's Version Artifacts Functional Article: pldi24main-p804-p (type: Full Paper) doi:10.1145/3656460

Static Analysis for Checking the Disambiguation Robustness of Regular Expressions
Konstantinos Mamouras, Alexis Le Glaunec, Wu Angela Li, and Agnishom Chattopadhyay
(Rice University, USA)

Publisher's Version Article: pldi24main-p806-p (type: Full Paper) doi:10.1145/3656461

Equivalence and Similarity Refutation for Probabilistic Programs
Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný, and Đorđe Žikelić
(IST Austria, Austria; Masaryk University, Czechia; Singapore Management University, Singapore)

Publisher's Version Artifacts Reusable Article: pldi24main-p847-p (type: Full Paper) doi:10.1145/3656462

Probabilistic Programming with Programmable Variational Inference
McCoy R. Becker, Alexander K. Lew, Xiaoyan Wang, Matin Ghavami, Mathieu Huot, Martin C. Rinard, and Vikash K. Mansinghka
(Massachusetts Institute of Technology, USA)

Publisher's Version Artifacts Reusable Article: pldi24main-p861-p (type: Full Paper) doi:10.1145/3656463

PL4XGL: A Programming Language Approach to Explainable Graph Learning
Minseok Jeon, Jihyeok Park, and Hakjoo Oh
(Korea University, South Korea)

Publisher's Version Archive submitted (680 kB) Article: pldi24main-p875-p (type: Full Paper) doi:10.1145/3656464

A Family of Fast and Memory Efficient Lock- and Wait-Free Reclamation
Ruslan Nikolaev and Binoy Ravindran
(Pennsylvania State University, USA; Virginia Tech, USA)

Publisher's Version Artifacts Reusable Article: pldi24main-p456-p (type: Full Paper) doi:10.1145/3658851