Compiling with Abstract Interpretation
summary
Turns abstract interpreters into compilers by representing domain interfaces as free algebra domains and encoding small compilation passes as domain functors whose soundness and completeness equate to forward and backward simulation. Includes an SSA translation via a non‑standard SSA signature so an SSA-based non-relational domain is strictly more precise than a standard non‑relational domain for similar time/memory, recovers precision on low‑level code, implements an OCaml library, shows ~5–10% precision gains with 2×–20× runtime overhead.
AI-written summary · about
chapters (11)
- 0:00Compiling with abstract interpretation
- 1:04Analysis vs program transformations
- 2:30Abstract interpretation basics
- 4:16Free algebra domains
- 6:21Domain functors for compilation
- 9:22Soundness in functor transformations
- 11:50Compilation to SSA with functors
- 13:57Precision gains from SSA
- 14:39OCamel implementation
- 15:23Limitations and future work
- 15:44Q&A
related talks
09mRetargeting an Abstract Interpreter for a New Language by Partial Evaluation (Short Paper)
46mMechanizing Abstract Interpretation
24mThe Best of Abstract Interpretations
26mSSA Translation Is an Abstract Interpretation
30mAnalyzing Programs with SMT Solvers
27mTaming Unsoundness with Gradual Abstract Interpretation
25mNice to Meet You: Synthesizing Practical MLIR Abstract Transformers
20mCertified Abstract Machines for Skeletal Semantics