Abstract Local Completeness: A Local form of Abstract Non-Interference
summary
Defines abstract local completeness as an intermediate between global completeness and per-input local completeness, formalizes it as completeness over all concrete inputs sharing one abstract value, and proves equivalence relationships on the sign-domain examples (e.g., f(x) = (x+1)^2) showing concrete counterexamples and satisfying cases. Presents a sound but incomplete proof system with rules for assignments, guards, sequence, join and iteration, a blind predicate for outputs, and a domain simplification fixed‑point construction to enforce the property.
AI-written summary · about
chapters (6)
- 0:00Local completeness basics
- 10:38Sign domain example
- 15:18Local abstract completeness defined
- 18:32Proof system for local completeness
- 24:37Applications and future work
- 26:43Q&A on proof rules
related talks
23mSeparating the Wheat from the Chaff: Understanding (In-)Completeness of Proof(…)
36mThe Abstract Method, In General
52mThink Abstractly, Work Concretely
20mOn Multi-Language Abstraction: Towards a Static Analysis of Multi-Language Programs
15mIncremental Certified Programming
34mAbstract Interpretation, Software Model Checking, and Beyond - A Celebration of the(…)
25mUniversal Composability is Secure Compilation
13mData Abstraction: A General Framework to Handle Program Verification of Data Structures