Interactive Abstract Interpretation with Demanded Summarization
summary
Presents demanded summarization, an algorithm and engine that makes summary‑based abstract interpretation incremental and compositional while supporting arbitrary abstract domains and guaranteeing from-scratch consistency. Implements a hierarchy of per‑procedure DIGs and a DSG that records summary uses, handles recursion with self‑referential summary queries, and embeds widening in the engine. Prototype on octagons runs 2500 synthetic edits and Bugstorm Java fixes, cuts recomputed states to 0.1–2.7% of batch and improves tail latency (notably P99), showing the approach is practical.
AI-written summary · about
chapters (12)
- 0:00Interactive static analysis intro
- 1:05Need for interactive analysis
- 2:27Demanded abstract interpretation
- 5:16Interprocedural analysis extension
- 6:00Demand and summarization
- 8:51Summarization graph structure
- 10:16Recursion with self-summaries
- 11:40Formal interactive summary analysis
- 13:07Responsiveness after edits
- 14:50Reduction in recomputation
- 16:15Conclusion
- 16:37Q&A on widening
related talks
46mMechanizing Abstract Interpretation
27mTaming Unsoundness with Gradual Abstract Interpretation
24mThe Best of Abstract Interpretations
20mOptimal Program Synthesis via Abstract Interpretation
09mRetargeting an Abstract Interpreter for a New Language by Partial Evaluation (Short Paper)
21mSynthesizing Formal Semantics from Executable Interpreters
25mCall-Guarded Abstract Definitional Interpreters
14mOne Down, 699 to Go: or, synthesising compositional desugarings