A Formal Framework to Measure the Incompleteness of Abstract Interpretations

on YouTube ↗22m

" summary

Defines a weaker distance notion called pre-metric that relaxes quasi-metric axioms so distances work on pre-ordered abstract and concrete domains, shows how to derive distances via concretization or abstraction, and introduces epsilon partial forward/backward-completeness. Uses Interpr with octagons and polyhedra and measures imprecision as extra volume (boxes approximation) finding octagons ≈33% larger than polyhedra and polyhedra ≈20% larger than concrete so polyhedra is 20% partial forward-complete while octagons fail; results are worked out manually, not implemented.

AI-written summary · about

" chapters (11)

1. 0:00Introduction
2. 0:23Abstract interpretations background
3. 1:49Completeness vs incompleteness
4. 3:55Partial backward completeness
5. 5:41Quasimetric distances limits
6. 8:15Premetric distances introduced
7. 11:28Domain distance derivation
8. 12:52Revised completeness properties
9. 13:56Static analysis example
10. 17:52Premetric axioms importance
11. 19:16Q&A