SAS 2023
Sun 22 - Tue 24 October 2023 Cascais, Portugal
co-located with SPLASH 2023
Sun 22 Oct 2023 12:00 - 12:30 at Room I - Domain precision Chair(s): Bor-Yuh Evan Chang

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 Oct

Displayed 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
30m
Talk
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
30m
Talk
Domain Precision in Galois Connection-less Abstract Interpretation
SAS 2023
Isabella Mastroeni University of Verona, Italy, Michele Pasqua University of Verona
Pre-print
12:00
30m
Talk
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