Abstract Interpretation Repair
summary
This work gives an algorithmic way to repair abstract interpreters by add one point u into the abstract domain along a program trace, producing the minimal refinement that restores precision for that input. It supplies forward and backward repair strategies, proves optimality for Galois-connection-style domains, shows that partitioning reconstruction yields CEGAR-like behavior, and enables running a cheap domain globally while invoking an expensive, precise domain only on the traced refinement points.
AI-written summary · about
chapters (7)
- 0:00Introduction to abstraction
- 0:38The problem of precision
- 2:36Limitations of completeness
- 6:18Local completeness strategy
- 9:11Non-compositionality issues
- 11:39Application of the repair
- 14:03Q&A and technical discussion
related talks
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...
30mAutomatic Inference of Relational Object Invariants
34mAbstract Interpretation, Software Model Checking, and Beyond - A Celebration of the(…)
36mThe Abstract Method, In General
15mAbstract Interpretation of Temporal Safety Effects of Higher Order Programs
52mThink Abstractly, Work Concretely
27mAn Abstract Domain for Heap Commutativity
24mU-Turn: Enhancing Incorrectness Analysis by Reversing Direction