PLDI 2024
89 papers
- A Family of Fast and Memory Efficient Lock- and Wait-Free Reclamation
- A HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite Automata
- A Lightweight Polyglot Code Transformation Language
- A Proof Recipe for Linearizability in Relaxed Memory Separation Logic
- A Tensor Compiler with Automatic Data Packing for Simple and Efficient Fully Homomorphic Encryption
- A Verified Compiler for a Functional Tensor Language
- Allo: A Programming Model for Composable Accelerator Design
- An Algebraic Language for Specifying Quantum Networks
- Associated Effects: Flexible Abstractions for Effectful Programming
- Automated Verification of Fundamental Algebraic Laws
- Bit Blasting Probabilistic Programs
- Boosting Compiler Testing by Injecting Real-World Code
- Bringing the WebAssembly Standard up to Speed with SpecTec
- Compatible Branch Coverage Driven Symbolic Execution for Efficient Bug Finding
- Compilation of Modular and General Sparse Workspaces
- Compilation of Qubit Circuits to Optimized Qutrit Circuits
- Compiling Conditional Quantum Gates without Using Helper Qubits
- Compiling Probabilistic Programs for Variable Elimination with Information Flow
- Compiling with Abstract Interpretation
- Compositional Semantics for Shared-Variable Concurrency
- Concurrent Immediate Reference Counting
- Consolidating Smart Contracts with Behavioral Contracts
- Context-Free Language Reachability via Skewed Tabulation
- Daedalus: Safer Document Parsing
- Decidable Subtyping of Existential Types for Julia
- Descend: A Safe GPU Systems Programming Language
- Diffy: Data-Driven Bug Finding for Configurations
- Don't Write, but Return: Replacing Output Parameters with Algebraic Data Types in C-to-Rust Translation
- Efficient Static Vulnerability Analysis for JavaScript with Multiversion Dependency Graphs
- Equivalence and Similarity Refutation for Probabilistic Programs
- Equivalence by Canonicalization for Synthesis-Backed Refactoring
- Falcon: A Fused Approach to Path-Sensitive Sparse Data Dependence Analysis
- Falcon: A Scalable Analytical Cache Model
- Floating-Point TVPI Abstract Domain
- Foundational Integration Verification of a Cryptographic Server
- From Batch to Stream: Automatic Generation of Online Algorithms
- GenSQL: A Probabilistic Programming System for Querying Generative Models of Database Tables
- Hashing Modulo Context-Sensitive 𝛼-Equivalence
- Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties
- Hyperblock Scheduling for Verified High-Level Synthesis
- Inductive Approach to Spacer
- Input-Relational Verification of Deep Neural Networks
- IsoPredict: Dynamic Predictive Analysis for Detecting Unserializable Behaviors in Weakly Isolated Data Store Applications
- Jacdac: Service-Based Prototyping of Embedded Systems
- KATch: A Fast Symbolic Verifier for NetKAT
- LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs
- Linear Matching of JavaScript Regular Expressions
- Live Verification in an Interactive Proof Assistant
- Maximum Consensus Floating Point Solutions for Infeasible Low-Dimensional Linear Programs with Convex Hull as the Intermediate Representation
- Mechanised Hypersafety Proofs about Structured Data
- Modular Hardware Design of Pipelined Circuits with Hazards
- NetBlocks: Staging Layouts for High-Performance Custom Host Network Stacks
- Numerical Fuzz: A Type System for Rounding Error Analysis
- Optimistic Stack Allocation and Dynamic Heapification for Managed Runtimes
- PL4XGL: A Programming Language Approach to Explainable Graph Learning
- Predictable Verification using Intrinsic Definitions
- Probabilistic Programming with Programmable Variational Inference
- Program Analysis for Adaptive Data Analysis
- Quantitative Robustness for Vulnerability Assessment
- Qubit Recycling Revisited
- Quest Complete: The Holy Grail of Gradual Security
- Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq
- Recursive Program Synthesis using Paramorphisms
- Reducing Static Analysis Unsoundness with Approximate Interpretation
- Refined Input, Degraded Output: The Counterintuitive World of Compiler Behavior
- RefinedRust: A Type System for High-Assurance Verification of Rust Programs
- Reward-Guided Synthesis of Intelligent Agents with Control Structures
- RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly
- Robust Resource Bounds with Static Analysis and Bayesian Inference
- SMT Theory Arbitrage: Approximating Unbounded Constraints using Bounded Theories
- SPORE: Combining Symmetry and Partial Order Reduction
- Scaling Type-Based Points-to Analysis with Saturation
- SpEQ: Translation of Sparse Codes using Equivalences
- Space-Efficient Polymorphic Gradual Typing, Mostly Parametric
- Static Analysis for Checking the Disambiguation Robustness of Regular Expressions
- Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving
- Stream Types
- SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT Techniques
- Superfusion: Eliminating Intermediate Data Structures via Inductive Synthesis
- Symbolic Execution for Quantum Error Correction Programs
- Syntactic Code Search with Sequence-to-Tree Matching: Supporting Syntactic Search with Incomplete Code Fragments
- The Functional Essence of Imperative Binary Search Trees
- The T-Complexity Costs of Error Correction for Control Flow in Quantum Computation
- Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language
- V-Star: Learning Visibly Pushdown Grammars from Program Inputs
- VESTA: Power Modeling with Language Runtime Events
- Verification under Intel-x86 with Persistency
- Verified Extraction from Coq to OCaml
- Wavefront Threading Enables Effective High-Level Synthesis