OOPSLA 2025
216 papers
- A Complete Formal Semantics of eBPF Instruction Set Architecture for Solana
- A Domain-Specific Probabilistic Programming Language for Reasoning about Reasoning (Or: A Memo on memo)
- A Flow-Sensitive Refinement Type System for Verifying eBPF Programs
- A Hoare Logic for Symmetry Properties
- A Language for Quantifying Quantum Network Behavior
- A Lightweight Type-and-Effect System for Invalidation Safety: Tracking Permanent and Temporary Invalidation with Constraint-Based Subtype Inference
- A Mechanized Semantics for Dataflow Circuits
- A Refinement Methodology for Distributed Programs in Rust
- A Sound Static Analysis Approach to I/O API Migration
- A Unifying Approach to Product Constructions for Quantitative Temporal Inference
- ABC: Towards a Universal Code Styler through Model Merging
- API-Guided Dataset Synthesis to Finetune Large Code Models
- Abstract Interpretation of Temporal Safety Effects of Higher Order Programs
- Abstraction Refinement-Guided Program Synthesis for Robot Learning from Demonstrations
- AccelerQ: Accelerating Quantum Eigensolvers with Machine Learning on Quantum Simulators
- Active Learning for Neurosymbolic Program Synthesis
- Adaptive Shielding via Parametric Safety Proofs
- Adequacy for Algebraic Effects Revisited
- Advancing Performance via a Systematic Application of Research and Industrial Best Practice
- Agora: Trust Less and Open More in Verification for Confidential Computing
- An Empirical Evaluation of Property-Based Testing in Python
- An Empirical Study of Bugs in the rustc Compiler
- ApkDiffer: Accurate and Scalable Cross-Version Diffing Analysis for Android Applications
- Artemis: Toward Accurate Detection of Server-Side Request Forgeries through LLM-Assisted Inter-procedural Path-Sensitive Taint Analysis
- AutoVerus: Automated Proof Generation for Rust Code
- Automated Discovery of Tactic Libraries for Interactive Theorem Proving
- Automated Verification of Soundness of DNN Certifiers
- Automatic Linear Resource Bound Analysis for Rust via Prophecy Potentials
- Automatically Verifying Replication-Aware Linearizability
- Bennet: Randomized Specification Testing for Heap-Manipulating Programs
- Binary Cryptographic Function Identification via Similarity Analysis with Path-Insensitive Emulation
- Bolt-On Strong Consistency: Specification, Implementation, and Verification
- Boosting Program Reduction with the Missing Piece of Syntax-Guided Transformations
- Borrowing from Session Types
- Bridging the Gap between Real-World and Formal Binary Lifting through Filtered-Simulation
- Carapace: Static-Dynamic Information Flow Control in Rust
- Certified Decision Procedures for Width-Independent Bitvector Predicates
- Characterizing Implementability of Global Protocols with Infinite States and Data
- Checking Observational Correctness of Database Systems
- Checking δ-Satisfiability of Reals with Integrals
- Choreographic Quick Changes: First-Class Location (Set) Polymorphism
- CoSSJIT: Combining Static Analysis and Speculation in JIT Compilers
- Code Style Sheets: CSS for Code
- Coinductive Proofs of Regular Expression Equivalence in Zero Knowledge
- Combining Formal and Informal Information in Bayesian Program Analysis via Soft Evidences
- Compiling Classical Sequent Calculus to Stock Hardware: The Duality of Compilation
- Complete the Cycle: Reachability Types with Expressive Cyclic References
- Compositional Quantum Control Flow with Efficient Compilation in Qunity
- Compositional Symbolic Execution for the Next 700 Memory Models
- Compressed and Parallelized Structured Tensor Algebra
- Contract System Metatheories à la Carte: A Transition-System View of Contracts
- Convex Hull Approximation for Activation Functions
- Correct Black-Box Monitors for Distributed Deadlock Detection: Formalisation and Implementation
- Correct-by-Construction: Certified Individual Fairness through Neural Network Training
- Corrigendum: PAFL: Enhancing Fault Localizers by Leveraging Project-Specific Fault Patterns
- Cost of Soundness in Mixed-Precision Tuning
- Counterexample-Guided Inference of Modular Specifications
- DESIL: Detecting Silent Bugs in MLIR Compiler Infrastructure
- Debugging WebAssembly? Put Some Whamm on It!
- Denotational Foundations for Expected Cost Analysis
- DepFuzz: Efficient Smart Contract Fuzzing with Function Dependence Guidance
- Dependency-Aware Compilation for Surface Code Quantum Architectures
- Destination Calculus: A Linear 𝜆-Calculus for Purely Functional Memory Writes
- Detecting and Explaining (In-)equivalence of Context-Free Grammars
- Divide and Conquer: A Compositional Approach to Game-Theoretic Security
- Divining Profiler Accuracy: An Approach to Approximate Profiler Accuracy through Machine Code-Level Slowdown
- Dynamic Wind for Effect Handlers
- Efficient Abstract Interpretation via Selective Widening
- Efficient Algorithms for the Uniform Tokenization Problem
- Efficient Decrease-and-Conquer Linearizability Monitoring
- Efficient Incremental Verification of Neural Networks Guided by Counterexample Potentiality
- Embedding Quantum Program Verification into Dafny
- Encode the ∀∃ Relational Hoare Logic into Standard Hoare Logic
- Enhancing APR with PRISM: A Semantic-Based Approach to Overfitting Patch Detection
- Exploring the Theory and Practice of Concurrency in the Entity-Component-System Pattern
- Extraction and Mutation at a High Level: Template-Based Fuzzing for JavaScript Engines
- FO-Complete Program Verification for Heap Logics
- Fast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification
- Fast Constraint Synthesis for C++ Function Templates
- Faster Explicit-Trace Monitoring-Oriented Programming for Runtime Verification of Software Tests
- Finch: Sparse and Structured Tensor Programming with Control Flow
- Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing
- Flexible and Expressive Typed Path Patterns for GQL
- Flix: A Design for Language-Integrated Datalog
- Float Self-Tagging
- Formalizing Linear Motion G-Code for Invariant Checking and Differential Testing of Fabrication Tools
- Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back
- Fray: An Efficient General-Purpose Concurrency Testing Platform for the JVM
- From Linearity to Borrowing
- Fuzzing C++ Compilers via Type-Driven Mutation
- GALA: A High Performance Graph Neural Network Acceleration LAnguage and Compiler
- Garbage Collection for Rust: The Finalizer Frontier
- Guarding the Privacy of Label-Only Access to Neural Network Classifiers via iDP Verification
- HEMVM: A Heterogeneous Blockchain Framework for Interoperable Virtual Machines
- Hambazi: Spatial Coordination Synthesis for Augmented Reality
- Heap-Snapshot Matching and Ordering using CAHPs: A Context-Augmented Heap-Path Representation for Exact and Partial Path Matching using Prefix Trees
- HeapBuffers: Why Not Just Using a Binary Serialization Format for Your Managed Memory?
- HieraSynth: A Parallel Framework for Complete Super-Optimization with Hierarchical Space Decomposition
- Homomorphism Calculus for User-Defined Aggregations
- HpC: A Calculus for Hybrid and Mobile Systems
- HybridPersist: A Compiler Support for User-Friendly and Efficient PM Programming
- IncIDFA: An Efficient and Generic Algorithm for Incremental Iterative Dataflow Analysis
- Incremental Bidirectional Typing via Order Maintenance
- Incremental Certified Programming
- Inductive Synthesis of Inductive Heap Predicates
- Integrating Resource Analyses via Resource Decomposition
- Interactive Bitvector Reasoning using Verified Bit-Blasting
- Interleaving Large Language Models for Compiler Testing
- JavART: A Lightweight Rule-Based JIT Compiler using Translation Rules Extracted from a Learning Approach
- KestRel: Relational Verification using E-Graphs for Program Alignment
- LOUD: Synthesizing Strongest and Weakest Specifications
- Language-Parametric Reference Synthesis
- Large Language Model Powered Symbolic Execution
- Laurel: Unblocking Automated Verification with Large Language Models
- Liberating Merges via Apartness and Guarded Subtyping
- Lilo: A Higher-Order, Relational Concurrent Separation Logic for Liveness
- MIO: Multiverse Debugging in the Face of Input/Output
- MTP: A Meaning-Typed Language Abstraction for AI-Integrated Programming
- Memory-Safety Verification of Open Programs with Angelic Assumptions
- MetaKernel: Enabling Efficient Encrypted Neural Network Inference through Unified MVM and Convolution
- Metamorph: Synthesizing Large Objects from Dafny Specifications
- Mind the Abstraction Gap: Bringing Equality Saturation to Real-World ML Compilers
- Mini-Batch Robustness Verification of Deep Neural Networks
- Modal Abstractions for Virtualizing Memory Addresses
- Modal Effect Types
- Model-Guided Fuzzing of Distributed Systems
- Modeling Reachability Types with Logical Relations: Semantic Type Soundness, Termination, Effect Safety, and Equational Theory
- Modular Reasoning about Global Variables and Their Initialization
- Multi-Language Probabilistic Programming
- Multi-modal Sketch-Based Behavior Tree Synthesis
- Non-interference Preserving Optimising Compilation
- Notions of Stack-Manipulating Computation and Relative Monads
- On Abstraction Refinement for Bayesian Program Analysis
- On Higher-Order Model Checking of Effectful Answer-Type-Polymorphic Programs
- On the Impact of Formal Verification on Software Development
- Opportunistically Parallel Lambda Calculus
- Orax: A Feedback-Driven Framework for Efficiently Solving Satisfiability Modulo Theories and Oracles
- PAFL: Enhancing Fault Localizers by Leveraging Project-Specific Fault Patterns
- PReMM: LLM-Based Program Repair for Multi-method Bugs via Divide and Conquer
- Pathological Cases for a Class of Reachability-Based Garbage Collectors
- Peepco: Batch-Based Consistency Optimization
- Place Capability Graphs: A General-Purpose Model of Rust's Ownership and Borrowing Guarantees
- Polymorphic Records for Dynamic Languages
- Probabilistic Inference for Datalog with Correlated Inputs
- Products of Recursive Programs for Hypersafety Verification
- Proof Repair across Quotient Type Equivalences
- Pyrosome: Verified Compilation for Modular Metatheory
- P³: Reasoning about Patches via Product Programs
- QED in Context: An Observation Study of Proof Assistant Users
- QbC: Quantum Correctness by Construction
- Qualified Types with Boolean Algebras
- Quantified Underapproximation via Labeled Bunches
- Quantization with Guaranteed Floating-Point Neural Network Classifications
- REPTILE: Performant Tiling of Recurrences
- ROSpec: A Domain-Specific Language for ROS-Based Robot Software
- React-tRace: A Semantics for Understanding React Hooks: An Operational Semantics and a Visualizer for Clarifying React Hooks
- Reasoning about External Calls
- RestPi: Path-Sensitive Type Inference for REST APIs
- Revamping Verilog Semantics for Foundational Verification
- Revealing Sources of (Memory) Errors via Backward Analysis
- SPLAT: A Framework for Optimised GPU Code-Generation for SParse reguLar ATtention
- SafeRace: Assessing and Addressing WebGPU Memory Safety in the Presence of Data Races
- SafeTree: Expressive Tree Policies for Microservices
- Scalable Equivalence Checking and Verification of Shallow Quantum Circuits
- Scalable and Accurate Application-Level Crash-Consistency Testing via Representative Testing
- Scaling Instruction-Selection Verification against Authoritative ISA Semantics
- Scaling Optimization over Uncertainty via Compilation
- Semantics of Sets of Programs
- Shaking Up Quantum Simulators with Fuzzing and Rigour
- Show Me Why It's Correct: Saving 1/3 of Debugging Time in Program Repair with Interactive Runtime Comparison
- Software Model Checking via Summary-Guided Search
- Sound and Modular Activity Analysis for Automatic Differentiation in MLIR
- Soundness of Predictive Concurrency Analyses
- Static Inference of Regular Grammars for Ad Hoc Parsers
- Statically Analyzing the Dataflow of R Programs
- Stencil-Lifting: Hierarchical Recursive Lifting System for Extracting Summary of Stencil Kernel in Legacy Codes
- Structural Abstraction and Refinement for Probabilistic Programs
- Structural Information Flow: A Fresh Look at Types for Non-interference
- Structural Temporal Logic for Mechanized Program Verification
- Symbolic MRD: Dynamic Memory, Undefined Behaviour, and Extrinsic Choice
- Synchronized Behavior Checking: A Method for Finding Missed Compiler Optimizations
- Syntactic Completions with Material Obligations
- Synthesizing DSLs for Few-Shot Learning
- Synthesizing Implication Lemmas for Interactive Theorem Proving
- Synthesizing Sound and Precise Abstract Transformers for Nonlinear Hyperbolic PDE Solvers
- Tabby: A Synthesis-Aided Compiler for High-Performance Zero-Knowledge Proof Circuits
- TailTracer: Continuous Tail Tracing for Production Use
- The Continuous Tensor Abstraction: Where Indices Are Real
- The Power of Regular Constraint Propagation
- The Simple Essence of Monomorphization
- The Simple Essence of Overloading: Making Ad-Hoc Polymorphism More Algebraic with Flow-Based Variational Type-Checking
- The Simulation Semantics of Synthesisable Verilog
- Towards Verifying Crash Consistency
- Towards a Theoretically-Backed and Practical Framework for Selective Object-Sensitive Pointer Analysis
- TraceLinking Implementations with Their Verified Designs
- Tracing Just-in-Time Compilation for Effects and Handlers
- Translation Validation for LLVM's AArch64 Backend
- Tuning Random Generators: Property-Based Testing as Probabilistic Programming
- Tunneling through the Hill: Multi-way Intersection for Version-Space Algebras in Program Synthesis
- Two Approaches to Fast Bytecode Frontend for Static Analysis
- Type-Outference with Label-Listeners: Foundations for Decidable Type-Consistency for Nominal Object-Oriented Generics
- Type-Preserving Flat Closure Optimization
- UTFix: Change Aware Unit Test Repairing using LLM
- Understanding and Improving Flaky Test Classification
- Universal Scalability in Declarative Program Analysis (with Choice-Based Combination Pruning)
- Unveiling Heisenbugs with Diversified Execution
- Validating SMT Rewriters via Rewrite Space Exploration Supported by Generative Equality Saturation
- Validating Soundness and Completeness in Pattern-Match Coverage Analyzers
- Verification of Bit-Flip Attacks against Quantized Neural Networks
- Verifying Asynchronous Hyperproperties in Reactive Systems
- We've Got You Covered: Type-Guided Repair of Incomplete Input Generators
- What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures
- Work Packets: A New Abstraction for GC Software Engineering, Optimization, and Innovation
- Zero-Overhead Lexical Effect Handlers
- im2im: Automatically Converting In-Memory Image Representations using a Knowledge Graph Approach
- qblaze: An Efficient and Scalable Sparse Quantum Simulator