A Formal Framework to Measure the Incompleteness of Abstract Interpretations
In program analysis by abstract interpretation, backward-completeness represents no loss of precision between the result of the analysis and the abstraction of the concrete execution, while forward-completeness stands for no imprecision between the concretization of the analysis result and the concrete execution. Program analyzers satisfying one of the two properties (or both) are considered precise. Regrettably, as for all approximation methods, the presence of false-alarms is most of the time unavoidable and therefore we need to deal somehow with incompleteness of both. To this end, a new property called partial completeness has recently been formalized as a relaxation of backward-completeness allowing a limited amount of imprecision measured by quasi-metrics. However, the use of quasi-metrics enforces distance functions to adhere precisely the abstract domain ordering, thus not suitable to be used to weaken the forward-completeness property which considers also abstract domains that are not necessarily based on Galois Connections. In this paper, we formalize a weaker form of quasi-metric, called pre-metric, which can be defined on all domains equipped with a pre-order relation. 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, according to the information and the corresponding level of approximation that we want to measure. Finally, by exploiting pre-metrics as our imprecision meter, we introduce the partial forward/backward-completeness properties.
Sun 22 OctDisplayed time zone: Lisbon change
11:00 - 12:30 | Domain precisionSAS 2023 at Room I Chair(s): Bor-Yuh Evan Chang University of Colorado at Boulder; Amazon | ||
11:00 30mTalk | How fitting is your abstract domain? SAS 2023 Roberto Giacobazzi University of Arizona, Isabella Mastroeni University of Verona, Italy, Elia Perantoni University of Verona Pre-print | ||
11:30 30mTalk | Domain Precision in Galois Connection-less Abstract Interpretation SAS 2023 Pre-print | ||
12:00 30mTalk | A Formal Framework to Measure the Incompleteness of Abstract Interpretations SAS 2023 Marco Campion INRIA & École Normale Supérieure | Université PSL, Caterina Urban Inria & École Normale Supérieure | Université PSL, Mila Dalla Preda University of Verona, Roberto Giacobazzi University of Arizona Pre-print |