Relating Distances and Abstractions: An Abstract Interpretation Perspective
summary
Formalizes when a pre-metric induces an upper closure operator (uco) via Galois connections, showing uco-representable prematrices form a strict subset and giving the construction: force symmetry on zero distances, close under transitivity to get equivalence classes, pick least upper-bound representatives, then enforce monotonicity and idempotence. Introduces a composed semantic/quantitative approximation and a confidentiality property Partial Abstract Non-Interference, proves an ε proof implies ε Partial Completeness of the best abstract semantics, and the converse yields 2·ε.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 0:43Program behavior challenges
- 2:29Quantitative vs qualitative
- 3:52Pre-metrics properties
- 4:55Upper closure operators
- 6:58Pre-metrics to operators
- 9:46Operator properties
- 10:48Combining distances
- 12:13Non-inference application
- 14:41Partial completeness
- 17:08Conclusion
- 18:17Q&A
related talks
24mThe Best of Abstract Interpretations
25mA Logic for the Imprecision of Abstract Interpretations
15mStable Relations and Abstract Interpretation of Higher-Order Programs
18mCompiling with Abstract Interpretation
26mObservational Equality: Now for Good
14mAdequacy for Algebraic Effects Revisited
26mProperty-Directed Reachability as Abstract Interpretation in the Monotone Theory
20mAbstract Interpretation with Confidence