There are 10 paper titles which come from either PLDI 2014 or PLDI 2024. (Year drawn at random, then paper.) Can you guess which is which?
- Adaptive, Efficient Parallel Execution of Parallel Programs
- Doppio: Breaking the Browser Language Barrier
- Expressing and Verifying Probabilistic Assertions
- Modular Control-Flow Integrity
- Don't Sweat the Small Stuff: Formal Verification of C Code Without the Pain
- Test-Driven Synthesis
- Compiler-Assisted Detection of Transient Memory Errors
- FlowDroid: Precise Context, Flow, Field, Object-sensitive and Lifecycle-aware Taint Analysis for Android Apps
- Dynamic Enforcement of Determinism in a Parallel Scripting Language
- End-to-End Verification of Stack-Space Bounds for C Programs
- Stochastic Optimization of Floating Point Programs using Tunable Precision
- Slicing Probabilistic Programs
- A Theory of Changes for Higher-Order Languages — Incrementalizing λ-Calculi by Static Differentiation
- Program Consolidation
- Globally Precise-restartable Execution of Parallel Programs
- First-class Runtime Generation of High-performance Types using Exotypes
- Getting F-Bounded Polymorphism Back into Shape
- Fast: a Transducer-Based Language for Tree Manipulation
- SCCharts: Sequentially Constructive Statecharts for Safety-Critical Applications
- Race Detection for Android Applications
- Taming the Parallel Effect Zoo: Extensible Deterministic Parallelism with Lvish
- Optimal Inference of Fields in Row-Polymorphic Records
- Persistent Pointer Information
- Maximal Sound Predictive Race Detection With Control Flow Abstraction
- Surgical Precision JIT Compilers
- VeriCon: Towards Verifying Controller Programs in Software-Defined Networks
- Selective Context-Sensitivity Guided by Impact Pre-Analysis
- Lifting Reduction Semantics through Syntactic Sugar
- Introspective Analysis: Context-Sensitivity, Across the Board
- Code Completion with Statistical Language Models
- Commutativity Race Detection
- DoubleChecker: Efficient Sound and Precise Atomicity Checking
- Adapton: Composable, Demand-Driven Incremental Computation
- Natural Proofs for Data-structure Manipulation in C
- Verification Modulo Versions: Towards Usable Verification
- On Abstraction Refinement for Program Analyses in Datalog
- Hybrid Top-down and Bottom-up Interprocedural Analysis
- Compositional Solution Space Quantification for Probabilistic Software Analysis
- Race Detection for Event-Driven Mobile Applications
- A Model Counter For Constraints Over Unbounded Strings
- Improving JavaScript Performance Through Predictable Type Specialization
- FlashExtract: A Framework for Data Extraction by Examples
- Compiler Validation via Equivalence Modulo Inputs
- Test Driven Repair of Data Races in Structured Parallel Programs
- Accurate Application Progress Analysis for Large-Scale Parallel Debugging
- Automatic Runtime Error Repair and Containment via Recovery Shepherding
- Automating Formal Proofs for Reactive Systems
- Chlorophyll: Synthesis-Aided Compiler for Low-Power Spatial Architectures
- A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages
- Resource Limits for Haskell
- A Framework for Enhancing Data Reuse via Associative Reordering
- Tracelet-Based Code Search in Executables
- The Future of Fast Code: Giving Hardware What It Wants
- Bit Blasting Probabilistic Programs
- Compiling Probabilistic Programs for Variable Elimination with Information Flow
- Equivalence and Similarity Refutation for Probabilistic Programs
- GenSQL: A Probabilistic Programming System for Querying Generative Models of Database Tables
- Probabilistic Programming with Programmable Variational Inference
- Compilation of Qubit Circuits to Optimized Qutrit Circuits
- Qubit Recycling Revisited
- The T-Complexity Costs of Error Correction for Control Flow in Quantum Computation
- Compiling Conditional Quantum Gates without Using Helper Qubits
- An Algebraic Language for Specifying Quantum Networks
- Daedalus: Safer Document Parsing
- SpEQ: Translation of Sparse Codes using Equivalences
- Compiling with Abstract Interpretation
- Don’t Write, but Return: Replacing Output Parameters with Algebraic Data Types in C-to-Rust Translation
- Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving
- Consolidating Smart Contracts with Behavioral Contracts
- NetBlocks: Staging Layouts for High-Performance Custom Host Network Stacks
- KATch: A Fast Symbolic Verifier for NetKAT
- Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language
- Verified Extraction from Coq to OCaml
- Verification under Intel-x86 with Persistency
- RefinedRust: A Type System for High-Assurance Verification of Rust Programs
- Hyperblock Scheduling for Verified High-Level Synthesis
- Space-Efficient Polymorphic Gradual Typing, Mostly Parametric
- Associated Effects
- Decidable Subtyping of Existential Types for Julia
- Numerical Fuzz: A Type System for Rounding Error Analysis
- Stream Types
- A Tensor Compiler with Automatic Data Packing for Simple and Efficient Fully Homomorphic Encryption
- Quantitative Robustness for Vulnerability Assessment
- Quest Complete: The Holy Grail of Gradual Security
- Foundational Integration Verification of a Cryptographic Server
- Refined Input, Degraded Output: The Counterintuitive World of Compiler Behavior
- Compatible Branch Coverage Driven Symbolic Execution for Efficient Bug Finding
- Diffy: Data-Driven Bug Finding for Configurations
- Boosting Compiler Testing by Injecting Real-World Code
- A Verified Compiler for a Functional Tensor Language
- Compilation of Modular and General Sparse Workspaces
- Descend: A Safe GPU Systems Programming Language
- AI-Assisted Programming Today and Tomorrow
- The Functional Essence of Imperative Binary Search Trees
- Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq
- Maximum Consensus Floating Point Solutions for Infeasible Low-Dimensional Linear Programs with Convex Hull as the Intermediate Representation
- Live Verification in an Interactive Proof Assistant
- Predictable Verification using Intrinsic Definitions
- Linear Matching of JavaScript Regular Expressions
- RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly
- Bringing the WebAssembly Standard up to Speed with SpecTec
- Optimistic Stack Allocation and Dynamic Heapification for Managed Runtimes
- Concurrent Immediate Reference Counting
- Equivalence by Canonicalization for Synthesis-Backed Refactoring
- PL4XGL: A Programming Language Approach to Explainable Graph Learning
- Syntactic Code Search with Sequence-to-Tree Matching
- V-Star: Learning Visibly Pushdown Grammars from Program Inputs
- Hashing Modulo Context-Sensitive Alpha-Equivalence
- Mechanised Hypersafety Proofs about Structured Data
- Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties
- A HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite Automata
- SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT Techniques
- Inductive Approach to Spacer
- SMT Theory Arbitrage: Approximating Unbounded Constraints using Bounded Theories
- Much Still to Do in Compiler Verification (A Perspective from the CakeML Project)
- From Batch to Stream: Automatic Generation of Online Algorithms
- Superfusion: Eliminating Intermediate Data Structures via Inductive Synthesis
- Recursive Program Synthesis using Paramorphisms
- Reward-Guided Synthesis of Intelligent Agents with Control Structures
- A Lightweight Polyglot Code Transformation Language
- SPORE: Combining Symmetry and Partial Order Reduction
- IsoPredict: Dynamic Predictive Analysis for Detecting Unserializable Behaviors in Weakly Isolated Data Store Applications
- LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs
- A Family of Fast and Memory Efficient Lock- and Wait-Free Reclamation
- Efficient Static Vulnerability Analysis for JavaScript with Multiversion Dependency Graphs
- Floating-Point TVPI Abstract Domain
- Reducing Static Analysis Unsoundness with Approximate Interpretation
- Falcon: A Scalable Analytical Cache Model
- Falcon: A Fused Approach to Path-Sensitive Sparse Data Dependence Analysis
- A Proof Recipe for Linearizability in Relaxed Memory Separation Logic
- Compositional Semantics for Shared-Variable Concurrency
- Input-Relational Verification of Deep Neural Networks
- Automated Verification of Fundamental Algebraic Laws
- Allo: A Programming Model for Composable Accelerator Design
- VESTA: Power Modeling with Language Runtime Events
- Modular Hardware Design of Pipelined Circuits with Hazards
- Jacdac: Service-Based Prototyping of Embedded Systems
- Wavefront Threading Enables Effective High-Level Synthesis
- Scaling Type-Based Points-to Analysis with Saturation
- Program Analysis for Adaptive Data Analysis
- Robust Resource Bounds with Static Analysis and Bayesian Inference
- Context-Free Language Reachability via Skewed Tabulation
- Static Analysis for Checking the Disambiguation Robustness of Regular Expressions
Loading...
Total score: