OOPSLA 2026
75 papers
- (Dis)Proving Spectre Security with Speculation-Passing Style
- A Minimalist Proof Language for Neural Theorem Proving over Isabelle/HOL
- A Tale of 1001 LoC: Potential Runtime Error-Guided Specification Synthesis for Verifying Large-Scale Programs
- Automatic Propagation of Profile Information through the Optimization Pipeline
- Beacon: Detecting Broken Access Control Vulnerabilities in DBMSs via System Catalog Consistency Validation
- Beer: Interactive Alarm Resolution in Bayesian Program Analysis via Exploration-Exploitation
- Beyond Coverage: Automatic Test Suite Augmentation for Enhanced Effectiveness using Large Language Models
- Block Tests
- CLower: Detecting Compiler Pessimization Bugs through Redundant Memory Accesses
- CMakeSonar: A Static Approach to Detecting CMake Bugs with a Fine-Grained Type System
- Class-Dictionary Specialization with Rank-2 Polymorphic Functions
- Commuting Conversions and Join Points for Call-by-Push-Value
- Context-Free Language Reachability via Efficient Relation Chaining
- DeCo: A Core Calculus for Incremental Functional Programming with Generic Data Types
- Debugging Debugging Information using Dynamic Call Trees
- Decompiling for Constant-Time Analysis
- Deegen: A JIT-Capable VM Generator for Dynamic Languages
- Designing GPU Data Structures for Efficient Memory Oversubscription
- Detecting Flaky Tests by Controlling Nondeterministic API Behavior
- Determining the Unreachable: Constraint-Guided Reachability Analysis for Dependency Vulnerabilities
- Diatom: Polylithic Binary Lifting with Data-Flow Summaries and Type-Aware IR Linking
- Differential Execution with Lexical Tracing
- EditFlow: Benchmarking and Optimizing Code Edit Recommendation Systems via Reconstruction of Developer Flows
- Effectively Propositional Higher-Order Functional Programming
- Efficient Directed Hybrid Fuzzing via Target-Centric Seed Selection and Generation
- Efficient Incremental GR(1) Synthesis via Monotonic Fixed-Point Reuse
- Fail Faster: Staging and Fast Randomness for High-Performance PBT
- Floating-Point Usage on GitHub: A Large-Scale Study of Statically Typed Languages
- Frashokereti: Non-aborting Optimistically Replicated Objects
- From Raw Pointers to Memory Safety: A Modular Demand-Driven Typestate Analysis for Rust
- Fully-Automatic Type Inference for Borrows with Lifetimes
- Geo: A Query Rewrite Framework for Graph Pattern Mining
- Grammar Repair with Examples and Tree Automata
- Handling Exceptions and Effects with Automatic Resource Analysis
- Hermes: Making Path-Sensitive Pointer Analysis Scalable for Sparse Value-Flow Analysis
- Hunting CUDA Bugs at Scale with cuFuzz
- Hybrid Game Control Envelope Synthesis
- IRIDIUM: A Framework for Statically Optimizing JavaScript Programs
- InspectCoder: Dynamic Analysis-Driven Self Repair through Interactive LLM-Debugger Collaboration
- LARTS: Language Abstractions for Real-Time and Secure Systems
- LLM-Powered Silent Bug Fuzzing in Deep Learning Libraries via Versatile and Controlled Bug Transfer
- Lawyer: Modular Obligations-Based Liveness Reasoning in Higher-Order Impredicative Concurrent Separation Logic
- Learning Symmetric Invariants from Symmetric Samples
- Localizing Type Errors for Syntactic Sugar by Lifting
- Mechanically Translating Iterative Dataflow Analysis to Algebraic Program Analysis
- Mechanised Semantics of Multi-stage Programming
- MetaSpace: Metamorphic Testing for Spatial Cognition in Embodied Agents
- Metamorphic Testing for Infrastructure-as-Code Engines
- Mixed Choice in Asynchronous Multiparty Session Types
- Mixtris: Mechanised Higher-Order Separation Logic for Mixed Choice Multiparty Message Passing
- OBsmith: LLM-Powered JavaScript Obfuscator Testing
- Online Input Grammar Synthesis Aided Symbolic Execution
- PLEX: Normalization for Refinement Types
- Peeling Off the Cocoon: Unveiling Suppressed Golden Seeds for Mutational Greybox Fuzzing
- Phaedrus: Predicting Dynamic Application Behavior with Lightweight Generative Models and LLMs
- Process-Centric Analysis of Agentic Software Systems
- Prunario: Testing Autonomous Driving Systems by Pruning Likely Redundant Scenarios
- RAT-CAT-SAT: Model Checking Memory Consistency Models
- RandSet: Randomized Corpus Reduction for Fuzzing Seed Scheduling
- Reframing Paths as Logic: Semantic Segmentation for Vulnerability Detection
- SART: Sign-Absolute Reformulation Theory for Binary Variable Reduction in Neural Network Verification
- Scylla: Translating an Applicative Subset of C to Safe Rust
- Sound and Complete Invariant-Based Heap Encodings
- Speak Now: Safe Actor Programming with Multiparty Session Types
- Specy: Learning Specifications for Distributed Systems from Event Traces
- Static Factorisation of Probabilistic Programs with User-Labelled Sample Statements and While Loops
- SymGPT: Auditing Smart Contracts via Combining Symbolic Execution with Large Language Models
- Taming the Hydra: Targeted Control-Flow Transformations for Dynamic Symbolic Execution
- Type Inference for Functional and Imperative Dynamic Languages
- Type-Safe Monotonic Object Evolution
- Understanding and Finding JIT Compiler Performance Bugs
- VeriEQ: Finding Verilog Simulators and Synthesizers Bugs with Equivalence Circuit Transformation
- When Lifetimes Liberate: A Type System for Arenas with Higher-Order Reachability Tracking
- When Specifications Meet Reality: Uncovering API Inconsistencies in Ethereum Infrastructure
- noDice: Inference for Discrete Probabilistic Programs with Nondeterminism and Conditioning