Partial (In)Completeness in Abstract Interpretation: Limiting the Imprecision in
summary
Defines a quasi-metric a-compatible on abstract domains (examples: weighted path length for sign and interval domains) and formalizes epsilon-partial completeness meaning at most epsilon distance from the concrete result, i.e., a bounded number of false alarms. Proves nontrivial domains admit programs with unbounded imprecision, shows membership in the epsilon-complete class is decidable when the domain satisfies a chain condition (algorithm via dovetailed concrete runs) but undecidable in general, and gives a Hoare-style proof system that composes and sums epsilon error bounds.
AI-written summary · about