PLDI 2021
87 papers
- AKG: automatic kernel generation for neural processing units using polyhedral transformations
- Abstraction for conflict-free replicated data types
- Adaptive restarts for stochastic synthesis
- Alive2: bounded translation validation for LLVM
- An efficient interpreter for Datalog by de-specializing relations
- Automated conformance testing for JavaScript engines via deep compiler fuzzing
- Automatically enforcing fresh and consistent inputs in intermittent systems
- Beyond the elementary representations of program invariants over algebraic data types
- Bliss: auto-tuning complex applications using a pool of diverse lightweight learning models
- Boosting SMT solver performance on mixed-bitwise-arithmetic expressions
- Canary: practical static detection of inter-thread value-flow bugs
- Central moment analysis for cost accumulators in probabilistic programs
- Chianina: an evolving graph system for flow- and context-sensitive analyses of million lines of C code
- CoStar: a verified ALL(*) parser
- CompCertO: compiling certified open C components
- Compiler-assisted object inlining with value fields
- Compiling Stan to generative probabilistic languages and extension to deep probabilistic programming
- Concise, type-safe, and efficient structural diffing
- Concolic program repair
- Concurrent deferred reference counting with constant-time overhead
- Cyclic program synthesis
- DIY assistant: a multi-modal end-user programmable virtual assistant
- DNNFusion: accelerating deep neural networks execution with advanced operator fusion
- DeepCuts: a deep learning optimization framework for versatile GPU workloads
- Demanded abstract interpretation
- Developer and user-transparent compiler optimization for interactive applications
- Distance-in-time versus distance-in-space
- DreamCoder: bootstrapping inductive program synthesis with wake-sleep library learning
- Example-guided synthesis of relational queries
- Execution reconstruction: harnessing failure reoccurrences for failure reproduction
- Fast and precise certification of transformers
- Filling typed holes with live GUIs
- Fluid: a framework for approximate concurrency via controlled dependency relaxation
- Frequent background polling on a shared thread, using light-weight compiler interrupts
- Gleipnir: toward practical error analysis for Quantum programs
- Hashing modulo alpha-equivalence
- High performance correctly rounded math libraries for 32-bit floating point representations
- IOOpt: automatic derivation of I/O complexity bounds for affine programs
- Incremental whole-program analysis in Datalog with lattices
- Integration verification across software and hardware for a simple embedded system
- JPortal: precise and efficient control-flow tracing for JVM programs with Intel processor trace
- Learning to find naming issues with big code and small supervision
- Logical bytecode reduction
- Mirror: making lock-free data structures persistent
- Modular data-race-freedom guarantees in the promising semantics
- On probabilistic termination of functional programs with continuous distributions
- Path-sensitive sparse analysis without path conditions
- Perceus: garbage free reference counting with reuse
- Phased synthesis of divide and conquer programs
- Polynomial reachability witnesses via Stellensätze
- Porcupine: a synthesizing compiler for vectorized homomorphic encryption
- Practical smart contract sharding with ownership and commutativity analysis
- Proof repair across type equivalences
- Provable repair of deep neural networks
- Proving non-termination by program reversal
- Quantitative analysis of assertion violations in probabilistic programs
- Quantum abstract interpretation
- RbSyn: type- and effect-guided program synthesis
- RefinedC: automating the foundational verification of C code with refined ownership types
- Repairing serializability bugs in distributed database programs via automated schema refactoring
- Reticle: a virtual machine for programming modern FPGAs
- Retrofitting effect handlers onto OCaml
- Revamping hardware persistency models: view-based and axiomatic persistency models for Intel-x86 and Armv8
- Reverse engineering for reduction parallelization via semiring polynomials
- Robustness certification with generative models
- SPPL: probabilistic programming with fast exact symbolic inference
- Satisfiability modulo ordering consistency theory for multi-threaded program verification
- Scooter & Sidecar: a domain-specific approach to writing secure database migrations
- Snapshot-free, transparent, and robust memory reclamation for lock-free data structures
- Sound probabilistic inference via guide types
- Specification synthesis with constrained Horn clauses
- SyRust: automatic testing of Rust libraries with semantic-aware program synthesis
- Symbolic Boolean derivatives for efficiently solving extended regular expression constraints
- Synthesizing data structure refinements from integrity constraints
- Task parallel assembly language for uncompromising parallelism
- Termination analysis without the tears
- Test-case reduction and deduplication almost for free with transformation-based compiler testing
- Trace-based control-flow analysis
- Transfinite Iris: resolving an existential dilemma of step-indexed separation logic
- Unleashing the hidden power of compiler optimization on binary code difference: an empirical study
- Unqomp: synthesizing uncomputation in Quantum circuits
- Vectorized secure evaluation of decision forests
- Viaduct: an extensible, optimizing compiler for secure distributed programs
- Web question answering with neurosymbolic program synthesis
- When threads meet events: efficient and precise static race detection with origins
- Wire sorts: a language abstraction for safe hardware composition
- Zooid: a DSL for certified multiparty computation: from mechanised metatheory to certified multiparty processes