How fitting is your abstract domain?
summary
Presents a sound, language- and domain-agnostic proof system that decides whether an abstract domain can produce answers strictly better than a chosen threshold, formalizing adequacy as a representability property distinct from completeness. Gives an algorithmic refinement loop (input/output iterations) that adds concrete-derived abstract elements to reach adequacy, shows the pattern on the sign and interval domains with worked examples and a small prototype implementation, and notes termination is not guaranteed.
AI-written summary · about
chapters (19)
- 0:00Introduction
- 0:23Abstract interpretation soundness
- 1:27Completeness and false alarms
- 3:14Completeness vs expressiveness
- 4:21Notion of adequacy
- 6:07Global and local adequacy
- 7:34Completeness vs adequacy
- 8:17Refining domains for adequacy
- 10:43Input/output refinement
- 13:58Iterative refinement to fixed point
- 14:21Program logic for adequacy
- 17:54Adequacy as quality measure
- 18:37Intentional nature of adequacy
- 19:19Transforming programs for adequacy
- 20:02Q&A
- 20:44Widening techniques comparison
- 21:27Domains vs transformers
- 22:50Termination guarantees
- 24:14Automation and future work