Read our audit of AI-generated memory-safety proofs, which examines the guarantees behind Anthropic and Theorem’s verification results.
Latest
- A Type System for Communication-Safe Hardware Design
- Approximate Counting for Symbolic Automata
- Validating Concurrent Correctness Witnesses by Thread-Modular Abstract Interpretation
- Instrumentation Optimization for Practical Dynamic Race Detection
- Dynamic Race Detection with O(1) Samples
- Fixed Parameter Tractable Linearizability Monitoring
- State Space Estimation for DPOR-based Model Checkers
- Anvil: A General-Purpose Timing-Safe Hardware Description Language
- Counting and Sampling Traces in Regular Languages
- The Complexity of Testing Message-Passing Concurrency
- Efficient Decrease-And-Conquer Linearizability Monitoring
- Efficient Timestamping for Sampling-Based Race Detection
- Program Skeletons for Automated Program Translation
- Selectively Uniform Concurrency Testing
- The Decision Problem for Regular First-Order Theories
- Greybox Fuzzing for Concurrency Testing
- Predictive Monitoring with Strong Trace Prefixes
- A faster FPRAS for #NFA
- Optimistic Prediction of Synchronization-Reversal Data Races
- Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic
- Coarser Equivalences for Causal Concurrency
- How Hard Is Weak-Memory Testing?
- Predictive Monitoring against Pattern Regular Languages
- Dynamic Race Detection with O(1) Samples
- Optimal Reads-From Consistency Checking for C11-Style Memory Models
- Sound Dynamic Deadlock Prediction in Linear Time
- A Tree Clock Data Structure for Causal Orderings in Concurrent Executions
- Controller Synthesis for Linear System With Reach-Avoid Specifications
- Checking LTL[F,G,X] on Compressed Traces in Polynomial Time
- Dynamic Data-Race Detection through the Fine-Grained Lens
- Optimal Prediction of Synchronization-Preserving Races
- Scalable Statistical Root Cause Analysis on App Telemetry
- Atomicity Checking in Linear Time using Vector Clocks
- Decidable Synthesis of Programs with Uninterpreted Functions
- Deciding Memory Safety for Single-Pass Heap-Manipulating Programs
- Exact Quantitative Probabilistic Model Checking Through Rational Search
- The Complexity of Dynamic Data Race Prediction
- What's Decidable About Program Verification Modulo Axioms?
- Decidable Verification of Uninterpreted Programs
- A Decidable Fragment of Second Order Logic With Applications to Synthesis
- Controller Synthesis Made Real: Reach-Avoid Specifications and Linear Dynamics
- Data Race Detection on Compressed Traces
- What Happens-After the First Race? Enhancing the Predictive Power of Happens-Before Based Dynamic Race Detection
- Dynamic Race Prediction in Linear Time
- Exact Quantitative Probabilistic Model Checking Through Rational Search
- Look for the Proof to Find the Program: Decorated-Component-Based Program Synthesis
- Computing Information Flow Using Symbolic Model-Checking
- Weak Singular Hybrid Automata