Abstract Interpretation with Confidence
summary
Paper defines alarm confidence as the probability of local completeness: the chance that a sampled concrete program, drawn from the set consistent with a given abstract-analysis execution, makes the analyzer locally complete. It gives a constructive method — an oracle denotational semantics and a tractable under‑approximation ⟨⟨·⟩⟩ and ⟨⟨·⟩⟩^{lc} — proves both correct, encodes per‑command distributions and correlations, handles loops by correlated sampling plus unrolling, and reports no empirical evaluation yet.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 1:30Motivation for statistical analysis
- 3:40Confidence in abstract interpretation
- 8:17Computing confidence locally
- 12:11Practical semantics for confidence
- 16:05Loops and correlations handling
- 17:52Conclusion
- 18:12Q&A
related talks
24mThe Best of Abstract Interpretations
25mCall-Guarded Abstract Definitional Interpreters
27mTaming Unsoundness with Gradual Abstract Interpretation
18mCompiling with Abstract Interpretation
30mRelatively Complete Verification of Probabilistic Programs
25mA Logic for the Imprecision of Abstract Interpretations
46mMechanizing Abstract Interpretation
20mInteractive Abstract Interpretation with Demanded Summarization