A Formal Framework to Measure the Incompleteness of Abstract Interpretations

In program analysis by abstract interpretation, completeness represents the best possible scenario where no imprecision is generated by the abstract interpreter. However, as for all approximation methods, the presence of false-alarms is unavoidable and therefore we need to deal somehow with imprecision, i.e., incompleteness. To this end, the partial completeness property has been recently formalized in order to tolerate a limited amount of imprecision when the abstract and concrete domains are complete lattices and form a Galois Connection. Partial completeness measures the amount of imprecision by using quasi-metrics compatible with the underlying abstract domain. In this paper we generalize the partial completeness property by considering also abstractions that admit a concretization map only and are not necessarily complete lattices. This leads us to formalize a weaker form of quasi-metric, called premetric, which can be defined on all domains equipped with a pre-order relation. Pre-metrics allow us to design distance functions that well fit in the considered abstract interpretation, according to the information and the corresponding level of approximation that we want to measure. We show how this newly defined notion of pre-metric allows us to derive other pre-metrics on other domains by exploiting the concretization and, when available, the abstraction maps.