Grids: A Domain for Analyzing the Distribution of Numerical Values^{⋆}

Roberto Bagnara^{1}, Katy Dobson^{2}, Patricia M. Hill^{2}, Matthew Mundell^{2}, and Enea Zaffanella^{1}

1 Department of Mathematics, University of Parma, Italy,

                     {bagnara,zaffanella}@cs.unipr.it

2 School of Computing, University of Leeds, UK,

                   {katyd,hill,mattm}@comp.leeds.ac.uk

Abstract. This paper explores the abstract domain of grids, a domain that is able to represent sets of equally spaced points and hyperplanes over an n-dimensional vector space. Such a domain is useful for the static analysis of the patterns of distribution of the values program variables can take. We present the domain, its representation and the basic operations on grids necessary to define the abstract semantics. We show how the definition of the domain and its operations exploit well-known techniques from linear algebra as well as a dual representation that allows, among other things, for a concise and efficient implementation.

1 Introduction

We distinguish between two kinds of numerical information about the values program variables can take: outer limits (or bounds within which the values must lie) and the pattern of distribution of these values. Both kinds of information have important applications: in the field of automatic program verification, limit information is crucial to ensure that array accesses are within bounds, while distribution information is what is required to ensure that external memory accesses obey the alignment restriction imposed by the host architecture. In the field of program optimization, limit information can be used to compile out various kinds of run-time tests, whereas distribution information enables several transformations for efficient parallel execution as well as optimizations that enhance cache behavior.

Both limit and distribution information often come in a relational form; for instance, the outer limits or the pattern of possible values of one variable may depend on the values of one or more other variables. Domains that can capture relational information are generally much more complex than domains that do not have this capability; in exchange they usually offer significantly more precision, often important for the overall performance of the client application. Relational

⋆ This work has been partly supported by EPSRC project EP/C520726/1 “Numerical Domains for Software Analysis,” by MIUR project “AIDA — Abstract Interpretation: Design and Applications,” and by a Royal Society (ESEP) award.

-4 -2 4 2 -2 -4  6 4 2

(a) The grid L

-4 -2 4 2 -2 -4  6 4 2

(b) The grid L′

Fig. 1. Congruence and generator systems representing two grids in ℝ^{2}

limit information can be captured, among other possibilities, by means of polyhedral domains, that is, domains that represent regions of some n-dimensional vector space bounded by a finite set of hyperplanes [10]. Although polyhedral domains such as the domain of convex polyhedra have been thoroughly researched and are widely used, relational domains for representing the (linear) distribution of numerical values have been less well researched. Moreover, as far as we know and at the time of writing, there is no available implementation providing all the basic operations needed by a relational abstract domain for distribution information. This is in spite of the fact that previous research has shown that a knowledge about the (discrete) distribution of numerical information, especially when combined with that of the limit information, can significantly improve the quality of the analysis results [1].

This paper closes this gap by providing a complete account of the relational domain of grids; a domain for capturing numerical distribution information. It includes a detailed survey of previous work in this area; gives two representations for the domain; outlines how these can be reduced and also how to convert between them; and shows how this double description directly supports methods for comparing, joining and intersecting elements of this domain. The paper also outlines affine image and preimage operations and two new widenings for grids.

Grids in a Nutshell. Figure 1 illustrates two ways of describing a grid; either by means of a finite set of congruence relations that all grid points must satisfy (given by dashed lines) or by means of a finite set of generating vectors used for constructing the grid points and lines (given by filled squares and thick lines).

The squares in Figure 1(a) illustrate a grid L indicating possible values of integer variables x and y resulting from executing the program fragment in Figure 2 for any value of m. The congruence relations x = 0 (mod 2) and x + 2y = 2 (mod 4) are represented by the vertical dashed lines and sloping lines, respectively. The set of congruence relations C = {x = 0 (mod 2), x + 2y = 2 (mod 4)}, called a congruence system, is said to describe L. The filled squares mark the points p_{1} = ( \begin{matrix}2 \\ 0 \end{matrix} ) , p_{2} = ( \begin{matrix}6 \\ 0 \end{matrix} ) and p_{3} = ( \begin{matrix}4 \\ 1 \end{matrix} ) while all the squares (both filled and unfilled) mark points v = π_{1}p_{1} + π_{2}p_{2} + π_{3}p_{3}, where π_{1}, π_{2}, π_{3} ∈ ℤ and π_{1} + π_{2} + π_{3} = 1. The set of points P = {p_{1}, p_{2}, p_{3}} is said to generate L. Some of these generating points can be replaced by parameters that give the gradient and distance between neighboring points. Specifically, by subtracting the point p_{1} from each of the other two generating points p_{2} and p_{3}, we obtain the parameters q_{2} = ( \begin{matrix}4 \\ 0 \end{matrix} ) and q_{3} = ( \begin{matrix}2 \\ 1 \end{matrix} ) for L that are marked by the thick lines between points p_{1} and p_{2} and points p_{1} and p_{3}, respectively. It follows that each point v ∈ L can be written as v = p_{1} + π_{2}q_{2} + π_{3}q_{3} for some π_{2}, π_{3} ∈ ℤ.

The dashed line in Figure 1(b) illustrates

                                            x := 2; y := 0;  (P1)
                                            for i := 1 to m  (P2)
                                              if ... then
                                                x := x + 4   (P3)
                                              else
                                                x := x + 2;
                                                y := y + 1   (P4)
                                              endif          (P5)
                                            endfor

Fig. 2. Fragment based on an example in [10] the grid L′ defining the line x = y + 1 and marks the vectors of values of the real variables x and y after an assignment x := y + 1, assuming that nothing is known about the value of y. As equalities are congruences modulo 0, the set C′ = {x − y = 1} is also called a congruence system and describes L′. Observe that the grid L′ consists of all points that can be obtained as λℓ + p′, for any λ ∈ ℝ, where ℓ = ( \begin{matrix}1 \\ 1 \end{matrix} ) and p′ = ( \begin{matrix}1 \\ 0 \end{matrix} ) ; the vector ℓ, called a line, defines a gradient and the vector p′ is a generating point marking a position for the line (illustrated in Figure 1(b) by the thick line and the filled square, respectively).

From what we have just seen, any grid can be represented both by a congruence system and by a generator system. The latter may consist of three components: a set of lines, a set of parameters and a set of points. For instance, the triples G_{1} = (∅, ∅, P ) and G_{2} = (∅, {q_{2}, q_{3}}, {p_{1}}) are both generator systems for L while the triple G′ = ({ℓ}, ∅, {p′}) is a generator system for L′.

Contributions. The paper provides an account of the relational domain of grids, fully implemented within the Parma Polyhedra Library [2, 4]. In this section we provide the first comprehensive survey of the main research threads concerning these and similar domains. The other contributions are given below.

Minimizing representations. Assuming the grid is represented by a congruence and generator system in an n-dimensional vector space consisting of m congruences or generators, then we outline algorithms for minimizing the representation (based on the Hermite normal form algorithm [29]) that have worst-case complexity O(n^{2}m). Note that previous proposals for minimization such as those in [14, 23] have worse complexity bounds (see below).

Converting representations. The congruence and generator representations described informally above form the two components of a double description method for the grid domain very similar to that for convex polyhedra [20]. For a double description method, conversion algorithms between the two systems are needed; we show how conversion can be implemented using any matrix inversion algorithm, inheriting the corresponding worst-case complexity. For instance, the complexity is O(n^{3}) when adopting the standard Gaussian elimination method; since matrix inversion has the same worst-case complexity as matrix multiplication, better theoretical complexity bounds apply [5]. Previous proposals for congruence to generator conversion have complexity no better than O(n^{4}) [15].

Grid operations. For static analysis, it is useful to provide all the set-theoretic lattice operations for grids (assuming the usual subset ordering) such as comparison, join and meet. We show that these operations are straightforward given the availability of the appropriate representation(s) in minimal form; and hence show that some have complexities strictly better than that of previous proposals [14]. We also describe a grid difference operator which is new to this paper.

Affine transformation operators. Affine image and preimage operators can be used to capture the effect of assignment statements in a program when the expression is linear although, as noted by Müller-Olm and Seidl in [21], analyses that use affine spaces for approximating the semantics of procedures are not sufficiently precise to detect all valid affine relations for programs with procedures. Here we specify, for the domain of grids, the affine image and preimage operators for a single update where only one dimension is modified.

Widenings. It was observed by Granger [15], that, if the grid generators can be in the rationals, then the grid domain does not satisfy the ascending chain condition; so, to guarantee termination of the analysis, a widening operation is required. In [15, Proposition 10], a widening is given for non-relational grids that returns a line parallel to an axis whenever the modulus for that dimension changes. It is then proposed that a generalized form of this could be used as a widening for relational grids; however, exactly how this is to be done is unclear. In this paper, we define two possible generalizations which come with simple syntactic checks that have efficient implementations.

Related Work. In [12], Granger shows how a static analysis can usefully employ a simple non-relational grid domain (that is a grid described by congruences of the form x = c (mod f) where c and f are integers) and that this domain can obtain more precise information for applications such as automatic vectorization. Larsen et al. [17] also developed a static analyzer over a non-relational grid domain specifically designed to detect when dynamic memory addresses are congruent with respect to a given modulus; they show that, this information helps in the construction of a comprehensive set of program transformations for saving energy on low-power architectures and improving performance on multimedia processors. We note that these applications should carry over to the more complex domain considered here. In addition, Miné has shown how to construct, from the non-relational congruence domain in [12], a zone-congruence domain (that is, a domain that only allows weakly relational congruences that have the form x − y = a (mod b) where a and b are rationals) [19].

Concerning fully relational domains, note that the use of a domain of linear equality relations for program analysis had already been studied by Karr [16].

In [14], Granger generalized this to provide a domain of linear congruence relations on an integral domain, i.e., a domain generated by integral vectors in n-dimensions; and then, in [13, 15], generalizes the results to the full grid domain. In [13–15], domain elements are represented by congruence and generator systems similar to the ones defined here. Standard algorithms for solving linear equations are used in converting from generator to congruence systems; however, a more complex O(n^{4}) algorithm is provided for converting from congruence to generator systems. Assuming the number of generators is n + 1, the algorithm for minimizing the generator system has complexity O(n^{3} log_{2} n). Operators for comparing grids and computing the greatest lower and least upper bounds are also described. In particular, the join operation defined in [14] has complexity O(n^{4} log_{2} n), since the generators of one grid are added, one at a time, to the generators of the other; after each addition the minimization algorithm is applied to compute a new linearly independent set. The grid meet operation which also minimizes the addition of one congruence at a time has complexity O(n^{4}).

The problem of how best to apply the grid domain in a program analyzer, has been studied by Müller-Olm and Seidl in [23] also building on the work of Karr [16]. Here, the prime focus is for the design of an interprocedural analysis for programs containing assignment statements and procedure calls. The algorithm has three stages: first, for each program point, a matrix M containing a (minimized) set of generators (i.e., vectors of values that hold at that point) is found; secondly, the determinant f of M is computed; thirdly, a congruence system with modulo f that satisfies all the vectors in M is determined. Stage one is similar to that proposed by Granger [14] for minimizing a set of generators. Stages two and three differ from the conversion in [14] in that the modulus f is computed separately and used to reduce the sizes of the coordinates. Note that the framework described in [23] subsumes previous works by the same authors.

Following an independent stream of research, Ancourt [1] considered the domain of ℤ-polyhedra; that is a domain of integral lattices intersected with the domain of convex polyhedra (see also [24–26]). We are primarily interested here in the “integral lattices” component which may be seen as a subdomain of the domain of grids where the grid is full dimensional and all the grid points are integral vectors. The representation of these integral lattices is a special case of our generator representation where, for n dimensions, there must be exactly one point and n linearly independent parameters, all of which must be integral. There is no support for a congruence representation.

All the operations on ℤ-polyhedra (and therefore the lattices) require canonic representations; hence Quinton et al. [25, 26] define a canonical form for these lattices with a method for its computation. We note that the algorithm for computing the canonic form has complexity O(n^{4}), where n is the number of dimensions of the vector space. Other operations provided are those of lattice intersection, affine image and affine preimage. As there is no congruence representation, the intersection of two lattices is computed directly from the generator representations [1]; a refined version of this method is provided in [25] which we note that, as for computing the canonic form, has complexity O(n^{4}). The operations of grid join and grid difference (as defined here) are not considered; instead the union operator takes two lattices L_{1} and L_{2} and returns the set {L_{1}, L_{2}} unless one (say L_{1}) is contained in the other, in which case they return the larger, L_{2}. Similarly the difference operation returns a set of lattices representing the set difference L_{1} \ L_{2}. The domain of integral lattices has been implemented in PolyLib [18] following the approach in [25, 26]. This means that only the generator representation is supported and some operations return sets of lattices while others manipulate and simplify these sets.

The homogeneous form of a representation given in Section 4, is required by the conversion algorithm. This form is not new to this paper; in fact several researchers have observed this. For instance, Granger [14] describes a map from a linear congruence system in n variables to a homogeneous one in n + 1 variables; Nookala and Risset [24] explain that the PolyLib [18] adds a dimension to make the (generator) representation homogeneous; while Müller-Olm and Seidl [23] consider extended states where vectors have an extra 0’th component.

Plan of the Paper. Preliminary concepts and notation are given in Section 2. Section 3 introduces a grid together with its congruence and generator representations while Section 4 provides the main algorithms needed to support the double description. Section 5 introduces grid widening and the paper concludes in Section 6. A long version of the paper containing all proofs is available at

http://www.comp.leeds.ac.uk/hill/Papers/papers.html.

2 Preliminaries

The cardinality of a set S is denoted by # S. The set of integers is denoted by ℤ, rationals by ℚ and reals by ℝ. The complexities will assume a unit cost for every arithmetic operation.

Matrices and Vectors. If H is a matrix in ℝ^{n×m}, the transposition of H is denoted by H^{T} ∈ ℝ^{m×n}. A vector v = (v_{1}, …, v_{n}) ∈ ℝ^{n} is also regarded as a matrix in ℝ^{n×1}. The scalar product of vectors v and w ∈ ℝ^{n}, denoted by ⟨v, w⟩, is the real number v^{T}w = ∑_{i=1}^{n} v_{i}w_{i}. The vector e_{i} ∈ ℝ^{n} has 1 in the i-th position and 0 in every other position. We let

piv_{<}(v) := \begin{cases}0 & if v = 0 \\ max\{i | 1 ≤ i ≤ n, v_{i} ≠ 0\} & if v ≠ 0 \end{cases}

piv_{>}(v) := \begin{cases}n + 1 & if v = 0 \\ min\{i | 1 ≤ i ≤ n, v_{i} ≠ 0\} & if v ≠ 0. \end{cases}

We write v ⇑ v′, if piv_{<}(v) = piv_{<}(v′) = k and either k = 0 or v_{k} = v′_{k} and v ⇓ v′, if piv_{>}(v) = piv_{>}(v′) = k and either k = n + 1 or v_{k} = v′_{k}.

Integer Combinations. The set S = {v_{1}, …, v_{k}} ⊆ ℝ^{n} is affinely independent if, for all λ ∈ ℝ^{k}, λ = 0 is the only solution of {∑_{i=1}^{k} λ_{i}v_{i} = 0, ∑_{i=1}^{k} λ_{i} = 0}. For all λ ∈ ℝ^{k}, the vector v = ∑_{j=1}^{k} λ_{j}v_{j} is said to be a linear combination of S. This combination is affine, if ∑_{j=1}^{k} λ_{j} = 1; and integral, if λ ∈ ℤ^{k}. The set of all linear (resp., affine, integral, integral and affine) combinations of S is denoted by linear.hull (resp., affine.hull(S), int.hull(S), int.affine.hull(S)).

Congruences and Congruence Relations. For any a, b, f ∈ ℝ, a ≡_{f} b denotes the congruence ∃μ ∈ ℤ . a − b = μf. Let 𝕊 ∈ {ℚ, ℝ}. For each vector a ∈ 𝕊^{n} and scalars b, f ∈ 𝕊, the notation ⟨a, x⟩ ≡_{f} b stands for the linear congruence relation in 𝕊^{n} defined by the set { v ∈ ℝ^{n} | ∃μ ∈ ℤ . ⟨a, v⟩ = b+μf }; when f ≠ 0, the relation is said to be proper; ⟨a, x⟩ ≡_{0} b denotes the equality ⟨a, x⟩ = b. Thus, provided a ≠ 0, the relation ⟨a, x⟩ ≡_{f} b defines the set of affine hyperplanes { (⟨a, x⟩ = b + μf) | μ ∈ ℤ }; when a = 0, we assume that b ≠ 0; if b ≡_{f} 0, ⟨0, x⟩ ≡_{f} b defines the universe ℝ^{n} and the empty set, otherwise.

Any vector that satisfies ⟨a, x⟩ = b + μf for some μ ∈ ℤ is said to satisfy the relation ⟨a, x⟩ ≡_{f} b. Congruence relations in 𝕊^{n}, such as ⟨a, x⟩ ≡_{1} b and ⟨2a, x⟩ ≡_{2} 2b, defining the same hyperplanes are considered equivalent.

The pivot notation for vectors is extended to congruences: if β = (⟨a, x⟩ ≡_{f} a_{0}) then piv_{<}(β) := piv_{<}(a); if γ = (⟨c, x⟩ ≡_{g} c_{0}) and ga ⇑ fc, then we write β ⇑ γ; so that β and γ are either both equalities or both proper congruences.

3 The Grid Domain

Here we introduce grids and their representation. Note that the use of the word ‘grid’ here is to avoid confusion with the meaning of ‘lattice’ (used previously for elements similar to a grid) in its set-theoretic context (particularly relevant when working in abstract interpretation).

Grids and the Congruence Representation. A congruence system in ℚ^{n} is a finite set of congruence relations C in ℚ^{n}. As we do not distinguish between syntactically different congruences defining the same set of vectors, we can assume that all proper congruences in C have modulus 1.

Definition 1. Let C be a congruence system in ℝ^{n}. If L is the set of vectors in ℝ^{n} that satisfy all the congruences in C, we say that L is a grid described by a congruence system C in ℚ^{n}. We also say that C is a congruence system for L and write L = gcon(C). If gcon(C) = ∅, then we say that C is inconsistent.

The grid domain 𝔾_{n} is the set of all grids in ℝ^{n} ordered by the set inclusion relation, so that ∅ and ℝ^{n} are the bottom and top elements of 𝔾_{n} respectively.

The vector space ℝ^{n} is called the universe grid. In set theoretical terms, 𝔾_{n} is a lattice under set inclusion. Many algorithms given here will require the congruence systems not only to have minimal cardinality but also such that the coefficients of (a permutation of) the congruences can form a triangular matrix.

Definition 2. Suppose C is a congruence system in ℚ^{n}. Then we say that C is in minimal form if either C = {⟨0, x⟩ ≡_{0} 1} or C is consistent and, for each congruence β = (⟨a, x⟩ ≡_{f} b) ∈ C, the following hold:

1. if piv_{<}(β) = k, then k > 0 and a_{k} > 0;

2. for all β′ ∈ C \ {β}, piv_{<}(β′) ≠ piv_{<}(β).

Proposition 1. Let C be a congruence system in ℚ^{n} and m = # C. Then there exists an algorithm for finding a congruence system C′ in minimal form with worst-case complexity O(n^{2}m) such that gcon(C) = gcon(C′).

Note that the algorithm mentioned in Proposition 1, is based on the Hermite normal form algorithm; details about the actual algorithm are given in the proof. Note also, that when m < n, the complexity of this algorithm is just O(m^{2}n).

The Generator Representation. Let L be a grid in 𝔾_{n}. Then

– a vector p ∈ L is called a point of L;

– a vector q ∈ ℝ^{n} \ {0} is called a parameter of L if L ≠ ∅ and p + μq ∈ L, for all points p ∈ L and all μ ∈ ℤ;

– a vector ℓ ∈ ℝ^{n} \ {0} is called a line of L if L ≠ ∅ and p + λℓ ∈ L, for all points p ∈ L and all λ ∈ ℝ.

If L, Q and P are finite sets of vecors in ℝ^{n} and

L := linear.hull(L) + int.hull(Q) + int.affine.hull(P)

where the symbol ‘+’ denotes the Minkowski’s sum,^{3} then L ∈ 𝔾_{n} is a grid (see [29, Section 4.4] and also Proposition 7). The 3-tuple (L, Q, P), where L, Q and P denote sets of lines, parameters and points, respectively, is said to be a generator system in ℚ^{n} for L and we write L = ggen((L, Q, P)). Note that, for any grid L in 𝔾_{n}, there is a generator system (L, Q, P) in ℚ^{n} for L (see again [29, Section 4.4] and also Proposition 6). Note also that the grid L = ggen((L, Q, P)) = ∅ if and only if the set of points P = ∅. If P ≠ ∅, then L = ggen((L, ∅, Q_{p} ∪ P)) where, for some p ∈ P, Q_{p} = { p + q ∈ ℝ^{n} | q ∈ Q }.

As for congruence systems, for many procedures in the implementation, it is useful if the generator systems have a minimal number of elements. Definition 3. Suppose G = (L, Q, P) is a generator system in ℚ^{n}. Then we say that G is in minimal form if either L = Q = P = ∅ or # P = 1 and, for each generator v ∈ L ∪ Q, the following hold:

1. if piv_{>}(v) = k, then v_{k} > 0;

2. for all v′ ∈ (L ∪ Q) \ {v}, piv_{>}(v′) ≠ piv_{>}(v).

Proposition 2. Let G = (L, Q, P) be a generator system in ℚ^{n} and m = # L + # Q + # P. Then there exists an algorithm for finding a generator system G′ in minimal form with worst-case complexity O(n^{2}m) such that ggen(G′) = ggen(G).

As for Proposition 1, the algorithm mentioned in Proposition 2 is based on the Hermite normal form algorithm. Note also that, when m < n, the complexity of this algorithm is again just O(m^{2}n).

3 This is defined, for each S, T ⊆ ℝ^{n}, by S + T := { s + t ∈ ℝ^{n} | s ∈ S, t ∈ T }.

Double Description. We have shown that any grid L can be described by using a congruence system C and also generated by a generator system G. For the same reasons as for the polyhedral domain, it is useful to represent the grid L by the double description (C, G). Just as for the double description method for convex polyhedra, in order to maintain and exploit such a view of a grid, an implementation must include algorithms for converting a representation of one kind into a representation of the other kind and for minimizing both representations. Note that having easy access to both representations is assumed in the implementation of many grid operators including those described here.

Suppose we have a double description (C, G) of a grid L ∈ 𝔾_{n}, where both C and G are in minimal form. Then, it follows from the definition of minimal form that # C ≤ n + 1 and # L + # Q ≤ n. In fact, we have a stronger result. Proposition 3. Let (C, G) be a double description where both C and G are in minimal form. Letting C = E ∪F, where E and F are sets of equalities and proper congruences, respectively, and G = (L, Q, P), then # F = # Q = n − # L − # E.

Example 1. Consider the grids L and L′ in Figure 1. The congruence systems C and C′ are in minimal form and the generator systems G_{2} and G′ are also in minimal form; however, G_{1} is not in minimal form as it contains more than one point. Furthermore, for i = 1, 2, the pairs (C, G_{i}) are double descriptions for L while (C′, G′) is a double description for L′.

Comparing Grids. For any pair of grids L_{1} = ggen((L, Q, P)), L_{2} = gcon(C) in 𝔾_{n}, we can decide whether L_{1} ⊆ L_{2} by checking if every generator in (L, Q, P) satisfies every congruence in C. Note that a parameter or line v satisfies a congruence ⟨a, x⟩ ≡_{f} b if ⟨a, v⟩ ≡_{f} 0. Therefore, assuming the systems C and G are already in minimal form, the complexity of comparison is O(n^{3}).

Given that it is known that one grid is a subset of another, there are quicker tests for checking equality - the following definition is used in their specification.

Definition 4. Let C_{1}, C_{2} be congruence systems in minimal form. Then C_{1}, C_{2} are said to be pivot equivalent if, for each i, j ∈ {1, 2} where i ≠ j, for each β ∈ C_{i}, there exists γ ∈ C_{j} such that β ⇑ γ.

Let G_{1} = (L_{1}, Q_{1}, {p_{1}}) and G_{2} = (L_{2}, Q_{2}, {p_{2}}) be generator systems in minimal form. Then G_{1}, G_{2} are said to be pivot equivalent if, for each i, j ∈ {1, 2} where i ≠ j: for each q_{i} ∈ Q_{i}, there exists q_{j} ∈ Q_{j} such that q_{i} ⇓ q_{j}; and, for each ℓ_{i} ∈ L_{i}, there exists ℓ_{j} ∈ L_{j} such that piv_{>}(ℓ_{i}) = piv_{>}(ℓ_{j}).

Proposition 4. Let L_{1} = gcon(C_{1}) = ggen(G_{1}) and L_{2} = gcon(C_{2}) = ggen(G_{2}) be non-empty grids in 𝔾_{n} such that L_{1} ⊆ L_{2}. If C_{1} and C_{2} are pivot equivalent congruence systems in minimal form or G_{1} and G_{2} are pivot equivalent generator systems in minimal form, then L_{1} = L_{2}.

It follows from Proposition 4, that provided L_{1} ⊆ L_{2} and L_{1} and L_{2} have both their generator or congruence systems already in minimal form, then the complexity of checking if L_{1} = L_{2} is just O(n). Moreover, if it is found that one pair of corresponding pivot elements of the congruence or generator systems differ, then we can immediately deduce that the grids they describe also differ.

Intersection and Grid Join. For grids L_{1}, L_{2} ∈ 𝔾_{n}, the intersection of L_{1} and L_{2}, defined as the set intersection L_{1} ∩L_{2}, is the largest grid included in both L_{1} and L_{2}; similarly, the grid join of L_{1} and L_{2}, denoted by L_{1} ⊕ L_{2}, is the smallest grid that includes both L_{1} and L_{2}. In theoretical terms, the intersection and grid join operators are the binary meet and join operators on the lattice 𝔾_{n}. They can easily be computed; if L_{1} = gcon(C_{1}) = ggen(G_{1}) and L_{2} = gcon(C_{2}) = ggen(G_{2}), then L_{1} ∩ L_{2} = gcon(C_{1} ∪ C_{2}) and L_{1} ⊕ L_{2} = ggen(G_{1} ∪ G_{2}).

In practice, the cost of computing the grid intersection and join depends on a number of factors: if generator systems G_{1} and G_{2} for L_{1} and L_{2} are known, then the complexity of computing L_{1} ⊕ L_{2} is linear in either # G_{1} or # G_{2}; if, however, only congruence systems C_{1} and C_{2} for L_{1} and L_{2} (not necessarily in minimal form) are known, then the complexity is that of minimizing and converting them which is, at worst, O(n^{2} max(# C_{1}, # C_{2}, n)). A similar argument applies to the complexities of the meet operation. However, the above operations are not directly comparable with the meet and join operations given in [14]. For such a comparison, for instance for the join operation, we assume that generator systems for L_{1} and L_{2} in minimal form are available (i.e., each with at most n + 1 generators) and the operation returns a generator system in minimal form for L_{1} ⊕ L_{2}. Then the complexity is O(n^{3}), the complexity of minimizing a generator system with at most 2n + 2 generators, which is strictly better than O(n^{4} log_{2} n), the complexity of the equivalent operation in [14].

Example 2. Consider the grids L_{1} = gcon(C_{1}) and L_{2} = gcon(C_{2}) in 𝔾_{2} where C_{1} := {x ≡_{2} 0, −x + y ≡_{3} 0} and C_{2} := {x ≡_{4} 0, −x + 2y ≡_{6} 0}. Then the grid intersection is L_{1} ∩ L_{2} = gcon(C_{1} ∪ C_{2}); thus, as C = {x ≡_{12} 0, y ≡_{3} 0} is a reduced form of C_{1} ∪ C_{2}, we have L_{1} ∩ L_{2} = gcon(C).

Consider L_{1} = ggen((∅, ∅, P_{1})) and L_{2} = ggen((∅, ∅, P_{2})) in 𝔾_{2}, where P_{1} := ( \begin{matrix}2 & 0 & 0 \\ 2 & 3 & 0 \end{matrix} ) and P_{2} := ( \begin{matrix}4 & 0 & 0 \\ 2 & 3 & 0 \end{matrix} ) . Then the grid join L_{1} ⊕ L_{2} is generated by (∅, ∅, P_{1}∪P_{2}); thus, the generator system G := (∅, ( \begin{matrix}2 & 0 \\ 0 & 1 \end{matrix} ) , ( \begin{matrix}0 \\ 0 \end{matrix} )) is a minimal form of (∅, ∅, P_{1} ∪ P_{2}) and L_{1} ⊕ L_{2} = ggen(G). Note that here L_{1} ⊕ L_{2} ≠ L_{1} ∪ L_{2}.

Grid Difference. For grids L_{1}, L_{2} ∈ 𝔾_{n}, the grid difference L_{1} ⊖ L_{2} of L_{1} and L_{2} is the smallest grid containing the set-theoretic difference of L_{1} and L_{2}.

Proposition 5. The grid L_{1} ⊖ L_{2} is returned by the algorithm in Figure 3.

Assuming C_{1} and C_{2} are available and in minimal form, it follows from the complexities of minimization, conversion and comparison operations that the grid difference algorithm in Figure 3 has worst-case complexity O(n^{4}).

Affine Images and Preimages. Affine transformations for the vector space ℝ^{n} will map hyperplanes to hyperplanes and preserve intersection properties between hyperplanes; such transformations can be represented by matrices in ℝ^{n×n}. It follows that the set 𝔾_{n} is closed under the set of all affine transformations for ℝ^{n}. Simple and useful linear affine transformations for numerical

Input: Nonempty grids L_{1} = gcon(C_{1}) and L_{2} = gcon(C_{2}) in 𝔾_{n}. Output: A grid in 𝔾_{n}.

(1) L′ := ∅

(2) while ∃β = (e ≡_{f} 0) ∈ C_{2}

(3) C_{2} := C_{2} \ {β}

(4) if L_{1} ⊈ gcon({β})

(5) if L_{1} ⊆ gcon({2e ≡_{f} 0})

(6) L_{β} := gcon(C_{1} ∪ {2e − f ≡_{2f} 0})

(7) L′ := L′ ⊕ L_{β}

(8) else

(9) return L_{1}

(10) return L′

Fig. 3. The grid difference algorithm

domains, including the grids, are provided by the ‘single update’ affine image and affine preimage operators.

Given a grid L ∈ 𝔾_{n}, a variable x_{k} and linear expression e = ⟨a, x⟩ + b with coefficients in ℚ, the affine image operator ϕ(L, x_{k}, e) maps the grid L to

{ (p_{1}, …, p_{k−1}, ⟨a, p⟩ + b, p_{k+1}, …, p_{n})^{T} ∈ ℝ^{n} | p ∈ L }.

Conversely, the affine preimage operator ϕ^{−1}(L, x_{k}, e) maps the grid L to

{ p ∈ ℝ^{n} | (p_{1}, …, p_{k−1}, ⟨a, p⟩ + b, p_{k+1}, …, p_{n})^{T} ∈ L }.

Observe that the affine image ϕ(L, x_{k}, e) and preimage ϕ^{−1}(L, x_{k}, e) are invertible if and only if the coefficient a_{k} in the vector a is non-zero.

Program Analysis Using Grids. We show how the grid domain can be used to find properties of the program variables not found using the polyhedra domain [10], constraint-based analysis [28] or polynomial invariants [27].

Example 3. The program fragment in Figure 2 is annotated with program points Pj, for j = 1, …, 5. Let L_{j}^{i} ∈ 𝔾_{2} denote the grid computed at the i-th iteration executed by the point Pj. Initially, L_{j}^{0} = ∅ = gcon({1 = 0}), for j = 1, …, 5. After one and two iterations of the loop we have:

L_{1}^{1} = gcon({x = 2, y = 0}), L_{2}^{1} = gcon({x = 2, y = 0}),
L_{3}^{1} = gcon({x = 6, y = 0}), L_{4}^{1} = gcon({x = 4, y = 1}),
L_{5}^{1} = gcon({x = 4, y = 1}) ⊕ gcon({x = 6, y = 0})
= gcon({x + 2y = 6, x ≡_{2} 0}),
L_{2}^{2} = gcon({x = 2, y = 0}) ⊕ gcon({x + 2y = 6, x ≡_{2} 0})
= gcon({x + 2y ≡_{4} 2, x ≡_{2} 0}).

Subsequent computation steps show that an invariant for P2 has already been computed since L_{3}^{2} = L_{3}^{1}, L_{4}^{2} = L_{4}^{1}, L_{5}^{2} = L_{5}^{1} so that L_{2}^{3} = L_{2}^{2}. Thus at the end of the program, the congruences x + 2y ≡_{4} 2 and x ≡_{2} 0 hold.

Observe that, using convex polyhedra, a similar analysis will find instead that the inequalities x − 2y ≥ 2, x + 2y ≥ 6 and y ≥ 0 hold [10].

4 Implementation

In this section, we describe convenient internal representations of the congruence and generator systems in terms of arrays (i.e., matrices) and show how matrix inversion provides a basis for converting between these representations.

Homogeneous Representations. A congruence system C is homogeneous if, for all (⟨a, x⟩ ≡_{f} b) ∈ C, we have b = 0. Similarly, a generator system (L, Q, P) is homogeneous if 0 ∈ P. For the implementation, it is convenient to work with a homogeneous system. Thus we first convert any congruence or generator system in ℚ^{n} to a homogeneous system in ℚ^{n+1}. The extra dimension is denoted with a 0 subscript; the vector x̂ = (x_{0}, …, x_{n})^{T}; and e_{0} denotes the vector (1, 0^{T})^{T}.

Consider the congruence system C = E ∪F in ℚ^{n}, where E is a set of equalities and F is a set of proper congruences. Then the homogeneous form for C is the congruence system Ĉ = Ê ∪ F̂ in ℚ^{n+1} defined by:

Ê:= { ⟨(−b, a^{T})^{T}, x̂⟩ = 0 | (⟨a, x⟩ = b) ∈ E },
F̂ := { ⟨f^{−1}(−b, a^{T})^{T}, x̂⟩ ≡_{1} 0 | (⟨a, x⟩ ≡_{f} b) ∈ F } ∪ {⟨e_{0}, x̂⟩ ≡_{1} 0}.

The congruence ⟨e_{0}, x̂⟩ ≡_{1} 0 expresses the fact that 1 ≡_{1} 0. By writing Ê = (E^{T}x = 0) and F̂ = (F^{T}x ≡_{1} 0), where E, F ⊆ ℚ^{n+1}, it can be seen that the pair (F, E), called the matrix form of Ĉ, is sufficient to determine C.

Consider next a generator system G = (L, Q, P) in ℚ^{n}. Then the homogeneous form for G is the generator system Ĝ:= (L̂, Q̂ ∪ P̂, {0}) in ℚ^{n+1} where

L̂ := {(0, ℓ^{T})^{T} | ℓ ∈ L}, Q̂ := {(0, q^{T})^{T} | q ∈ Q}, P̂ := {(1, p^{T})^{T} | p ∈ P }.

The original grid L = gcon(C) (resp., L = ggen(G)) can be recovered from the grid L̂ = gcon(Ĉ) (resp., L̂ = ggen(Ĝ)) since L = { v ∈ ℝ^{n} | (1, v^{T})^{T} ∈ L̂) }. Note that, if (C, G) is a double description for a grid and Ĉand Ĝ are homogeneous forms for C and G, then (Ĉ, Ĝ) is also a double description.

Converting Representations. By considering the matrix forms of the (homogeneous forms of the) representations, we can build the conversion algorithms on top of those for matrix inversion. For an informal explanation why this is appropriate, suppose that the generator system G = (∅, Q, {0}) in ℚ^{n} is in minimal form and Q is a non-singular square matrix. Letting L = ggen(G) = { Qπ | π ∈ ℤ^{n} }, then we also have L = { v ∈ ℝ^{n} | Q^{−1}v ≡_{1} 0 }, so that (Q^{−1}, ∅) is the matrix form of a congruence system for the same grid L. Similarly we can use matrix inversion to convert the matrix form of a homogeneous congruence system in minimal form consisting of n proper congruences for a grid L to a generator system for L. When the matrices to be inverted have less than n linearly independent columns, the algorithms first add vectors e_{i} where 1 ≤ i ≤ n, as necessary, so as to make the matrices non-singular and hence invertible.

Proposition 6. Let C be a congruence system in ℚ^{n} in minimal form; (F, E) the matrix form of the homogeneous form for C; N a matrix in ℤ^{n+1} whose vectors are of the form e_{i}, i ∈ {0, …, n}, and such that (N, F̂, Ê) is square and nonsingular; and (L̂, Q̂, M) := ((N, F̂, Ê)^{−1})^{T} where # L̂ = # N, # Q̂ = # F̂ and # M = # Ê. Then Ĝ = (L̂, Q̂, {0}) is the homogeneous form for a generator system G in minimal form and ggen(G) = gcon(C).

Proposition 7. Let G be a generator system in ℚ^{n} in minimal form; Ĝ = (L̂, Q̂, {0}) the homogeneous form for G; M a matrix in ℤ^{n+1} whose vectors are of the form e_{i}, i ∈ {0, …, n}, and such that (L̂, Q̂, M) is square and nonsingular; and (N, F̂, Ê) := ((L̂, Q̂, M)^{−1})^{T} where # N = # L̂, # F̂ = # Q̂ and # Ê = # M. Then (F̂, Ê) is the matrix form of the homogeneous form for a congruence system C in minimal form and gcon(C) = ggen(G).

Both algorithms just perform matrix inversion; so their complexity depends on the inversion algorithm adopted in the implementation. As far as we know, the current best theoretical worst-case complexity is O(n^{2.376}) [5]. Note that, in the current implementation in the PPL, the conversion algorithm is based on the Gaussian elimination method, which has complexity O(n^{3}).

5 Grid Widening

A simple and general characterization of a widening for enforcing and accelerating convergence of an upward iteration sequence is given in [6–9]. We assume here a minor variation of this classical definition (see footnote 6 in [9, p. 275]).

Definition 5. (Widening.) Let ⟨D, ⊢, 0, ⊕⟩ be a join-semilattice. The partial operator ∇: D × D ↣ D is a widening if

1. for each d_{1}, d_{2} ∈ D, d_{1} ⊢ d_{2} implies that d_{1} ∇ d_{2} is defined and d_{2} ⊢ d_{1} ∇ d_{2};

2. for each increasing chain d_{0} ⊢ d_{1} ⊢ ⋯, the increasing chain defined by d′_{0} := d_{0} and d′_{i+1} := d′_{i} ∇ (d′_{i} ⊕ d_{i+1}), for i ∈ ℕ, is not strictly increasing.

In addition to the formal requirements in Definition 5, it is also important to have a widening that has an efficient implementation, preferably, one that depends on a simple syntactic mapping of the representations. At the same time, so that the widening is well-defined, the result of this operation should be independent of the actual representation used. For this reason, the two widenings we propose assume specific minimal forms for the congruence and generator systems.

Definition 6. A congruence system C is in strong minimal form if, for each pair of distinct proper congruences, ⟨a, x⟩ ≡_{1} b and ⟨c, x⟩ ≡_{1} d in C, if piv_{<}(c) = k > 0, then −c_{k} < 2a_{k} ≤ c_{k}. A generator system G = ((L, Q, P)) in ℚ^{n} is in strong minimal form if G is in minimal form and, for each pair of distinct parameters u, v ∈ Q, if piv_{>}(v) = k ≤ n, then −v_{k} < 2u_{k} ≤ v_{k}.

Proposition 8. There exists an algorithm with complexity O(n^{3}) for converting a congruence system C (resp., generator system G) in minimal form to a congruence system C′ (resp., generator system G′) in strong minimal form such that gcon(C) = gcon(C′) (resp., ggen(G) = ggen(G′)).

The widenings defined below use either the congruence or the generator systems.

Definition 7. Let L_{1} = gcon(C_{1}) and L_{2} = gcon(C_{2}) be two grids in 𝔾_{n} such that L_{1} ⊆ L_{2}, C_{1} is in minimal form and C_{2} is in strong minimal form. Then the grid widening L_{1} ∇_{C} L_{2} is defined by

L_{1} ∇_{C} L_{2} := \begin{cases}L_{2}, & if L_{1} = ∅ or dim(L_{1}) < dim(L_{2}), \\ gcon(C_{S}), & otherwise, \end{cases}

where C_{S} := { γ ∈ C_{2} | ∃β ∈ C_{1} . β ⇑ γ }.

Definition 8. Let L_{1} = ggen(G_{1}) and L_{2} = ggen(G_{2}) be two grids in 𝔾_{n} such that L_{1} ⊆ L_{2}, G_{1} = (L_{1}, Q_{1}, P_{1}) is in minimal form and G_{2} = (L_{2}, Q_{2}, P_{2}) is in strong minimal form. Then the grid widening L_{1} ∇_{G} L_{2} is defined by

L_{1} ∇_{G} L_{2} := \begin{cases}L_{2}, & if L_{1} = ∅ or dim(L_{1}) < dim(L_{2}); \\ ggen(G_{S}), & otherwise, \end{cases}

where G_{S} := (L_{2} ∪ (Q_{2} \ Q_{S}), Q_{S}, P_{2}) and Q_{S} := { v ∈ Q_{2} | ∃u ∈ Q_{1} . u ⇓ v }.

Proposition 9. The operators ‘∇_{C}’ and ‘∇_{G}’ are both widenings on 𝔾_{n}.

In Definition 7, it is required that C_{2} is in strong minimal form. The following example shows that this is necessary for the operator ‘∇_{C}’ to be well-defined.

Example 4. Let L_{1} := gcon(C_{1}), L_{2} := gcon(C_{2}) and L′_{2} := gcon(C′_{2}) where C_{1} = {x ≡_{2} 0, y ≡_{2} 0}, C_{2} = {x ≡_{1} 0, x + y ≡_{2} 0}, C′_{2} = {x ≡_{1} 0, 3x + y ≡_{2} 0}; then L_{2} = L′_{2}. Note that only C_{1} and C_{2} are in strong minimal form. Therefore, assuming C_{S} (resp., C_{S}′) is defined as in Definition 7 using C_{1} and C_{2} (resp., C_{1} and C′_{2}), we have C_{S} = {x + y ≡_{2} 0} and C_{S}′ = {3x + y ≡_{2} 0}. Thus L_{1} ∇_{C} L_{2} = gcon(C_{S}) ≠ gcon(C_{S}′).

Example 5. To see that the widenings depend on the variable ordering, consider the grids L_{1} = gcon(C_{1}) = gcon(C′_{1}) and L_{2} = gcon(C_{2}) = gcon(C′_{2}) in 𝔾_{2}, where

C_{1} := {5x + y ≡_{1} 0, 22x ≡_{1} 0}, C_{2} := {5x + y ≡_{1} 0, 44x ≡_{1} 0},
C′_{1} := {9y + x ≡_{1} 0, 22y ≡_{1} 0}, C′_{2} := {9y + x ≡_{1} 0, 44y ≡_{1} 0}.

Assume for C_{1} and C_{2} that the variables are ordered so that x precedes y, as in the vector (x, y)^{T}; then, C_{1} and C_{2} are in strong minimal form and, according to Definition 7, we obtain L_{1} ∇_{C} L_{2} = gcon({5x + y ≡_{1} 0}). On the other hand, C′_{1} and C′_{2} are in strong minimal form when taking the variable order where y precedes x. In this case, by Definition 7, L_{1} ∇_{C} L_{2} = gcon({9y + x ≡_{1} 0}).

6 Conclusion

We have defined a domain of grids and shown that any element may be represented either by a congruence system which is a finite set of congruences (either equalities or proper congruences); or a generator system which is a triple of finite sets of vectors (denoting sets of lines, parameters and points). Assuming such a system in ℚ^{n} has m congruences or generators, then the minimization algorithms have worst-case complexity O(n^{2}m). It is shown that any matrix inversion algorithms such as Gaussian elimination which has complexity O(n^{3}), can be used for converting between generator and congruence systems in minimal form. Thus, the complexity of converting any system with m elements is no worse than O(n^{2}m) if m > n and O(n^{3}), otherwise.

The minimization and conversion algorithms, form the basis for a double description method for grids so that any generator or congruence systems, possibly in minimal form, can be provided on demand; the complexity of such a provision being as stated above. Assuming this method, we have shown that operations for comparison, intersection and grid join are straightforward. The complexity of comparing two grids is O(n^{3}) but, for just checking equality when it is already known that one of the grids is a subset of the other, we have described simpler procedures with complexity O(n). The intersection and grid join just take the union of the congruence or generator systems, respectively, so that, from a theoretical perspective, these have complexity O(n). However, in the implementation, we assume a common divisor for all the coordinates or coefficients in the system; hence, combining the systems requires changing the denominators of both components to their least common multiple with a consequential need to scale all the numerators in the representation; giving a worst-case complexity of O(n^{2}). We have also described an algorithm for computing the grid difference with complexity O(n^{4}). Observe that this operator is useful in the specification of the certificate-based widening for the grid powerset domain [3].

The grid domain is implemented in the PPL [2, 4] following the approach described in this paper. Among the tests available in the PPL are the examples in this paper and implementations of the running examples in [22, 23]. The PPL provides full support for lifting any domain to the powerset of that domain, so that a user of the PPL can experiment with powersets of grids and the extra precision this provides. An interesting line of research is the combination of the grids domain with the polyhedral domains provided by the PPL: not only the ℤ-polyhedra domain, but also many variations such as the grid-polyhedra, gridoctagon, grid-bounded-difference, grid-interval domains and their powersets.

References

1. C. Ancourt. Génération Automatique de Codes de Transfert pour Multiprocesseurs à Mémoires Locales. PhD thesis, Université de Paris VI, March 1991.

2. R. Bagnara, P. M. Hill, and E. Zaffanella. The Parma Polyhedra Library User’s Manual. Department of Mathematics, University of Parma, Parma, Italy, release 0.9 edition, March 2006. Available at http://www.cs.unipr.it/ppl/.

3. R. Bagnara, P. M. Hill, and E. Zaffanella. Widening operators for powerset domains. Software Tools for Technology Transfer, 8(4/5):449–466, 2006.

4. R. Bagnara, E. Ricci, E. Zaffanella, and P. M. Hill. Possibly not closed convex polyhedra and the Parma Polyhedra Library. In M. V. Hermenegildo and G. Puebla, editors, Static Analysis: Proceedings of the 9th International Symposium, volume 2477 of Lecture Notes in Computer Science, pages 213–229, Madrid, Spain, 2002. Springer-Verlag, Berlin.

5. D. Coppersmith and S. Winograd. Matrix multiplication via arithmetic progressions. Journal of Symbolic Computation, 9(3):251–280, 1990.

6. P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In B. Robinet, editor, Proceedings of the Second International Symposium on Programming, pages 106–130, Paris, France, 1976. Dunod, Paris, France.

7. P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the Fourth Annual ACM Symposium on Principles of Programming Languages, pages 238–252, New York, 1977. ACM Press.

8. P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2(4):511–547, 1992.

9. P. Cousot and R. Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In M. Bruynooghe and M. Wirsing, editors, Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming, volume 631 of Lecture Notes in Computer Science, pages 269–295, Leuven, Belgium, 1992. Springer-Verlag, Berlin.

10. P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, pages 84–96, Tucson, Arizona, 1978. ACM Press.

11. R. Giacobazzi, editor. Static Analysis: Proceedings of the 11th International Symposium, volume 3148 of Lecture Notes in Computer Science, Verona, Italy, 2004. Springer-Verlag, Berlin.

12. P. Granger. Static analysis of arithmetical congruences. International Journal of Computer Mathematics, 30:165–190, 1989.

13. P. Granger. Analyses Sémantiques de Congruence. PhD thesis, École Polytechnique, 921128 Palaiseau, France, July 1991.

14. P. Granger. Static analysis of linear congruence equalities among variables of a program. In Samson Abramsky and T. S. E. Maibaum, editors, TAPSOFT’91: Proceedings of the International Joint Conference on Theory and Practice of Software Development, Volume 1: Colloquium on Trees in Algebra and Programming (CAAP’91), volume 493 of Lecture Notes in Computer Science, pages 169–192, Brighton, UK, 1991. Springer-Verlag, Berlin.

15. P. Granger. Static analyses of congruence properties on rational numbers (extended abstract). In P. Van Hentenryck, editor, Static Analysis: Proceedings of the 4th International Symposium, volume 1302 of Lecture Notes in Computer Science, pages 278–292, Paris, France, 1997. Springer-Verlag, Berlin.

16. M. Karr. Affine relationships among variables of a program. Acta Informatica, 6:133–151, 1976.

17. S. Larsen, E. Witchel, and S. P. Amarasinghe. Increasing and detecting memory address congruence. In Proceedings of the 2002 International Conference on Parallel Architectures and Compilation Techniques (PACT’02), pages 18–29, Charlottesville, VA, USA, 2002. IEEE Computer Society Press.

18. V. Loechner. PolyLib: A library for manipulating parameterized polyhedra. Avail-

able at http://icps.u-strasbg.fr/^{∼}loechner/polylib/, March 1999. Declares

itself to be a continuation of [30].

19. A. Miné. A few graph-based relational numerical abstract domains. In M. V. Hermenegildo and G. Puebla, editors, Static Analysis: Proceedings of the 9th International Symposium, volume 2477 of Lecture Notes in Computer Science, pages 117–132, Madrid, Spain, 2002. Springer-Verlag, Berlin.

20. T. S. Motzkin, H. Raiffa, G. L. Thompson, and R. M. Thrall. The double description method. In H. W. Kuhn and A. W. Tucker, editors, Contributions to the Theory of Games – Volume II, number 28 in Annals of Mathematics Studies, pages 51–73. Princeton University Press, Princeton, New Jersey, 1953.

21. M. Müller-Olm and H. Seidl. Precise interprocedural analysis through linear algebra. In N. D. Jones and X. Leroy, editors, Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2004), pages 330–341, Venice, Italy, 2004. ACM Press.

22. M. Müller-Olm and H. Seidl. Analysis of modular arithmetic. In M. Sagiv, editor, Programming Languages and Systems, Proceedings of the 14th European Symposium on Programming, volume 3444 of Lecture Notes in Computer Science, pages 46–60, Edinburgh, UK, 2005. Springer-Verlag, Berlin.

23. M. Müller-Olm and H. Seidl. A generic framework for interprocedural analysis of numerical properties. In C. Hankin and I. Siveroni, editors, Static Analysis: Proceedings of the 12th International Symposium, volume 3672 of Lecture Notes in Computer Science, pages 235–250, London, UK, 2005. Springer-Verlag, Berlin.

24. S. P. K. Nookala and T. Risset. A library for Z-polyhedral operations. Publication interne 1330, IRISA, Campus de Beaulieu, Rennes, France, 2000.

25. P. Quinton, S. Rajopadhye, and T. Risset. On manipulating Z-polyhedra. Technical Report 1016, IRISA, Campus Universitaire de Bealieu, Rennes, France, July 1996.

26. P. Quinton, S. Rajopadhye, and T. Risset. On manipulating Z-polyhedra using a canonic representation. Parallel Processing Letters, 7(2):181–194, 1997.

27. E. Rodríguez-Carbonell and D. Kapur. An abstract interpretation approach for automatic generation of polynomial invariants. In Giacobazzi [11], pages 280–295.

28. S. Sankaranarayanan, H. Sipma, and Z. Manna. Constraint-based linear-relations analysis. In Giacobazzi [11], pages 53–68.

29. A. Schrijver. Theory of Linear and Integer Programming. Wiley Interscience Series in Discrete Mathematics and Optimization. John Wiley & Sons, 1999.

30. D. K. Wilde. A library for doing polyhedral operations. Master’s thesis, Oregon State University, Corvallis, Oregon, December 1993. Also published as IRISA Publication interne 785, Rennes, France, 1993.