Comparison of abstract interpretations

Abstract

The central idea of the technique of Abstract Interpretation is that the analysis of a program consists of executing it on a special (abstract) domain D of values in which each operation µ, used during the normal execution, is interpreted as a corresponding operation µD on D. More formally, an (abstract) domain is a complete lattice that enjoys a Galois insertion into the concrete domain. An interpretation consists of a domain and a collection of monotone operations over that domain. Due to the success of the technique, several interpretations with similar purposes have been proposed. In the classical theory of abstract interpretation, the only way we have to compare two interpretations is to show that one abstracts the other. The weakness of this type of comparison is that it does not allow us to compare various interpretations with respect to some, but not all, of the information they express. This paper presents new notions that enable us to make such precise comparisons. These notions are applicable to the comparison of abstract interpretations for all kinds of programming languages and with all sorts of analysis frameworks. We show that our new notions form a natural extension to the existing notion of one interpretation abstracting another. We demonstrate the utility of our technique by using it to compare abstract interpretations for analysis of logic programs with respect to their ability to infer variable groundness.