Abstract Interpretation - Examples of Abstract Domains

Examples of Abstract Domains

One can assign to each variable x available at a given program point an interval . A state assigning the value v(x) to variable x will be a concretization of these intervals if for all x, v(x) is in . From the intervals and for variables x and y, one can easily obtain intervals for x+y and for x−y ; note that these are exact abstractions, since the set of possible outcomes for, say, x+y, is precisely the interval . More complex formulas can be derived for multiplication, division, etc., yielding so-called interval arithmetics.

Let us now consider the following very simple program:

With reasonable arithmetic types, the result for z should be zero. But if we do interval arithmetic starting from x in, one gets z in . While each of the operations taken individually was exactly abstracted, their composition isn't.

The problem is evident: we did not keep track of the equality relationship between x and y; actually, this domain of intervals does not take into account any relationships between variables, and is thus a non-relational domain. Non-relational domains tend to be fast and simple to implement, but imprecise.

Some examples of relational numerical abstract domains are:

• congruence relations on integers
• convex polyhedra – with some high computational costs
• "octagons"
• difference-bound matrices
• linear equalities

and combinations thereof.

When one chooses an abstract domain, one typically has to strike a balance between keeping fine-grained relationships, and high computational costs.