Mechanizing Abstract Interpretation
summary
Mechanizes abstract interpretation using Coq and produces an executable analyzer extracted to OCaml; 30,000 lines of Coq implement Verasco with interval, congruence, octagon and polyhedra domains (polyhedra via certificate checking). The project proves soundness but not termination, uses gamma-only domains (no computable alpha), needs manual loop unrolling in places, and runs up to ~1 minute for 100 lines of C—works as a verified proof-of-concept but has scalability and calculational-style limitations.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 3:14Motivations for mechanization
- 7:11Historical formalization attempts
- 10:20Verasco project overview
- 18:27Verasco results and limits
- 21:16Mechanization challenges
- 23:05Galois connections in mechanization
- 27:43Computability and proof limits
- 28:45Constructive Galois connections
- 33:40Plan U: computations vs proofs
- 37:31Future directions
- 40:20Q&A
related talks
18mCompiling with Abstract Interpretation
26mStatically Resolvable Ambiguity
20mCertified Abstract Machines for Skeletal Semantics
27mTaming Unsoundness with Gradual Abstract Interpretation
15mCompiling with Continuations, Correctly
16mUntangling Mechanized Proofs
19mProgressful Interpreters for Efficient WebAssembly Mechanisation
20mInteractive Abstract Interpretation with Demanded Summarization