Domain theory in abstract interpretation: equations, completeness and logic

Abstract. The aim of this thesis is to develop a methodology for systematically building abstract domains in the theory of abstract interpretation. Abstract interpretation is a general theory for describing non-standard semantics, (approximated) static analysis and, more generally, the behaviour of any discrete dynamic system at different levels of abstraction. Many interesting properties of abstract interpretation (e.g. concerning the precision of abstract computations) uniquely depend on the choice of the abstract domain. Central in the construction of an abstract interpretation is therefore the notion of abstract domain. When computing in an abstract domain, we deal with approximated objects and approximated computations. As a consequence, the result of an abstract computation is an approximation of the corresponding concrete one. In most cases, an approximation error is introduced and it may well happen that the abstract result is different from the concrete one, even if the abstract domain is sufficiently expressive to represent it. In other words, the expressivity of abstract domains does not reflect the precision of abstract computations.

The idea of this thesis arises from the observation that we can describe the precision degree of an abstract domain by a suitable generalization of the standard notion of completeness. Roughly speaking, a complete abstract interpretation turns out to be as precise as possible, relatively to its underlying abstract domains where approximated computations are encoded. In other words, abstract computations in complete abstract domains are as precise as the concrete ones. Therefore, completeness becomes the language by which we survey the relative precision of abstract domains in computing a given function. A completeness problem describes a relation between concrete and abstract computations, in such a way to bound approximation errors. Thus, completeness problems represent a compact and elegant language to describe the precision degree of the abstract domain we are interested in. Once we have expressed the desired precision level in terms of a completeness problem, we need a method to solve such a problem. The idea is to associate with each completeness problem a system of (possibly recursive) abstract domain equations in such a way that the solutions to the abstract domain equations satisfy the completeness problem. Intuitively, an abstract domain equation is some equation of kind X = F(X), where X is the abstract domain we look for and F is a monotone function transforming abstract domains. Abstract domain equations can then be solved iteratively by looking for the least fixpoint, since F is a monotone function. The way to move from completeness problems to domain equations is therefore the main point of this construction. For each completeness problem, we provide a constructive method to build the abstract domains which are solutions of a given problem. As a remarkable point of our result, we provide explicit, constructive characterizations of such domains. Finally, we address the problem of representing the objects in complete abstract domains. To this end, we supply a natural way to represent the abstract objects, by resorting to suitable fragments of (propositional) classic, intuitionistic and linear logic.