A Logic for the Imprecision of Abstract Interpretations
summary
Introduces a program logic, Error Propagation Logic, that produces an explicit bounding function mapping concrete-input imprecision to an upper bound on abstract-analysis error, and a separate omega-continuity calculus that composes moduli of continuity across sequence, join and iteration. Works with interval, hyperrectangle and octagon domains using counting or volume distances; join bounds must be proved per domain; widening explodes error so experiments use threshold widening. Proves partial local completeness when the derived bound holds; example: absolute-value composition yields bounds like 2t and an area bound of 52.
AI-written summary · about
chapters (7)
- 0:00Abstract interpretation basics
- 3:19Omega continuity definition
- 6:29Inductive omega continuity
- 11:43Error propagation logic
- 16:39Bounding imprecision rules
- 20:11Sequential composition example
- 22:21Conclusion & Q&A
related talks
24mThe Best of Abstract Interpretations
21mRelating Distances and Abstractions: An Abstract Interpretation Perspective
19mSynthesizing Backward Error Bounds, Backward
16mGradual Exact Logic: Unifying Hoare Logic and Incorrectness Logic via Gradual Verification
27mTaming Unsoundness with Gradual Abstract Interpretation
20mAbstract Interpretation with Confidence
17mCalculational design of Incorrectness Separation Logic
15mPartial Incorrectness Logic