The Best of Abstract Interpretations
summary
Characterizes when an inductive abstract interpretation equals the abstraction of the concrete semantics, proves that for any non‑trivial abstract domain the set of programs with that best correct approximation is not recursive, and shows there is no effective program transformation or minimal domain refinement that guarantees achieving it. Uses the sign domain example (+1 then −1) to demonstrate non‑compositionality, excludes widening, and gives a program logic that infers [pre]A p [post]A triples certifying that an analysis is indeed the best.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 2:12Program syntax and semantics
- 5:04Best code approximation
- 7:09Research questions on best analysis
- 9:17Structural properties of programs
- 13:15Impossibility results
- 15:02Defining BCA triples
- 18:56Proving best analysis
- 22:07Future work and conclusion
related talks
18mCompiling with Abstract Interpretation
21mRelating Distances and Abstractions: An Abstract Interpretation Perspective
25mA Logic for the Imprecision of Abstract Interpretations
20mAbstract Interpretation with Confidence
20mOptimal Program Synthesis via Abstract Interpretation
27mTaming Unsoundness with Gradual Abstract Interpretation
20mInteractive Abstract Interpretation with Demanded Summarization
26mProperty-Directed Reachability as Abstract Interpretation in the Monotone Theory