Taming Unsoundness with Gradual Abstract Interpretation
summary
Proposes that optimistic but unsound assumptions in abstract interpretation become safe by automatically inserting runtime checks so analysis results are sound w.r.t. an elaborated program. Implements proof‑of‑concept gradual sign and interval analyses and a check‑insertion pass using the Study platform. Shows that removing dead branches is valid only when checks guarantee assumed invariants at runtime, and reports successful prototype behavior while flagging open issues: runtime overhead unknown and need for real‑world annotations and case studies.
AI-written summary · about
chapters (7)
- 0:00Gradual abstract interpretation intro
- 1:03Static analysis and abstract interpretation
- 7:47Unsoundness in program analysis
- 11:15Gradual abstract interpretation concept
- 14:50Implementation and progress
- 18:23Summary and future work
- 19:05Q&A
related talks
18mCompiling with Abstract Interpretation
46mMechanizing Abstract Interpretation
09mRetargeting an Abstract Interpreter for a New Language by Partial Evaluation (Short Paper)
18mDeveloping a Dependently Typed Language with Runtime Proof Search
20mInteractive Abstract Interpretation with Demanded Summarization
19mGradual Correctness: a Dynamically Bidirectional Full-Spectrum Dependent Type Theory
20mAbstract Interpretation with Confidence
15mAbstract Interpretation of Temporal Safety Effects of Higher Order Programs