next up previous
Next: Distributed Computing/Coordination. Up: Related Work Previous: Language-Based Security.

Abstract Interpretation.

Abstract Interpretation is a theory for formally constructing conservative approximations of the semantics of programming languages. In practice, it is used for constructing semantics-based analysis algorithms for the automatic, static and conservative determination of dynamic properties of infinite-state programs [36,30].

The classical framework for abstract interpretation was introduced by Cousot [36,35,37]. In this framework a non-standard (approximate) program semantics is obtained from the standard (or concrete) one by replacing the actual (concrete) domain of computation and its basic (concrete) semantic operations with, respectively, an abstract domain and corresponding abstract semantic operations. The approximate, or abstract, semantics is usually related to the concrete one by a correctness relation; different formulations use Galois connections, logical relations or representation functions to define the correctness relation. The general idea is that the abstract semantics can be used to extract properties of the program statically. This is not always possible because abstract domains may still be infinite and, even if not, fixed point iterations may take too long to stabilise; the rich theory of abstract interpretation includes the notion of widening operators which may be used to accelerate convergence to a safe answer in these cases. Abstract interpretation is in a tradition of using non-standard semantics for analysis purposes which dates back to [53], where it was called pseudo-evaluation. Similar ideas were developed in [56] and [63]. This approach, under the name ``data flow analysis'', was used later on for compiler optimisation [44,52].

A quantitative approach to static analysis will be realised by the introduction of quantities such as probabilities in the framework of abstract interpretation. The extended framework can be used, for example, for performance analysis tasks, e.g. to automatically derive some sound statistical properties of the behaviour of the computer/program; this could be used for instance to establish an upper bound on the probability of failure. Initial work in this direction is on probabilistic abstract interpretation [22,21]. Related to this is the use of classical abstract interpretation for the analysis of probabilistic programs [50,51].


next up previous
Next: Distributed Computing/Coordination. Up: Related Work Previous: Language-Based Security.
Igor Siveroni 2004-08-12