PLDI 2023
83 papers
- A Lineage-Based Referencing DSL for Computer-Aided Design
- A Type System for Safe Intermittent Computing
- Abstract Interpretation of Fixpoint Iterators with Applications to Neural Networks
- Absynthe: Abstract Interpretation-Guided Synthesis
- An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits
- Architecture-Preserving Provable Repair of Deep Neural Networks
- Automated Detection of Under-Constrained Circuits in Zero-Knowledge Proofs
- Automated Expected Value Analysis of Recursive Programs
- Better Defunctionalization through Lambda Set Specialization
- Better Together: Unifying Datalog and Equality Saturation
- Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic
- CQS: A Formally-Verified Framework for Fair and Abortable Synchronization
- Cakes That Bake Cakes: Dynamic Computation in CakeML
- Collecting Cyclic Garbage across Foreign Function Interfaces: Who Takes the Last Piece of Cake?
- CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity
- Compound Memory Models
- Conflict-Driven Synthesis for Layout Engines
- Context Sensitivity without Contexts: A Cut-Shortcut Approach to Fast and Precise Pointer Analysis
- Covering All the Bases: Type-Based Verification of Test Input Generators
- CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives
- Cutting the Cake: A Language for Fair Division
- Defunctionalization with Dependent Types
- Derivative Based Nonbacktracking Real-World Regex Matching with Backtracking Semantics
- Discrete Adversarial Attack to Models of Code
- Don't Look UB: Exposing Sanitizer-Eliding Compiler Optimizations
- Dynamic Partial Order Reduction for Checking Correctness against Transaction Isolation Levels
- Efficient Parallel Functional Programming with Effects
- Embedding Hindsight Reasoning in Separation Logic
- Extensible Metatheory Mechanization via Family Polymorphism
- Fair Operational Semantics
- Feature-Sensitive Coverage for Conformance Testing of Programming Language Implementations
- Flux: Liquid Types for Rust
- Formally Verified Samplers from Probabilistic Programs with Loops and Conditioning
- Fuzzing Loop Optimizations in Compilers for C++ and Data-Parallel Languages
- Garbage-Collection Safety for Region-Based Type-Polymorphic Programs
- Generalized Policy-Based Noninterference for Efficient Confidentiality-Preservation
- HEaaN.MLIR: An Optimizing Compiler for Fast Ring-Based Homomorphic Encryption
- ImageEye: Batch Image Processing using Program Synthesis
- Incremental Verification of Neural Networks
- Indexed Streams: A Formal Intermediate Representation for Fused Contraction Programs
- Inductive Program Synthesis via Iterative Forward-Backward Abstract Interpretation
- Interval Parsing Grammars for File Format Parsing
- Iris-Wasm: Robust and Modular Verification of WebAssembly Programs
- Leveraging Rust Types for Program Synthesis
- Lilac: A Modal Separation Logic for Conditional Probability
- Loop Rerolling for Hardware Decompilation
- Memento: A Framework for Detectable Recoverability in Persistent Memory
- Merging Inductive Relations
- Modular Control Plane Verification via Temporal Invariants
- Modular Hardware Design with Timeline Types
- Mosaic: An Interoperable Compiler for Tensor Algebra
- Mostly Automated Proof Repair for Verified Libraries
- Obtaining Information Leakage Bounds via Approximate Model Counting
- One Pixel Adversarial Attacks via Sketched Programs
- Optimal Reads-From Consistency Checking for C11-Style Memory Models
- Parallelism in a Region Inference Context
- Parameterized Algebraic Protocols
- Performal: Formal Verification of Latency Properties for Distributed Systems
- Probabilistic Programming with Stochastic Probabilities
- Program Reconditioning: Avoiding Undefined Behaviour When Finding and Reducing Compiler Bugs
- Prompting Is Programming: A Query Language for Large Language Models
- Proving and Disproving Equivalence of Functional Programming Assignments
- Psym: Efficient Symbolic Exploration of Distributed Systems
- PureCake: A Verified Compiler for a Lazy Functional Language
- Putting Weak Memory in Order via a Promising Intermediate Representation
- Recursive State Machine Guided Graph Folding for Context-Free Language Reachability
- Register Tiling for Unstructured Sparsity in Neural Network Inference
- Reliable Actors with Retry Orchestration
- Repairing Regular Expressions for Extraction
- Responsive Parallelism with Synchronization
- Scallop: A Language for Neurosymbolic Programming
- Search-Based Regular Expression Inference on a GPU
- Sound Dynamic Deadlock Prediction in Linear Time
- Synthesizing MILP Constraints for Efficient and Robust Optimization
- Synthesizing Quantum-Circuit Optimizers
- Taype: A Policy-Agnostic Language for Oblivious Computation
- Trace-Guided Inductive Synthesis of Recursive Functional Programs
- Type-Checking CRDT Convergence
- VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A
- Verified Density Compilation for a Probabilistic Programming Language
- WasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for WebAssembly
- cuCatch: A Debugging Tool for Efficiently Catching Memory Safety Violations in CUDA Applications
- flap: A Deterministic Parser with Fused Lexing