Abstract Domains for Universal and Existential Properties

Abstract Domains for Universal and Existential Properties

Abstract

For both compiler optimisation and program debugging, we need a knowledge of the expected behaviour of the program, preferably, before execution. The theory of abstract interpretation (AI) has successfully been used for constructing provably correct algorithms that can analyse the program code and determine its run-time properties. Central to this is the notion of an abstract domain describing certain program properties. For any program property, the abstract domain (which is a lattice) has to be a compromise between many factors including the precision and cost of the analysis. Thus, an important line of research in AI is the design of abstract domains for capturing specific concrete properties of the program. Recently, there have been several proposals for constructing new abstract domains from existing ones and, in this talk, I will describe one particular technique illustrating the ideas and results with examples taken from logic programming.