Towards computing distances among abstract interpretations
Ignacio Casso San Roman · 2018
Abstract interpretation is a technique which safely approximates the execution of programs. These aproximations can then be used by static analysis tools to reason about properties that hold for all possible executions, in order to optimize, verify or debug programs, among other applications. Different abstractions, called abstract domains, and analysis algorithms, computing the fixpoints involved in different ways, are used in this process, resulting in different aproximations, all of which are correct but may have different precision. This use of abstract interpretations is purely qualitative: it relies on an order ⊑ in the abstract domains and the fact that one abstract interpretation over-aproximates or underaproximates the actual (or some given) semantics of programs. A quantitative use of abstract interpretations is not covered by the existing theory, that is, there is no way to measure how close two abstract interpretations are to each other, even when one overaproximates the other. However, the structure of abstract domains and (logic) programs suggests that one could define distances and metrics among those abstract domains and abstract interpretations, and those distances could arguably find many applications, such as comparing the precision of different analyses. In this work we develop theory and tools to work with abstract interpretations quantitatively, in the context of the Ciao and CiaoPP environment. First, we develop a theory for distances in abstract domains and propose distances for CiaoPP domains. Later, we extend those distances to distances between whole analyses of programs. Finally, we apply successfully those distances in experiments to measure the precision of different analyses.