Domain Precision in Galois Connection-Less Abstract Interpretation

The ever growing pervasiveness of software systems in modern days technology results in an increasing need of \emph{software/program correctness proofs}. The latter, allow developers to spot software failures before production, hence preventing potentially catastrophic repercussions on our society, as in the case of safety-critical infrastructures. Unfortunately, correctness proofs may fail (even when software is actually correct) due to program analysis imprecision: program analysis sacrifices precision in order to gain decidability. In standard abstract interpretation-based static analyses, such imprecision is ``measured'' in terms of \emph{completeness} of the chosen observation (i.e., of the chosen abstract domain) w.r.t. the programming language semantics. In this setting, fixed the language language, it is crucial to have decidable techniques to determine whether the chosen abstraction is sufficiently precise to analyze the program under consideration. In this paper, we characterize abstract domain precision from a novel point of view, providing a formal framework for \emph{characterizing} and (statically) \emph{verifying} abstract domain precision, that can be adopted also in the case of ``weakened'', i.e., Galois Connection-less, static analysis frameworks. Distinctive examples adopting such frameworks are the Convex Polyhedra and Automata domains, for which standard approaches to reason about analysis precision (i.e., completeness) cannot be applied.