Precise Widening Operators for Convex Polyhedra ⋆

Roberto Bagnara^{a}, Patricia M. Hill^{b}, Elisa Ricci^{a}, Enea Zaffanella^{a}

aDepartment of Mathematics, University of Parma, Italy

bSchool of Computing, University of Leeds, UK

Abstract

In the context of static analysis via abstract interpretation, convex polyhedra constitute the most used abstract domain among those capturing numerical relational information. Since the domain of convex polyhedra admits infinite ascending chains, it has to be used in conjunction with appropriate mechanisms for enforcing and accelerating the convergence of fixpoint computations. Widening operators provide a simple and general characterization for such mechanisms. For the domain of convex polyhedra, the original widening operator proposed by Cousot and Halbwachs amply deserves the name of standard widening since most analysis and verification tools that employ convex polyhedra also employ that operator. Nonetheless, there is an unfulfilled demand for more precise widening operators. In this paper, after a formal introduction to the standard widening where we clarify some aspects that are often overlooked, we embark on the challenging task of improving on it. We present a framework for the systematic definition of new widening operators that are never less precise than a given widening. The framework is then instantiated on the domain of convex polyhedra so as to obtain a new widening operator that improves on the standard widening by combining several heuristics. A preliminary experimental evaluation has yielded promising results. We also suggest an improvement to the well-known widening delay technique that allows to gain precision while preserving its overall simplicity.

Key words: abstract interpretation, widening operators, convex polyhedra.

⋆ This work has been partly supported by MURST projects “Aggregate- and Number-Reasoning for Computing: from Decision Algorithms to Constraint Programming with Multisets, Sets, and Maps” and “Constraint Based Verification of Reactive Systems.”

Email addresses: bagnara@cs.unipr.it (Roberto Bagnara),

hill@comp.leeds.ac.uk (Patricia M. Hill), zaffanella@cs.unipr.it (Enea

Preprint submitted to Science of Computer Programming 8 January 2005

1 Introduction

An ability to reason about numerical quantities is crucial for an increasing number of applications in the field of automated analysis and verification of complex systems. Of particular interest are representations that capture relational information, that is, information relating different quantities such as, for example, the length of a buffer and the contents of a program variable, or the number of agents in different states in the modeling of a distributed protocol.

Convex polyhedra, since the work of Cousot and Halbwachs [1], constitute the most used abstract domain among those capturing numerical, relational information. They have been used to solve, by abstract interpretation [2], several important data-flow analysis problems such as array bound checking, compile-time overflow detection, loop invariant computations and loop induction variables. Convex polyhedra are also used, among many other applications, for the analysis and verification of synchronous languages [3,4] and of linear hybrid automata (an extension of finite-state machines that models time requirements) [5,6], for the computer-aided formal verification of concurrent and reactive systems based on temporal specifications [7], for inferring argument size relationships in logic languages [8,9], for the automatic parallelization of imperative programs [10], for detecting buffer overflows in C [11], and for the automatic generation of the ranking functions needed to prove progress properties [12].

Since the domain of convex polyhedra admits infinite ascending chains, it has to be used in conjunction with appropriate mechanisms for enforcing and accelerating the convergence of fixpoint computations. Widening operators [2,13–15] provide a simple and general characterization for such mechanisms. In its simplest form, a widening operator on a poset ⟨P, ⊑⟩ is defined as a partial function ∇: P × P ↣ P satisfying:

(1) for all x, y ∈ P, if x ∇ y is defined then x ⊑ x ∇ y and y ⊑ x ∇ y;

(2) for all increasing chains y_{0} ⊑ y_{1} ⊑ ⋯, if the increasing chain x_{0} := y_{0} and x_{i+1} := x_{i} ∇ y_{i+1} is defined for all i ∈ ℕ, then it is not strictly increasing.

It must be observed that a widening operator may serve different purposes, besides forcing the stabilization of approximated iteration sequences after a finite number of iterations: it may be used to speed up the convergence of iteration sequences and to select among a (possibly infinite) set of approximations of concrete elements when considering abstract domains that are algebraically weak [14]. Thus a widening does not need to be a total function, the only requirement is that its domain of definition be compatible with the

Zaffanella).

intended application. The application will also affect the required trade-off between precision and efficiency: when speeding up convergence of an (perhaps intrinsically finite) iteration sequence, precision is more willingly given away; in other cases, the objective is to ensure termination without compromising precision too much. As a consequence, it is meaningful to have two or more widening operators, each one tuned with a different compromise between precision and efficiency. The different widenings can be used in different applications or even in the same application, with the system (carefully) switching from one to another during the analysis [16].

For the domain of convex polyhedra, the first widening operator was proposed by Cousot and Halbwachs in [1] and further refined in [17]. It amply deserves the name of standard widening since most analysis and verification tools that employ convex polyhedra also employ that operator.

There are a number of applications of convex polyhedra in the field of system analysis and verification that are particularly sensitive to the precision of the deduced numerical information. The importance of precision in the field of automated verification has led to the use of extrapolation operators, that is, binary operators satisfying condition 1 in the definition of widening but not condition 2 (i.e., without convergence guarantee). For instance, in [18], Henzinger and Ho propose a new extrapolation operator for use in the HyTech model checker since “Halbwachs’s widening operator [...] is sometimes too coarse for [their] purposes” (symbolic model checking of linear hybrid systems). An even more precise extrapolation operator, also used in the HyTech system, is presented in [19]: “This operator is tighter than (and therefore less aggressive than) both the widening operator of [4] and the extrapolation operator of [18], which is not monotone in its second argument.” Other extrapolation operators based on similar approaches have been sketched in [3]. Still in the field of automatic verification, the need for more precision than warranted by the standard widening is remarked in both [20] and [21]; and a new extrapolation operator on sets of convex polyhedra is defined in each of these papers.

If giving up convergence guarantees is acceptable (though not desirable) for semi-automatic, human-operated verifiers, this is certainly not the case for fully-automatic program analyzers. In this field, the request for more precision has been partly satisfied by delaying the application of the widening operator k times for some fixed parameter k ∈ ℕ [16]. A study of the effect of alternative values for k in the automatic determination of linear size relations between the arguments of logic programs has been conducted in [8,9]. One application of this idea is in termination inference [22]. In order to achieve reasonable precision, the cTI analyzer runs with k = 3 as a default, but there are simple programs (such as mergesort) whose termination can only be established with k > 3. On the other hand, setting k = 4 as the default can have a sensible impact on performance of cTI [F. Mesnard, personal communication, 2003].

Another technique to improve upon the results of the standard widening, while still ensuring termination, is described in [4,23] and named ‘widening up to’. The technique checks the stability of a given finite set of constraints (specific to the application domain under consideration, possibly obtained by a previous static analysis step) adding any stable constraints to the extrapolated set. This can therefore recover from those extrapolations that go beyond the specified limits, provided these limits are never violated by the underlying iterates.

It should not be forgotten that the results obtained by means of an upward iteration sequence with widening can be improved by means of a downward iteration, possibly using a narrowing operator [2,13–15]. So, although this is outside the scope of the present paper, we regard this as an interesting direction for further research since, to the best of our knowledge, no narrowing operators for the domain of convex polyhedra have ever been proposed.

In this paper, after a formal introduction to the standard widening where we clarify some important aspects that are often overlooked, we embark on the challenging task of improving on it. Elaborating on an idea originally proposed in [3], we present a domain-independent framework for the systematic definition of new widenings that are never less precise than a given widening operator. Their specification is based on the definition of a computable preorder relation which satisfies the ascending chain condition on the considered abstract domain and is compatible with the widening we are improving upon. The framework makes it particularly easy to combine several heuristics and prove that the resulting operator is indeed a widening at least as precise as the original widening. Here we instantiate it on the domain of convex polyhedra so as to obtain a widening operator improving on the standard widening. In particular, we consider a selection of extrapolation operators, some of which embody improvements of heuristics already proposed in the literature. An experimental evaluation of the new widening shows that, for the analysis problem considered, it captures common growth patterns and obtains precision improvements in as many as 33% of the benchmarks. We show that, as is the case for the standard widening, even the precision of the new widening can be improved by combining it with the ‘widening up to’ technique, while still ensuring convergence. We also propose a modification of the delay technique where, for a given parameter k, the analyzer avoids the first k widening applications that would have caused actual precision losses. That is, when counting the number of delays, it ignores those steps where widening has no effect on the outcome.

The paper is structured as follows: Section 2 recalls the required concepts and notations; Section 3 introduces the standard widening for the domain of convex polyhedra, highlighting a few important aspects of its formal definition that are often overlooked; Section 4 presents a domain-independent framework for the systematic definition of new widening operators improving upon any existing widening; Section 5 instantiates this framework to the domain of convex polyhedra by considering several variants of extrapolation techniques proposed in the literature, as well as one that is new to this paper; Section 6 summarizes the results of our experimental evaluation of the new widening; Section 7 discusses the integration of the new widening with several widening strategies and techniques. Section 8 concludes. This paper is a revised and extended version of [24].

2 Preliminaries

A preorder ‘⪯’ over a set S is a binary relation that is reflexive and transitive. A preorder is an equivalence relation (resp., a partial order) if it is also symmetric (resp., antisymmetric). A preorder ‘⪯’ induces an equivalence relation ‘≡’ on S such that, for each x, y ∈ S, x ≡ y if and only if both x ⪯ y and y ⪯ x. The strict version ‘≺’ of a preorder ‘⪯’ is the relation such that, for each x, y ∈ S, x ≺ y if and only if x ⪯ y and x ≢ y.

A poset, denoted by ⟨P, ⊑⟩, is a set P equipped with a partial order ‘⊑’. A chain over the poset ⟨P, ⊑⟩ is a subset C ⊆ P such that ‘⊑’ is a total order on C, i.e., for each x, y ∈ C such that x ≠ y, either x ⊏ y or y ⊏ x. A poset satisfies the ascending chain condition if all its strictly increasing chains are finite. A preorder ‘⪯’ on a set S induces the poset ⟨S/≡, ⊑⟩: the set S/≡ is the quotient of S with respect to the equivalence relation ‘≡’ induced by ‘⪯’; and the partial order ‘⊑’ is such that [x] ⊑ [y] if and only if x ⪯ y, for all equivalence classes [x], [y] ∈ S/≡. In the following, with a minor abuse of terminology and notation, we will sometimes define preorders on sets and later state properties that actually hold for the implicitly induced posets. For instance, a preorder ‘⪯’ will be said to satisfy the ascending chain condition on a set S to mean that the induced poset ⟨S/≡, ⊑⟩ satisfies the ascending chain condition.

The lexicographic product of the preorders ‘⪯_{a}’ and ‘⪯_{b}’ is the preorder ‘⪯_{ab}’ on S such that, for all x, y ∈ S,

x ⪯_{ab} y ⟺^{def} (x ≺_{a} y) ∨ (x ≡_{a} y ∧ x ⪯_{b} y).

If both ‘⪯_{a}’ and ‘⪯_{b}’ satisfy the ascending chain condition on S, then ‘⪯_{ab}’ satisfies the ascending chain condition too. If ‘⪯’ is a preorder on S and ⊥ ∉ S, then the ⊥-lifting of ‘⪯’ is obtained by defining ⊥ ≺ x for all x ∈ S. If ‘⪯’ satisfies the ascending chain condition on S, then its ⊥-lifting satisfies the ascending chain condition on {⊥} ∪ S.

Let U be a set and S ⊆ U. If s, t ∈ U and s ∈ S, then we write S[t/s] to denote the set (S \{s})∪{t}. The cardinality of S is denoted by # S. If M and N are finite multisets over ℕ, #(n, M) denotes the number of occurrences of n ∈ ℕ in M and M ⊑_{ms} N means that either M = N or there exists j ∈ ℕ such that #(j, M) > #(j, N) and, for each k ∈ ℕ with k > j, #(k, M) = #(k, N). The relation ‘⊑_{ms}’ is a partial order satisfying the ascending chain condition [25].

The set of non-negative reals is denoted by ℝ_{+}. Any vector v⃗ ∈ ℝ^{n} is also a matrix in ℝ^{n×1} so that it can be manipulated with the usual matrix operations of addition and multiplication, both by a scalar and by another matrix. For each i = 1, … n, the i-th component of a vector v⃗ ∈ ℝ^{n} is denoted by v_{i}. The transposition of a matrix M is denoted by M^{T}; thus, for all v⃗ ∈ ℝ^{n}, we have v⃗ = (v_{1}, …, v_{n})^{T}. The scalar product of v⃗, w⃗ ∈ ℝ^{n} is ⟨v⃗, w⃗⟩ := ∑_{i=1}^{n} v_{i}w_{i}. The vector 0 ∈ ℝ^{n} has all components equal to zero. We write v⃗ = w⃗ and v⃗ ≠ w⃗ to denote the propositions ⋀_{i=1}^{n}(v_{i} = w_{i}) and ¬(v⃗ = w⃗), respectively.

Let V = {v⃗_{1}, …, v⃗_{k}} ⊆ ℝ^{n} be a finite set of real vectors. For all scalar constants λ_{1}, …, λ_{k} ∈ ℝ, the vector v⃗ = ∑_{i=1}^{k} λ_{i}v⃗_{i} is said to be a linear combination of the vectors in V. Such a combination is said to be

• a positive (or conic) combination, if λ_{i} ∈ ℝ_{+} for i = 1, …, k;

• an affine combination, if ∑_{i=1}^{k} λ_{i} = 1;

• a convex combination, if it is both positive and affine.

The vectors in V are said to be linearly independent if the only solution to the equation

∑_{i=1}^{k} λ_{i}v⃗_{i} = 0

is λ_{i} = 0, for each i = 1, …, k; they are said to be affinely independent if the only solution of the system of equations

\{ \begin{matrix}∑_{i=1}^{k} λ_{i}v⃗_{i} & = 0, \\ ∑_{i=1}^{k} λ_{i} & = 0 \end{matrix}

is λ_{i} = 0, for each i = 1, …, k.

Let V ⊆ ℝ^{n}. The subspace of ℝ^{n} defined by the set of all affine combinations of finite subsets of V is called the affine hull of V and denoted by aff.hull(V); the orthogonal of V and the opposite of V are given, respectively, by

V^{⊥} := { w⃗ ∈ ℝ^{n} | ∀v⃗ ∈ V : ⟨v⃗, w⃗⟩ = 0 },
−V := { −v⃗ ∈ ℝ^{n} | v⃗ ∈ V }.

For each vector a⃗ ∈ ℝ^{n} and scalar b ∈ ℝ, where a⃗ ≠ 0, the linear inequality constraint ⟨a⃗, x⃗⟩ ≥ b defines a topologically closed affine half-space of ℝ^{n}. We do not distinguish between syntactically different constraints defining the same affine half-space so that, for example, x ≥ 2 and 2x ≥ 4 are the same constraint. The set P ⊆ ℝ^{n} is a (closed and convex) polyhedron if and only if either P can be expressed as the intersection of a finite number of closed affine half-spaces of ℝ^{n}, or n = 0 and P = ∅. The set of all closed polyhedra on ℝ^{n} is denoted by ℂℙ_{n}. In this paper, we only consider polyhedra in ℂℙ_{n} when n > 0. The set ℂℙ_{n}, when partially ordered by subset inclusion, is a lattice where the binary meet operation is set-intersection; the binary join operation, denoted ‘⊎’, is called convex polyhedral hull, poly-hull for short.

If k ≤ n + 1 is the maximum number of affinely independent points of a polyhedron P ∈ ℂℙ_{n}, then the dimension of P, denoted as dim(P), is k − 1. If P ≠ ∅, the characteristic cone of P is defined as

char.cone(P) := { w⃗ ∈ ℝ^{n} | ∀v⃗ ∈ P : v⃗ + w⃗ ∈ P },

whereas the lineality space of P is

lin.space(P) := char.cone(P) ∩ − char.cone(P).

The linear equality constraint ⟨a⃗, x⃗⟩ = b defines an affine hyperplane of ℝ^{n}, i.e., the intersection of the affine half-spaces ⟨a⃗, x⃗⟩ ≥ b and ⟨−a⃗, x⃗⟩ ≥ −b. Each polyhedron P ∈ ℂℙ_{n} can therefore be represented by a finite set of linear equality and inequality constraints C called a constraint system. We write P = con(C). The subsets of equality and inequality constraints in system C are denoted by eq(C) and ineq(C), respectively. When P = con(C) ≠ ∅, we say that the constraint system C is in minimal form if # eq(C) = n − dim(P) and there does not exist C′ ⊂ C such that con(C′) = P. All the constraint systems in minimal form describing a given polyhedron have the same cardinality. When the constraint system C is not in minimal form, a constraint γ ∈ C is said to be redundant in C if con(C \ {γ}) = con(C).

Let P ∈ ℂℙ_{n}. A vector p⃗ ∈ P is called a point of P; a vector r⃗ ∈ ℝ^{n}, where r⃗ ≠ 0, is called a ray of P if P ≠ ∅ and p⃗ + ρr⃗ ∈ P, for all points p⃗ ∈ P and all ρ ∈ ℝ_{+}; a vector l⃗ ∈ ℝ^{n} is called a line of P if both l⃗ and −l⃗ are rays of P. We do not distinguish between rays (resp., lines) differing by a positive (resp., non-null) factor so that, for example, (1, 3)^{T} and (2, 6)^{T} are the same ray.

Given three finite sets of vectors L, R, P ⊆ ℝ^{n} such that L = {l⃗_{1}, …, l⃗_{ℓ}}, R = {r⃗_{1}, …, r⃗_{r}}, P = {p⃗_{1}, …, p⃗_{p}} and 0 ∉ L∪R, then the triple G = (L, R, P) is called a generator system for the polyhedron

gen(G) := \{ ∑_{i=1}^{ℓ} λ_{i}l⃗_{i} + ∑_{i=1}^{r} ρ_{i}r⃗_{i} + ∑_{i=1}^{p} π_{i}p⃗_{i} | \begin{matrix}λ⃗ ∈ ℝ^{ℓ}, ρ⃗ ∈ ℝr_{+}, π⃗ ∈ ℝp_{+}, \\ ∑_{i=1}^{p} π_{i} = 1 \end{matrix} \}.

The polyhedron gen(G) is empty if and only if P = ∅. If P ≠ ∅, the vectors in L, R and P are lines, rays and points of gen(G), respectively. We define an ordering ‘⊑_{G}’ on generator systems such that, for any generator systems G_{1} = (L_{1}, R_{1}, P_{1}) and G_{2} = (L_{2}, R_{2}, P_{2}), G_{1} ⊑_{G} G_{2} if and only if L_{1} ⊆ L_{2}, R_{1} ⊆ R_{2} and P_{1} ⊆ P_{2}; if, in addition, G_{1} ≠ G_{2}, we write G_{1} ⊏_{G} G_{2}. When gen(G) ≠ ∅, the generator system G = (L, R, P) is said to be in minimal form if # L = dim(lin.space(P)) and there does not exist a generator system G′ ⊏_{G} G such that gen(G′) = gen(G). All the generator systems in minimal form describing a given polyhedron have the same cardinalities for the line, ray and point components.

The possibility of representing a convex polyhedron by means of both constraint and generator systems is the basis of the double description method [26], which exploits the duality principle to compute each representation starting from the other one, possibly minimizing both descriptions. Clever implementations of this conversion procedure, such as those based on the extension by Le Verge [27] of Chernikova’s algorithms [28–30], are the starting point for the development of software libraries based on the double description method.^{1}

Let β = (⟨a⃗, x⃗⟩ ▷◁ b) be a linear constraint, where ▷◁ ∈ {≥, =}. We say that a point (resp., a ray or a line) v⃗ saturates the constraint β if and only if ⟨a⃗, v⃗⟩ = b (resp., ⟨a⃗, v⃗⟩ = 0). For each point p⃗ and constraint system C, we define the constraint system

sat con(p⃗, C) := { β ∈ C | p⃗ saturates β };

for each constraint β and generator system G = (L, R, P), we define the generator system sat gen(β, G) := (L′, R′, P′), where

L′ := { l⃗ ∈ L | l⃗ saturates β },
R′ := { r⃗ ∈ R | r⃗ saturates β },
P′ := { p⃗ ∈ P | p⃗ saturates β }.

A generator system G = (L, R, P) is in orthogonal form if it is in minimal form and R ∪ P ⊆ L^{⊥}. All generator systems in orthogonal form describing a

1 These libraries include: Polylib, designed and written by H. Le Verge and D. K. Wilde [27,31]; PolyLib, the successor of the library by Le Verge and Wilde [32]; New Polka, by B. Jeannet [33]; the polyhedra library that comes with the HyTech tool [6]; the Parma Polyhedra Library [34,35].

given polyhedron have identical sets of rays and points. A generator system in minimal form can be transformed into an equivalent system in orthogonal form by means of the well-known Gram-Shmidt method. By duality, orthogonal forms can also be defined for constraint systems. For each linear constraint β = (⟨a⃗, x⃗⟩ ▷◁ b), where ▷◁ ∈ {≥, =}, let slope(β) := a⃗. A constraint system C is in orthogonal form if it is in minimal form and we have I ⊆ E^{⊥}, where

I := { slope(β) | β ∈ ineq(C) },
E := { slope(β) | β ∈ eq(C) }.

All constraint systems in orthogonal form describing a given polyhedron have identical sets of inequality constraints.

3 The Standard Widening

The first widening on convex polyhedra was introduced in [1]. Intuitively, if P_{1} is the polyhedron obtained in the previous step of the upward iteration sequence and the current step yields polyhedron P_{2}, then the widening of P_{2} with respect to P_{1} is the polyhedron defined by all the constraints of P_{1} that are satisfied by all the points of P_{2}. An improvement on the above idea was defined in [17]. This operator, termed standard widening, has indeed been used almost universally.

The formal specification of the standard widening requires that each equality constraint is split into the two corresponding linear inequalities; thus, for each constraint system C, we define

repr_{≥}(C) := { ⟨−a⃗, x⃗⟩ ≥ −b | (⟨a⃗, x⃗⟩ = b) ∈ C }

∪ { ⟨a⃗, x⃗⟩ ≥ b | (⟨a⃗, x⃗⟩ ▷◁ b) ∈ C, ▷◁ ∈ {≥, =} }.

Definition 1 (Standard widening on ℂℙ_{n}.) [17, Définition 5.3.3, p. 57] For i = 1, 2, let P_{i} ∈ ℂℙ_{n} be such that P_{i} = con(C_{i}) and I_{i} = repr_{≥}(C_{i}) [and let C_{1} be either inconsistent or in minimal form]. Then the polyhedron P_{1} ∇_{S} P_{2} ∈ ℂℙ_{n} is defined as

P_{1} ∇_{S} P_{2} := \begin{cases}P_{2}, & if P_{1} = ∅; \\ con(I′_{1} ∪ I′_{2}), & otherwise; \end{cases}

where

I′_{1} := { β ∈ I_{1} | P_{2} ⊆ con({β}) },
I′_{2} := { γ ∈ I_{2} | ∃β ∈ I_{1} . P_{1} = con(I_{1}[γ/β]) }.

The constraints in I′_{1} are those that would have been selected when using the original proposal of [1], whereas the constraints in I′_{2} are added to ensure that this widening is a well-defined operator on the domain of polyhedra (i.e., it does not depend on the particular constraint representation).

Note that, in Definition 1, the condition in square brackets was implicit from the context of [17, Définition 5.3.3, p. 57], though not explicitly present in the definition itself. Such a requirement has been sometimes neglected in later papers discussing the standard widening (and also in some implementations), but it is actually needed in order to obtain a correct definition. In fact the following two examples show that, if a non-minimal constraint description is taken into account, then not only is the widening operator not well defined (see Example 2) but also the chain condition may be violated (see Example 3).

Example 2 For i = 1, 2, let P_{i} = con(C_{i}) ∈ ℂℙ_{2}, where

C_{1} = {x ≥ 0, y ≥ 0, x − y ≥ 2},
C_{2} = {x ≥ 2, y ≥ 0}.

Note that the constraint x ≥ 0 is redundant in C_{1}. By applying Definition 1 without enforcing minimization, we would obtain the polyhedron

P = con({x ≥ 0, y ≥ 0}).

In contrast, when correctly enforcing minimization, we obtain the polyhedron

P′ = con({y ≥ 0}).

Example 3 Consider, for each k ∈ ℕ, the polyhedron P_{k} := con(C_{k}) ∈ ℂℙ_{1}, where

C_{k} := \{0 ≤ x, x ≤ \frac{k}{k + 1}\} ∪ \{x ≤ 2\},

and note that no C_{k} is minimal since the constraint x ≤ 2 is redundant in all of them. Moreover, the infinite chain constituted by the P_{k}’s, that is, using an interval notation,

P_{0} = [0, 0], P_{1} = [0, \frac{1}{2}], P_{2} = [0, \frac{2}{3}], P_{3} = [0, \frac{3}{4}], …,

is strictly increasing. We will now show that, if we do not enforce minimization in the computation of the standard widening ‘∇_{S}’, then for the infinite chain Q_{0} = P_{0}, …, Q_{k+1} = Q_{k} ∇_{S} P_{k+1}, … we have Q_{n} = P_{n} for each n ∈ ℕ, so that the chain condition is violated.

For each n ∈ ℕ we have Q_{n} = con(D_{n}), where D_{0} := C_{0} and

D_{k+1} := { β ∈ D_{k} | P_{k+1} ⊆ con({β}) }

∪ { γ ∈ C_{k+1} | ∃β ∈ D_{k} . Q_{k} = con(D_{k}[γ/β]) }.

We will show by induction that D_{n} = C_{n} for each n ∈ ℕ. First we note that {0 ≤ x, x ≤ 2} ⊆ D_{0} = C_{0} and thus {0 ≤ x, x ≤ 2} ⊆ D_{k} for each k ∈ ℕ, since P_{k+1} ⊆ con({0 ≤ x}) and P_{k+1} ⊆ con({x ≤ 2}). Now assume D_{k} = C_{k}

and take β = (x ≤ 2) ∈ D_{k} and γ = (x ≤ \frac{k+1}{k+2}) ∈ C_{k+1}, so that

con(D_{k}[γ/β]) = con(\{0 ≤ x, x ≤ \frac{k}{k + 1}, x ≤ \frac{k + 1}{k + 2}\})

= con(\{0 ≤ x, x ≤ \frac{k}{k + 1}\})

= con(D_{k}).

We thus have D_{k+1} = \{0 ≤ x, x ≤ \frac{k+1}{k+2}, x ≤ 2\} = C_{k+1}.

3.1 Implementation of the Standard Widening

The proposition below provides an algorithm for computing the standard widening of the pair of polyhedra P_{1} and P_{2} when P_{1} ⊆ P_{2}. The idea, which was proposed in [17] and later reported in [23], is to replace the expensive test in the specification of I′_{2} in Definition 1 with an appropriate saturation condition to be checked on any generator system for P_{1}. This is worthwhile in all implementations based on the double description method. The algorithm here is an improved version over these proposals since neither the addition of the set of constraints I′_{1} as given in Definition 1 nor the splitting of equality constraints into pairs of inequalities is required. A similar result, but without the use of saturation conditions, can be found in [9, Chapter 6].

Proposition 4 Let P_{1} = con(C_{1}) = gen(G_{1}) ∈ ℂℙ_{n} and P_{2} = con(C_{2}) ∈ ℂℙ_{n}, where P_{1} ⊆ P_{2} and C_{1} is either inconsistent or in minimal form. Then

P_{1} ∇_{S} P_{2} = \begin{cases}P_{2}, & if P_{1} = ∅; \\ con(C_{S}), & otherwise; \end{cases}

where C_{S} := { γ ∈ C_{2} | ∃β ∈ C_{1} . sat gen(γ, G_{1}) = sat gen(β, G_{1}) }.

PROOF. The result holds trivially when P_{1} = ∅. Therefore, we assume that P_{1} ≠ ∅, so that by hypothesis C_{1} is in minimal form, and prove that P_{1} ∇_{S} P_{2} = con(C_{S}) by considering the two inclusions separately.

Assume the notation introduced in Definition 1 for the constraint systems I_{1}, I_{2} and I′_{1}, I′_{2}, so that P_{1} ∇_{S} P_{2} = con(I′_{1} ∪ I′_{2}). Let also I_{S} = repr_{≥}(C_{S}), so that con(C_{S}) = con(I_{S}) and

I_{S} := { γ ∈ I_{2} | ∃β ∈ I_{1} . sat gen(γ, G_{1}) = sat gen(β, G_{1}) }.

First we prove P_{1} ∇_{S} P_{2} ⊆ con(C_{S}) by showing that I_{S} ⊆ I′_{2}. Suppose, for some a⃗ ∈ ℝ^{n} and b ∈ ℝ, γ := (⟨a⃗, x⃗⟩ ≥ b) ∈ I_{S}. By definition of C_{S}, we have γ ∈ I_{2}. We will show that there exists β ∈ I_{1} such that

P_{1} = con(I_{1}[γ/β])  (1)

so that, by Definition 1, γ ∈ I′_{2} as required. First note that, as γ ∈ I_{S}, by the hypothesis, we can assume that there exists β′ ∈ C_{1} such that

sat gen(γ, G_{1}) = sat gen(β′, G_{1}).  (2)

We consider the two subcases β′ ∈ eq(C_{1}) and β′ ∈ ineq(C_{1}) separately. Suppose first that β′ ∈ eq(C_{1}). Then sat gen(β′, G_{1}) = G_{1} so that, by (2), we have sat gen(γ, G_{1}) = G_{1}. Let γ′ := (⟨a⃗, x⃗⟩ = b) be the equality constraint corresponding to the inequality γ, so that we obtain sat gen(γ′, G_{1}) = G_{1}. Thus, γ′ is a valid equality for polyhedron P_{1}. By hypothesis, C_{1} is in minimal form, so that γ′ (and hence, also γ) can be expressed as a linear combination of some of the constraints in eq(C_{1}). Namely, there exist k > 0 equality constraints {γ_{1}, …, γ_{k}} ⊆ eq(C_{1}) such that both a⃗ = ∑_{i=1}^{k} λ_{i}a⃗_{i} and b = ∑_{i=1}^{k} λ_{i}b_{i} hold where, for 1 ≤ i ≤ k, λ_{i} ∈ ℝ \ {0} and γ_{i} := (⟨a⃗_{i}, x⃗⟩ = b_{i}). Thus

λ_{1}a⃗_{1} = a⃗ − ∑_{i=2}^{k} λ_{i}a⃗_{i};  λ_{1}b_{1} = b − ∑_{i=2}^{k} λ_{i}b_{i}.  (3)

For 1 ≤ i ≤ k, let γ_{i}^{+} := (⟨a⃗_{i}, x⃗⟩ ≥ b_{i}) and γ_{i}^{−} := (⟨−a⃗_{i}, x⃗⟩ ≥ −b_{i}); moreover, take

β_{1} := \begin{cases}γ_{1}^{+}, & if λ_{1} > 0; \\ γ_{1}^{−}, & if λ_{1} < 0; \end{cases}

and, for 2 ≤ i ≤ k, let

β_{i} := \begin{cases}γ_{i}^{+}, & if λ_{i} < 0; \\ γ_{i}^{−}, & if λ_{i} > 0. \end{cases}

Note that, by definition of ‘repr_{≥}’, we have {β_{1}, β_{2}, …, β_{k}} ⊆ I_{1}. Then, the two equations (3) show that the inequality constraint β_{1} ∈ I_{1} can be computed as a positive combination of the inequality constraint γ ∈ I′_{2} and the inequality constraints {β_{2}, …, β_{k}} ⊆ I_{1}. Therefore, (1) holds by letting β = β_{1}.

For the second subcase, suppose β′ ∈ ineq(C_{1}), so that β′ ∈ I_{1}. As C_{1} is in minimal form, sat gen(β′, G_{1}) ≠ G_{1}. Informally, β′ can be seen as identifying one of the facets of P_{1}. Since (2) holds, the constraint γ identifies the same facet of P_{1}; since P_{1} ⊆ P_{2} ⊆ con({γ}), it is also a valid constraint for P_{1}, so

that P_{1} = con(I_{1}[γ/β′]). Therefore, (1) holds by letting β = β′.

Secondly we prove con(C_{S}) ⊆ P_{1} ∇_{S} P_{2}; as P_{1} ∇_{S} P_{2} = con(I′_{1} ∪ I′_{2}), we have to prove

con(C_{S}) ⊆ con(I′_{1}),  (4)
con(C_{S}) ⊆ con(I′_{2}).  (5)

To prove (4), we first show

con(C_{S}) ⊆ aff.hull(P_{2}) ⊆ aff.hull(con(I′_{1})).  (6)

Suppose γ ∈ C_{2} is a constraint defining the affine hull of P_{2}, so that it is saturated by all the points of P_{2}. Since P_{1} ⊆ P_{2}, γ is also saturated by all the points of P_{1}. Hence, there exists β ∈ C_{1} such that sat gen(β, G_{1}) = G_{1} = sat gen(γ, G_{1}). Thus, by definition of C_{S}, we have γ ∈ C_{S}. As this holds for all the constraints defining the affine hull of P_{2}, aff.hull(con(C_{S})) ⊆ aff.hull(P_{2}).

Since P_{2} ⊆ P_{1} ∇_{S} P_{2} ⊆ con(I′_{1}), we have aff.hull(P_{2}) ⊆ aff.hull(con(I′_{1})) and

hence, as con(C_{S}) ⊆ aff.hull(con(C_{S})), (6) holds.

We next show that, if β is any constraint in I′_{1}, then con(C_{S}) ⊆ con({β}). If β is a constraint defining the affine hull of con(I′_{1}), then this follows from (6). Suppose next that β is not a constraint defining the affine hull of con(I′_{1}). By Definition 1, I′_{1} ⊆ I_{1}; so that, as β ∈ I′_{1} and C_{1} is in minimal form, β defines a facet of con(I′_{1}) and β ∈ I_{1}. By hypothesis, P_{1} ⊆ P_{2} and, by Definition 1, P_{2} ⊆ con({β}); therefore there exists a constraint γ ∈ I_{2} that is saturated by the same points in P_{2} that saturate β. Hence sat gen(β, G_{1}) = sat gen(γ, G_{1}) so that γ ∈ I_{S} and con(C_{S}) = con(I_{S}) ⊆ con({γ}); moreover, we also obtain

con({γ}) ∩ aff.hull(P_{2}) = con({β}) ∩ aff.hull(P_{2}) ⊆ con({β})

so that, by (6), we have con(C_{S}) = con({γ}) ∩ con(C_{S}) ⊆ con({β}). Therefore

con(C_{S}) ⊆ con({β}) for all β ∈ I′_{1}; hence (4) holds.

We now show that (5) holds. Suppose γ ∈ I′_{2} so that, by Definition 1, γ ∈ I_{2} and there exists β ∈ I_{1} such that P_{1} = con(I_{1}[γ/β]). As C_{1} is in minimal form,

sat gen(γ, G_{1}) = sat gen(β, G_{1}) so that γ ∈ I_{S}; and hence con(C_{S}) ⊆ con({γ}). As the choice of γ ∈ I′_{2} was arbitrary, (5) holds. □

The next example shows that the inclusion hypothesis P_{1} ⊆ P_{2} in Proposition 4, which is implicitly present in [17,23], is vital in guaranteeing that the algorithm computes an upper approximation of P_{1} and P_{2}. Note that this is independent from the two improvements mentioned above.

Example 5 Let P_{1} := con(C_{1}) ∈ ℂℙ_{2} and P_{2} := con(C_{2}) ∈ ℂℙ_{2}, where

C_{1} := {x = 0, 0 ≤ y ≤ 2},
C_{2} := {y ≥ 2}.

Then P_{1} = gen(G_{1}), where G_{1} = (∅, ∅, P) and P = {(0, 0)^{T}, (2, 0)^{T}}. Note that P_{1} ⊈ P_{2}. By Definition 1, we obtain I′_{1} = I′_{2} = ∅, so that P_{1} ∇_{S} P_{2} = ℝ^{2}. Considering the constraints β = (−y ≥ −2) ∈ C_{1} and γ = (y ≥ 2) ∈ C_{2}, we have

sat gen(β, G_{1}) = (∅, ∅, {(2, 0)^{T}}) = sat gen(γ, G_{1}),

so that γ ∈ C_{S}. Thus, the result of the algorithm specified by Proposition 4 would be P_{2}, which is different from P_{1} ∇_{S} P_{2} and, moreover, is not an upper approximation of P_{1}.

As far as the implementation of the standard widening is concerned, it is worth noting the following result, which provides the justification for an alternative algorithm based on the original proposal in [1]. A similar result has also been proved in [9, Chapter 6].

Proposition 6 Let P_{1}, P_{2} ∈ ℂℙ_{n}, where P_{1} ⊆ P_{2} and dim(P_{1}) = dim(P_{2}). Let also P_{1} = con(C_{1}), where the constraint system C_{1} is either inconsistent or in minimal form. Then

P_{1} ∇_{S} P_{2} = \begin{cases}P_{2}, & if P_{1} = ∅; \\ con(C_{d}), & otherwise, \end{cases}

where C_{d} := { β ∈ C_{1} | P_{2} ⊆ con({β}) }.

PROOF. The result trivially holds if C_{1} is inconsistent. Thus, in the rest of the proof, we assume that C_{1} is consistent and in minimal form.

Let I_{1} = repr_{≥}(C_{1}) and I_{d} = repr_{≥}(C_{d}); let also I′_{1} be as given in Definition 1. Since I_{d} ⊆ I′_{1}, we have P_{1} ∇_{S} P_{2} ⊆ con(I_{d}) = con(C_{d}). Thus, to prove that P_{1} ∇_{S} P_{2} = con(C_{d}), we show that con(C_{d}) ⊆ P_{1} ∇_{S} P_{2}.

As dim(P_{1}) = dim(P_{2}) and P_{1} ⊆ P_{2}, we also have aff.hull(P_{1}) = aff.hull(P_{2}). Thus, there exists a constraint system C_{2} which is in minimal form and such that P_{2} = con(C_{2}) and eq(C_{1}) = eq(C_{2}).

Let P_{1} = gen(G_{1}) for some generator system G_{1} and

C_{S} := { γ ∈ C_{2} | ∃β ∈ C_{1} . sat gen(γ, G_{1}) = sat gen(β, G_{1}) }.

By Proposition 4, P_{1} ∇_{S} P_{2} = con(C_{S}). Therefore, it remains for us to show that con(C_{d}) ⊆ con(C_{S}). Suppose γ ∈ C_{S}. Then, by definition of C_{S}, there exists β ∈ C_{1} such that

con({β}) ∩ aff.hull(P_{1}) = con({γ}) ∩ aff.hull(P_{1}).  (7)

As P_{2} ⊆ con({γ}) and P_{2} ⊆ aff.hull(P_{1}), we obtain P_{2} ⊆ con({β}), so that

we also have β ∈ C_{d}. For any β′ ∈ eq(C_{1}), aff.hull(P_{1}) ⊆ con({β′}) so that,

since aff.hull(P_{1}) = aff.hull(P_{2}), P_{2} ⊆ con({β′}); and hence, by definition

of C_{d}, β′ ∈ C_{d} so that aff.hull(P_{1}) = aff.hull(con(C_{d})). Therefore it follows

from (7) that con(C_{d}) ⊆ con({γ}). As this holds for all γ ∈ C_{S}, we obtain con(C_{d}) ⊆ con(C_{S}). □

The interesting fact about an algorithm based on Proposition 6 is that, in most cases, the computation of a constraint system for the polyhedron P_{2} can be avoided, because any generator system for P_{2} can be used to efficiently check if dim(P_{1}) = dim(P_{2}) and, if so, to select the constraints from C_{1}; only if dim(P_{1}) ≠ dim(P_{2}) do we have to fall back to an implementation based on Proposition 4. Note that it is almost always the case that polyhedron P_{2} has been obtained as the result of a poly-hull operation so that, in a “lazy” implementation based on the double description method, the polyhedron will be described by a generator system only (since, in such implementations, the poly-hull is computed by taking the union of the generator systems of the arguments).

4 A Framework for Improving Upon a Widening

In this section, generalising an idea originally proposed in [3], we present a framework for the systematic definition of new and precise widening operators improving upon an existing widening.

Since a generic widening operator is a partial function, our framework has to make some assumptions about its domain of definition, so as to ensure that any call to this operator is well defined. For this reason, in the following we adopt a minor variation of the classical definition of the widening operator given in Section 1 (see the footnote in [15, p. 275]).

Definition 7 (Widening.) Let ⟨L, ⊥, ⊑, ⊔⟩ be a join-semi-lattice (i.e., the least upper bound x ⊔ y exists for all x, y ∈ L). The operator ∇: L × L ↣ L is a widening if

(1) for all x, y ∈ L, x ⊑ y implies that x ∇ y is defined and y ⊑ x ∇ y;

(2) for all increasing chains y_{0} ⊑ y_{1} ⊑ ⋯, the increasing chain defined by x_{0} := y_{0} and x_{i+1} := x_{i} ∇ (x_{i} ⊔ y_{i+1}), for i ∈ ℕ, is not strictly increasing.

It can be proved that, for any monotonic operator F: L → L, the upward iteration sequence with widenings starting at the bottom element x_{0} := ⊥ and defined by

x_{i+1} := \begin{cases}x_{i}, & if F(x_{i}) ⊑ x_{i}; \\ x_{i} ∇ (x_{i} ⊔ F(x_{i})), & otherwise; \end{cases}

converges to a post-fixpoint of ‘F’ after a finite number of iterations [15]. Note that the widening is always applied to arguments x = x_{i} and y = x_{i} ⊔ F(x_{i}) satisfying x ⊏ y. Therefore, problems such as the one outlined in Example 5 will be automatically avoided.

The framework is based on a class of preorders formalizing a notion of, so to speak, “guaranteed limited growth.”

Definition 8 (∇-compatible limited growth ordering.) Let ‘ ∇’ be a widening operator on the join-semi-lattice ⟨L, ⊥, ⊑, ⊔⟩. A limited growth ordering ( lgo, for short) is the strict version of any finitely computable preorder on L that satisfies the ascending chain condition. A ∇-compatible lgo ↷ ⊆ L × L is a limited growth ordering such that

∀x, y ∈ L : x ⊏ y ⟹ x ↷ x ∇ y.

The computability requirement is important because we will directly use the lgo relation to provide an executable specification of the new widenings. The ∇-compatibility requirement ensures that, in the definition of the new widening, we can use the widening ‘∇’ as a last resort operator without compromising the convergence guarantee. As a matter of fact, even the finite convergence guarantee for the widening ‘∇’ is a direct consequence of the ∇-compatibility requirement for the lgo relation.

The next result shows how a ∇-compatible lgo simplifies the definition of a new widening that improves on ‘∇’.

Theorem 9 Let ‘ ∇’ be a widening on the join-semi-lattice ⟨L, ⊥, ⊑, ⊔⟩. Suppose that ↷ ⊆ L × L is a ∇-compatible lgo and h: L × L → L is an upper bound operator. For all x, y ∈ L such that x ⊑ y, let

x ˜∇ y := \begin{cases}h(x, y), & if x ↷ h(x, y) ⊏ x ∇ y; \\ x ∇ y, & otherwise. \end{cases}

Then the ‘ ˜∇’ operator is a widening at least as precise as ‘ ∇’.

PROOF. By hypothesis, ‘h’ is an upper bound operator and, by Definition 7, the same holds for the widening ‘∇’. Thus, in all cases we have y ⊑ x ˜∇ y, so that the first condition in Definition 7 holds. Note that, in both the cases of the definition of ‘ ˜∇’, we have x ↷ x ˜∇ y: in the first case, this property holds by construction, whereas in the second case it holds by hypothesis, since the limited growth ordering ‘↷’ is ∇-compatible. By Definition 8, ‘↷’ satisfies the ascending chain condition, so that the second condition in Definition 7 also holds. Hence the ‘ ˜∇’ operator is a widening. Finally, the fact that ‘ ˜∇’ is at least as precise as ‘∇’ follows directly from the definition of ‘ ˜∇’. □

The above schema is easily extended to a framework for combining any finite set of upper bound operators with an existing widening to form a new widening operator with improved precision.

It should be stressed that Theorem 9 is not strong enough to ensure that the final results of upward iteration sequences computed by using the improved widening operator ‘ ˜∇’ are uniformly more precise than those obtained by using the existing widening operator ‘∇’. This property would hold if both widenings were monotonic on both of their arguments. However, such a stronger requirement is rarely satisfied when considering accurate widening operators on abstract domains having infinite ascending chains.

5 An Improvement Upon the Standard Widening

In this section, we instantiate the framework presented in Theorem 9 to a new widening on the domain of convex polyhedra. In particular, we will define a widening that improves upon the precision of the standard widening ‘∇_{S}’. To do this, we need to define both a specific ∇_{S}-compatible lgo on ℂℙ_{n} as well as a set of upper bound operators for this domain.

5.1 A ∇_{S}-Compatible Limited Growth Ordering

The ∇_{S}-compatible lgo we use for the new widening is defined as a combination of several simpler lgo relations on the domain of convex polyhedra; for one of these, we need the following ancilliary definition.

Definition 10 (Number of non-null coordinates of a vector.) For each v⃗ ∈ ℝ^{n}, we write κ(v⃗) to denote the number of non-null coordinates of v⃗. For each finite set V ⊆ ℝ^{n}, we define κ(V) to be the multiset obtained by applying ‘ κ’ to each of the vectors in V.

We now define a specific lgo relation as (the strict version of) the lexicographic product of five preorders on ℂℙ_{n}.

Definition 11 (‘↷_{N} ⊆ ℂℙ_{n} × ℂℙ_{n}’.) For i = 1, 2, let P_{i} = con(C_{i}) = gen(G_{i}) ∈ ℂℙ_{n} be a non-empty polyhedron, where the constraint system C_{i} is in minimal form and the generator system G_{i} = (L_{i}, R_{i}, P_{i}) is in orthogonal form. Then the preorders ⪯_{d}, ⪯_{ℓ}, ⪯_{c}, ⪯_{p}, ⪯_{r} ⊆ ℂℙ_{n} × ℂℙ_{n} are defined, respectively, as the ∅-liftings of the following relations:

P_{1} ⪯_{d} P_{2} ⟺^{def} # eq(C_{1}) ≥ # eq(C_{2});  (8)
P_{1} ⪯_{ℓ} P_{2} ⟺^{def} # L_{1} ≤ # L_{2};  (9)
P_{1} ⪯_{c} P_{2} ⟺^{def} # C_{1} ≥ # C_{2};  (10)
P_{1} ⪯_{p} P_{2} ⟺^{def} # P_{1} ≥ # P_{2};  (11)
P_{1} ⪯_{r} P_{2} ⟺^{def} κ(R_{1}) ⊑_{ms} κ(R_{2}).  (12)

The relation ↷_{N} ⊆ ℂℙ_{n}×ℂℙ_{n} is the strict version of the lexicographic product ⪯_{n} := ⪯_{dℓcpr} ⊆ ℂℙ_{n}×ℂℙ_{n} of the five relations ‘ ⪯_{d}’, ‘ ⪯_{ℓ}’, ‘ ⪯_{c}’, ‘ ⪯_{p}’, and ‘ ⪯_{r}’, taken in this order.

Note that the relation ‘↷_{N}’ is well defined, since it does not depend on the particular constraint and generator representations chosen. In particular, the minimality conditions for the constraint (resp., generator) systems ensure that the relations ‘⪯_{d}’ and ‘⪯_{c}’ (resp., ‘⪯_{ℓ}’ and ‘⪯_{p}’) are well defined; moreover, the orthogonality condition for the generator systems ensures that the computation of the multisets κ(R_{i}) is not ambiguous, so that ‘⪯_{r}’ is also well-defined.

The next result shows that ‘↷_{N}’ satisfies the hypotheses of the framework and can be used to improve upon the standard widening.

Theorem 12 The ‘ ↷_{N}’ relation is a ∇_{S}-compatible lgo on ℂℙ_{n}.

PROOF. It follows directly from Definition 11 that all the five preorders ‘⪯_{d}’, ‘⪯_{ℓ}’, ‘⪯_{c}’, ‘⪯_{p}’, and ‘⪯_{r}’ are finitely computable. We show that all the preorders satisfy the ascending chain condition.

To see this, consider their restriction to the set S = ℂℙ_{n} \ {∅} of all the non-empty polyhedra and assume the notation introduced in Definition 11. As the constraint systems C_{i} and the generator systems G_{i} are in minimal form, then we have n − # eq(C_{i}) = dim(P_{i}) and # L_{i} = dim(lin.space(P_{i})). As these dimensions can only have values in the finite set {0, …, n}, the preorders ‘⪯_{d}’ and ‘⪯_{ℓ}’ both satisfy the ascending chain condition on S. As the cardinalities of the constraint systems C_{i} and of the sets of points P_{i} are finite, the preorders ‘⪯_{c}’ and ‘⪯_{p}’ both satisfy the ascending chain condition on S. As the cardinalities of the sets of rays R_{i} are finite, the multisets κ(R_{i}) are also finite, so that the preorder ‘⪯_{r}’ inherits the ascending chain condition (on S) from the multiset partial order ‘⊑_{ms}’. The extension of all the preorders on ℂℙ_{n} does not pose problems because, as noted in Section 2, the ∅-lifting preserves the ascending chain condition.

Since ‘⪯_{n}’ is defined as the lexicographic product of these five relations, it is still finitely computable and it satisfies the ascending chain condition so that, by Definition 8, its strict version ‘↷_{N}’ is a limited growth ordering on ℂℙ_{n}. To complete the proof, we show that ‘↷_{N}’ is ∇_{S}-compatible. Namely, assuming that P_{1} ⊂ P_{2}, we prove that P_{1} ↷_{N} P_{1} ∇_{S} P_{2}.

If P_{1} = ∅, then P_{1} ∇_{S} P_{2} = P_{2} and, since P_{1} ⊂ P_{2}, by Definition 11 we obtain P_{1} ↷_{N} P_{2}. Now suppose P_{1} ≠ ∅, so that also P_{2} ≠ ∅, and assume the notation introduced in Definition 11.

Let P_{1} ∇_{S} P_{2} = P and consider the constraint systems I′_{1} and I′_{2} as specified in Definition 1. Then, P_{2} ⊆ con(I′_{1}) since P_{2} ⊆ con({β}) for all β ∈ I′_{1}; and also P_{2} ⊆ con(I′_{2}) since I′_{2} ⊆ repr_{≥}(C_{2}). Thus,

P_{2} ⊆ con(I′_{1}) ∩ con(I′_{2}) = con(I′_{1} ∪ I′_{2}) = P.

Since P_{1} ⊂ P_{2}, we also obtain P_{1} ⊂ P so that dim(P_{1}) ≤ dim(P) and dim(lin.space(P_{1})) ≤ dim(lin.space(P)). Let P = con(C) = gen(G), where the constraint system C is in minimal form and the generator system G = (L, R, P) is in orthogonal form. From the previous dimensionality properties, it follows that # eq(C_{1}) ≥ # eq(C) and # L_{1} ≤ # L so that, by Definition 11, P_{1} ⪯_{d} P and P_{1} ⪯_{ℓ} P.

If P_{1} ≺_{d} P or P_{1} ≺_{ℓ} P, then we obtain P_{1} ↷_{N} P. Otherwise, let P_{1} ≡_{d} P and P_{1} ≡_{ℓ} P. As P_{1} ⊂ P_{2} ⊆ P, from P_{1} ≡_{d} P we also obtain P_{1} ≡_{d} P_{2}, so that dim(P_{1}) = dim(P_{2}). Thus, Proposition 6 applies and we obtain P = con(C_{d}), where

C_{d} = { β ∈ C_{1} | P_{2} ⊆ con({β}) }.

As C_{1} is in minimal form and C_{d} ⊆ C_{1}, C_{d} is also in minimal form. Moreover, P_{1} ⊂ P_{2} ⊆ P implies C_{d} ≠ C_{1}, so that # C_{1} > # C_{d}. Thus we obtain P_{1} ≡_{d} P, P_{1} ≡_{ℓ} P and P_{1} ≺_{c} P, which together imply P_{1} ↷_{N} P. □

The ‘↷_{N}’ relation is a variant of a similar notion of limited growth defined in [3, Theorem 3]. These two proposals are not formally comparable since neither of the relations refines the other. On one hand, in Definition 11 we consider preorders that were not considered in [3], namely ‘⪯_{c}’ and ‘⪯_{r}’; on the other hand, due to the specific lexicographic product computed, the preorder ‘⪯_{p}’ comes into play only when the iteration is stable with respect to ‘⪯_{c}’. Moreover, the relation defined in [3] is not ∇_{S}-compatible: neither the standard widening ‘∇_{S}’, nor the heuristics informally sketched in [3] can ensure that consecutive iterates satisfy the given notion of limited growth. In summary, the overall approach in [3] does not define a widening operator in the precise sense of Definition 7 [F. Besson, personal communication, 2002].

5.2 The Heuristic Techniques

We now present the four different heuristic techniques, later shown to be upper bound operators, that we will use for constructing the new widening.

5.2.1 First Technique: Do Not Widen

The simplest heuristics, already suggested in [15] and adopted in [3], is the one saying “do not widen”: if we are along an iteration chain having finite length, there is no need to provide further approximations, so that we can safely return the most precise upper bound P_{2} (remember that we assume P_{1} ⊂ P_{2}). In our context, this is the case whenever P_{1} ↷_{N} P_{2}.

Figure 1 shows two examples where the “do not widen” technique is able to improve on the standard widening. In the left hand diagram, the result of the application of the standard widening to the line segment P_{1} and the rectangle P_{2} is P_{1} ∇_{S} P_{2} = ℝ^{2}. Since dim(P_{1}) = 1 < 2 = dim(P_{2}), we have P_{1} ≺_{d} P_{2}, which implies P_{1} ↷_{N} P_{2}. In the right hand diagram, the result of the application of the standard widening to the half stripe polyhedron P_{1} and the full stripe polyhedron P_{2} is again ℝ^{2}. Since dim(P_{1}) = dim(P_{2}) = 2 and dim(lin.space(P_{1})) = 0 < 1 = dim(lin.space(P_{2})), we obtain P_{1} ≡_{d} P_{2} and P_{1} ≺_{ℓ} P_{2}, which again imply P_{1} ↷_{N} P_{2}. Thus, in both cases, the “do not widen” heuristics will return the most precise upper bound P_{2}.

O  P_{2}  P_{1} P_{1} ∇_{S} P_{2}  ^{O  P_{1} P_{2} P_{1} ∇_{S} P_{2}}

Fig. 1. The “do not widen” heuristics improving on the standard widening.

As this heuristic technique, when applicable, returns the most precise result, it has to be tried first. As a consequence, all the other widening techniques considered here including the standard widening, are only applied to a pair of polyhedra P_{1} and P_{2} such that P_{1} ↷̸_{N} P_{2}: by Definition 11, this implies both dim(P_{1}) ≥ dim(P_{2}) and dim(lin.space(P_{1})) ≥ dim(lin.space(P_{2})) so that, by the hypothesis P_{1} ⊂ P_{2}, we also obtain aff.hull(P_{1}) = aff.hull(P_{2}) and lin.space(P_{1}) = lin.space(P_{2}), respectively. For these other techniques, since we cannot return the most precise upper bound P_{2}, we have to select what information will be lost. Informally, we will try to preserve the information provided by stable components, whereas the information of components that have changed will be extrapolated according to a hypothetical “change pattern.” For instance, in the case of the widening in [1], each element of a constraint system is regarded as a separate component and the extrapolation just forgets about the constraints that have changed.

5.2.2 Second Technique: Combining Constraints

The second heuristics, which is a variant of a similar one sketched in [3], can be seen as an application of the above approach, where instead of the constraints we consider the points in the generator system describing the polyhedron of the previous iteration. When using the standard widening it may happen that points that are common to the boundaries of P_{1} and P_{2} (and, hence, likely to be an invariant feature along the chain of polyhedra) will not lie on the boundary of the widened polyhedron. This is the case, for instance, for the points p⃗ and q⃗ in Figure 2. For such a point, the technique forces the presence of an inequality constraint that is saturated by the point, so that they will lie on the boundary of the result.

Definition 13 (Combining Constraints.) Let P_{1}, P_{2} ∈ ℂℙ_{n} be such that P_{1} ⊂ P_{2}, aff.hull(P_{1}) = aff.hull(P_{2}) and lin.space(P_{1}) = lin.space(P_{2}). Let P_{1} = gen(G_{1}), P_{2} = con(C_{2}) and P_{1} ∇_{S} P_{2} = con(C_{S}), where the constraint systems C_{2}, C_{S} and the generator system G_{1} = (L_{1}, R_{1}, P_{1}) are in orthogonal

O  P_{1} P_{2} p⃗  q⃗ P_{1} ∇_{S} P_{2}  ^{O  h_{c}(P_{1}, P_{2}) p⃗  q⃗ P_{1} P_{2} P_{1} ∇_{S} P_{2}}

Fig. 2. The heuristics ‘h_{c}’ improving on the standard widening.

form. Let also

C_{⊕} := \{ ⊕(Cp⃗) | \begin{matrix}p⃗ ∈ P_{1}, sat con(p⃗, ineq(C_{S})) = ∅, \\ Cp⃗ = sat con(p⃗, ineq(C_{2})) ≠ ∅ \end{matrix} \},

where the operator ‘ ⊕’ computes a convex combination of a non-empty set of linear inequality constraints (i.e., of the corresponding coefficients), returning another linear inequality constraint. Then h_{c}(P_{1}, P_{2}) := con(C_{S} ∪ C_{⊕}).

Since the operator ‘h_{c}’ is only defined for arguments having the same affine hull and lineality space, by requiring orthogonal forms we ensure that the result does not depend on the particular representations considered.

Note that the particular convex combination encoded by function ‘⊕’ is deliberately left unspecified so as to allow for a very liberal definition of ‘h_{c}’ that still possesses the required properties. For instance, in [3] it was argued that a good heuristics could be obtained by letting ‘⊕’ compute a normed linear combination (i.e., a sort of average) of the chosen constraints. Another legitimate choice would be to “bless” one of the constraints in Cp⃗ and forget all the others. In both cases, by keeping just one constraint for each point p⃗, we hopefully reduce the cardinality of the constraint system describing the result, so that it is more likely that a strict increase on the preorder ‘⪯_{c}’ will be obtained. Actually, this attempt at reducing the number of constraints is the main difference between the technique presented in Definition 13 and the extrapolation operator proposed in [19, Section 3.3], which could itself be included in the current framework as a more refined widening heuristics.

5.2.3 Third Technique: Evolving Points

Our third heuristic technique is a variant of the extrapolation operator ‘∝’ defined in [18]. The technique examines each new point p⃗_{2} of the polyhedron P_{2} as if it was obtained from each old point p⃗_{1} of the polyhedron P_{1}: we say that p⃗_{2} is an evolution of p⃗_{1}. The extrapolation is defined as continuing this evolution towards infinity, therefore generating the ray having direction p⃗_{2}−p⃗_{1}. To ensure the resulting polyhedron is at least as precise as the standard

O  P_{1} P_{2} p⃗_{2}  P_{1} ∇_{S} P_{2}  ^{O  P_{1} P_{2}  P_{1} ∇_{S} P_{2} h_{p}(P_{1}, P_{2})}

Fig. 3. The heuristics ‘h_{p}’ improving on the standard widening.

widening, any new rays that violate a constraint of the standard widening are dropped. Note that any remaining new rays will subsume the point p⃗_{2}, so that it is likely that a strict increase in the preorder ‘⪯_{p}’ will be obtained.

Definition 14 (Evolving Points.) Let P_{1}, P_{2} ∈ ℂℙ_{n} be such that P_{1} ⊂ P_{2} and lin.space(P_{1}) = lin.space(P_{2}). For each i = 1, 2, consider a generator system G_{i} = (L_{i}, R_{i}, P_{i}) in orthogonal form such that P_{i} = gen(G_{i}) and let

R := { p⃗_{2} − p⃗_{1} | p⃗_{1} ∈ P_{1}, p⃗_{2} ∈ P_{2} \ P_{1} }.

Then we define h_{p}(P_{1}, P_{2}) = gen((L_{2}, R_{2} ∪ R, P_{2})) ∩ (P_{1} ∇_{S} P_{2}).

Since the operator ‘h_{p}’ is only defined for arguments having the same lineality space, by requiring orthogonal forms we ensure that the result does not depend on the particular generator system representations considered.

Figure 3 shows an example where the “evolving points” technique is able to improve on the standard widening. Note that the boundary of P_{1}∇_{S}P_{2} contains the intersection of the boundaries of P_{1} and P_{2}, so that the “combining constraints” technique is not applicable. Besides having the same affine hull and lineality space, polyhedra P_{1}, P_{2} and h_{p}(P_{1}, P_{2}) are defined by constraint systems in minimal form having the same cardinality, so that P_{1} ↷_{N} h_{r}(P_{1}, P_{2}) holds because we have a strict increase in the preorder ‘⪯_{p}’.

The difference with respect to the extrapolation operator ‘∝’ is that we do not require the two points to lie on the same 1-dimensional face of P_{2}; moreover, the result of ‘∝’ may be less precise than the standard widening. Note that, as in the “combining constraints” technique, it is possible to add just a single ray which is a convex combination of the rays in R instead of the complete set R, yielding a more precise widening technique. However, this technique and the one defined by the ‘h_{p}’ operator are incomparable with respect to the ‘↷_{N}’ relation and one can fail the ‘↷_{N}’ convergence criterion when the other succeeds.

5.2.4 Fourth Technique: Evolving Rays

In the fourth heuristic technique (which is new), we try to extrapolate the rays that have evolved since the last iteration. The technique examines each new ray r⃗_{2} of the polyhedron P_{2} as if it was generated by rotation of each old ray r⃗_{1} of the polyhedron P_{1}: we say that r⃗_{2} is an evolution of r⃗_{1}. The extrapolation is defined as continuing this evolution until one or more of the non-null coordinates of ray r⃗_{2} become zero. This way, it is likely that a strict increase in the preorder ‘⪯_{r}’ will be obtained. Intuitively, the new ray will reach one of the boundaries of the orthant^{2} where r⃗_{2} lies, without trespassing it. As for the previous heuristics, to ensure the resulting polyhedron is at least as precise as the standard widening, any new ray that violates a constraint of the standard widening is dropped.

Definition 15 (‘evolve’.) The function evolve: ℝ^{n} × ℝ^{n} → ℝ^{n} is defined, for each u⃗, v⃗ ∈ ℝ^{n}, as evolve(u⃗, v⃗) := w⃗, where

w_{i} := \begin{cases}0, & if ∃j ∈ \{1, …, n\} . (u_{i}v_{j} − u_{j}v_{i})u_{i}u_{j} < 0, \\ u_{i}, & otherwise. \end{cases}

To understand this definition consider a pair of coordinates i and j and suppose that the vectors u⃗ and v⃗ are projected onto the two-dimensional plane defined by i (for the first coordinate) and j (for the second coordinate). Then, we identify the direction of the rotation of the vector (u_{i}, u_{j})^{T} with respect to the vector (v_{i}, v_{j})^{T} by using the well-known cross-product test [36, Chapter 35]; the direction is clockwise if c := u_{i}v_{j} − u_{j}v_{i} > 0 and anti-clockwise when c < 0. Moreover, vector (u_{i}, u_{j})^{T} lies inside the first or third quadrant when q = u_{i}u_{j} > 0 and it lies inside the second or fourth quadrant when q < 0. Then, the condition cq < 0 states that the evolution is clockwise and (u_{i}, u_{j})^{T} is in the second or fourth quadrant or the evolution is anti-clockwise and (u_{i}, u_{j})^{T} is in the first or third quadrant: in all these cases, the evolution is towards the j axis. Thus, for a fixed i, if there exists j such that the evolution is towards the j axis, then we define w_{i} = 0. Otherwise, we let w_{i} = u_{i}. We are now ready to define our last widening heuristics.

Definition 16 (Evolving Rays.) Let P_{1}, P_{2} ∈ ℂℙ_{n} be such that P_{1} ⊂ P_{2} and lin.space(P_{1}) = lin.space(P_{2}). For each i = 1, 2, consider a generator system G_{i} = (L_{i}, R_{i}, P_{i}) in orthogonal form such that P_{i} = gen(G_{i}) and let

R := { evolve(r⃗_{2}, r⃗_{1}) | r⃗_{1} ∈ R_{1}, r⃗_{2} ∈ R_{2} \ R_{1} }.

Then we define h_{r}(P_{1}, P_{2}) := gen((L_{2}, R_{2} ∪ R, P_{2})) ∩ (P_{1} ∇_{S} P_{2}).

2 An orthant is one of the 2^{n} regions of ℝ^{n} defined by the 2^{n} possible combinations of signs for x_{1}, … x_{n}.

O  P_{1} P_{2} P_{1} ∇_{S} P_{2}  ^{O  P_{1} P_{2} h_{r}(P_{1}, P_{2}) P_{1} ∇_{S} P_{2}}

Fig. 4. The heuristics ‘h_{r}’ improving on the standard widening.

Figure 4 shows an example where the “evolving rays” technique is able to improve on the standard widening. It should be noted that the boundary of P_{1} ∇_{S} P_{2} contains the intersection of the boundaries of P_{1} and P_{2}, so that the “combining constraints” technique is not applicable. Neither can the “evolving points” technique be applied, since P_{1} and P_{2} are defined by generator systems in orthogonal form having the same set of points. Besides having the same affine hull and lineality space, polyhedra P_{1}, P_{2} and h_{r}(P_{1}, P_{2}), are defined by constraint and generator systems in minimal form having the same number of constraints and points, so that P_{1} ↷_{N} h_{r}(P_{1}, P_{2}) holds because we have a strict increase in the preorder ‘⪯_{r}’.

5.3 The New Widening

In order to use these heuristic techniques in the general framework of Theorem 9, we must show that each of them is an upper bound operator. The first technique is by definition an upper bound operator. We now show that the other three techniques are also upper bound operators.

Proposition 17 Let P_{1}, P_{2} ∈ ℂℙ_{n}, where P_{1} ⊂ P_{2}, aff.hull(P_{1}) = aff.hull(P_{2}) and lin.space(P_{1}) = lin.space(P_{2}). Then, for each technique h ∈ {h_{c}, h_{p}, h_{r}}, P_{2} ⊆ h(P_{1}, P_{2}) ⊆ P_{1} ∇_{S} P_{2}.

PROOF. Let P_{t} = h(P_{1}, P_{2}). Consider first the case when h = h_{c} and assume the notation introduced in Definition 13. The proof for P_{t} ⊆ P_{1} ∇_{S} P_{2} is immediate, since P_{t} is defined by a constraint system C_{S} ∪ C_{⊕} including all of the constraints defining P_{1} ∇_{S} P_{2}. To prove that P_{2} ⊆ P_{t} we show that P_{2} ⊆ con({β}), for each constraint β ∈ C_{S} ∪ C_{⊕} defining P_{t}. Clearly, if β ∈ C_{S} then the inclusion holds by the fact that the standard widening is an upper bound operator. If otherwise β ∈ C_{⊕}, then, for some Cp⃗ ⊆ ineq(C_{2}), we have β = ⊕(Cp⃗), so that P_{2} ⊆ con(Cp⃗) ⊆ con({β}).

Next, consider the cases when h ∈ {h_{p}, h_{r}} and assume the notation introduced in Definitions 14 and 16. Let G′ = (L_{2}, R_{2} ∪ R, P_{2}) and P′ = gen(G′); then P_{t} = P′ ∩ (P_{1} ∇_{S} P_{2}). Thus P_{t} ⊆ P_{1} ∇_{S} P_{2}. As G_{2} ⊑_{G} G′, we obtain P_{2} ⊆ P′. Moreover, since the standard widening is an upper bound operator, we also have P_{2} ⊆ P_{1} ∇_{S} P_{2}. Therefore, by the monotonicity of set intersection, we conclude P_{2} ⊆ P_{t}. □

We now present our new widening operator.

Definition 18 (The ‘∇_{N}’ widening.) Let P_{1}, P_{2} ∈ ℂℙ_{n}, where P_{1} ⊂ P_{2}. Then

P_{1} ∇_{N} P_{2} := \begin{cases}P_{2}, & if P_{1} ↷_{N} P_{2}; \\ h_{c}(P_{1}, P_{2}), & if P_{1} ↷_{N} h_{c}(P_{1}, P_{2}) ⊂ P_{1} ∇_{S} P_{2}; \\ h_{p}(P_{1}, P_{2}), & if P_{1} ↷_{N} h_{p}(P_{1}, P_{2}) ⊂ P_{1} ∇_{S} P_{2}; \\ h_{r}(P_{1}, P_{2}), & if P_{1} ↷_{N} h_{r}(P_{1}, P_{2}) ⊂ P_{1} ∇_{S} P_{2}; \\ P_{1} ∇_{S} P_{2}, & otherwise. \end{cases}

It can be seen that ‘∇_{N}’ is an instance of the framework given in Theorem 9: in particular, when applying the first heuristics, the omission of the applicability condition P_{2} ⊂ P_{1} ∇_{S} P_{2} is a simple and inconsequential optimization. Thus, the following result is a direct consequence of Theorems 9 and 12 and Proposition 17.

Proposition 19 The ‘ ∇_{N}’ operator is a widening at least as precise as ‘ ∇_{S}’.

PROOF. Suppose that P_{1}, P_{2} ∈ ℂℙ_{n}, where P_{1} ⊂ P_{2}, so that Definition 18 applies. If P_{2} = P_{1} ∇_{S} P_{2}, then P_{1} ∇_{N} P_{2} = P_{1} ∇_{S} P_{2}. By Theorem 12, ‘↷_{N}’ is a ∇_{S}-compatible lgo on ℂℙ_{n}. Moreover, when P_{2} ⊂ P_{1} ∇_{S} P_{2}, all the heuristic techniques used in Definition 18 are upper bound operators since the first technique returns the least upper bound P_{2} while, for the other techniques, this is a consequence of Proposition 17. Therefore we can apply Theorem 9 to obtain the thesis. □

As already explained at the end of the previous section, Proposition 19 cannot ensure that a static analysis that is using the new widening will never be less precise than the same analysis but using the standard widening. The reasons are illustrated in the next example, where we show that the standard widening is not monotonic on its first argument [1] and the new widening is not monotonic on both arguments.

Example 20 Consider the polyhedral domain ℂℙ_{2} and let

P_{1} = con({2 ≤ x ≤ 3, 2 ≤ y ≤ 3}),
P′_{1} = con({0 ≤ x ≤ 5, 0 ≤ y ≤ 5, 2 ≤ x + y ≤ 8, −3 ≤ x − y ≤ 3}),
P_{2} = con({0 ≤ x ≤ 5, 0 ≤ y ≤ 5, 1 ≤ x + y ≤ 9, −4 ≤ x − y ≤ 4}),

so that P_{1} ⊂ P′_{1} ⊂ P_{2}. By Definitions 1 and 18, noting that both P_{1} ↷̸_{N} P_{2} and P′_{1} ↷̸_{N} P_{2}, we obtain

P_{1} ∇_{S} P_{2} = P_{1} ∇_{N} P_{2} = ℝ^{2},
P′_{1} ∇_{S} P_{2} = P′_{1} ∇_{N} P_{2} = con({0 ≤ x ≤ 5, 0 ≤ y ≤ 5}).

Thus, we have P_{1} ∇_{S} P_{2} ⊈ P′_{1} ∇_{S} P_{2} and P_{1} ∇_{N} P_{2} ⊈ P′_{1} ∇_{N} P_{2}, showing that neither the standard widening nor the new widening are monotonic on the first argument. Consider now

Q_{1} = con({1 ≤ x ≤ 2, 1 ≤ y ≤ 2}),
Q_{2} = con({0 ≤ x ≤ 3, 0 ≤ y ≤ 3}),
Q′_{2} = con({x ≥ 0, y ≥ 0, x + y ≤ 6}),

so that Q_{1} ⊂ Q_{2} ⊂ Q′_{2}. By Definition 18, as Q_{1} ↷̸_{N} Q_{2} but Q_{1} ↷_{N} Q′_{2},

Q_{1} ∇_{N} Q_{2} = Q_{1} ∇_{S} Q_{2} = ℝ^{2},
Q_{1} ∇_{N} Q′_{2} = Q′_{2}.

Thus, we obtain Q_{1} ∇_{N} Q_{2} ⊈ Q_{1} ∇_{N} Q′_{2}, showing that the new widening is not monotonic on its second argument either.

Note that in spite of this lack of monotonicity the experimental evaluation reported in the next section shows that, for the considered application, precision degradations are very rare.

6 Experimental Evaluation

We have extended the Parma Polyhedra Library (PPL) [34,35], a modern C^{++} library for the manipulation of convex polyhedra, with a prototype implementation of the widening of Definition 18. The PPL has been integrated with the China analyzer [37] for the purpose of detecting linear argument size relations [8]. Our benchmark suite consists of 361 Prolog programs, ranging from small synthetic benchmarks to real-world applications. They define 23279 predicates whose analysis with China requires the direct use of a widening and about as many predicates for which no widening is used. In this respect, it must be

# programs  # predicates
k (delay) improve degr incomp improve degr incomp
0  121  0  2  1340  3  2
1  34  0  0  273  0  0
2  29  0  0  222  0  0
3  28  0  0  160  0  0
4  25  0  2  126  2  0
10  25  0  0  124  0  0

Table 1 Precision comparisons.

noted that China employs a sophisticate chaotic iteration strategy proposed in [38,39] that, among other benefits, allows to greatly reduce the number of widenings’ applications.^{3} This is an important point, since it would be quite easy to improve on an iteration strategy applying widenings “everywhere or improperly” [38]. The results of this experimental evaluation are summarized in Tables 1 and 2, where each row corresponds to a different choice for the value of the extrapolation threshold k, controlling the delay before the applications of both the standard and the new widening operators.

Table 1 shows the obtained precision improvements (in the columns labeled ‘improve’) and degradations (in the columns labeled ‘degr’), both in terms of the number of programs and the number of predicates affected; in the columns labeled ‘incomp’ we report those cases where incomparable results have been obtained. For k = 0, we observe a precision improvement on one third of the considered programs; not surprisingly, fewer improvements are obtained for higher values of k, but we still have an improvement on 7% of the benchmarks when considering k = 10. While confirming, as informally argued in [8], that for this particular analysis there is little incentive in using values of k greater than 4, our experiments show that the new widening captures growth patterns that do happen in practice and that for the standard widening (no matter how delayed) are out of reach. This is important since the results obtained in practice are, besides correctness, what really matters when evaluating widening operators. The experimentation also shows that the idea of delaying the widening [16] maintains its validity: even though the new widening is less sensible to the amount of delay applied, the results are still sensibly improved by delaying.

3 China uses the recursive fixpoint iteration strategy on the weak topological ordering defined by partitioning of the call graph into strongly-connected subcomponents [39].

∇^{k}_{S}  ∇^{k}_{N}
k (delay) all top 20 all top 20
0 1.00  0.72 1.05  0.77
1 1.09  0.79 1.11  0.80
2 1.16  0.83 1.18  0.84
3 1.23  0.88 1.25  0.89
4 1.32  0.95 1.34  0.95
10 1.82  1.23 1.85  1.24

Table 2 Time comparisons.

Table 2 shows the sum, over all the benchmarks, of the fixpoint computation times. This is expressed as a proportion of the time spent when using the standard widening with k = 0. Since smaller benchmarks may affect the outcome of this summarization, in the columns labeled ‘top 20’ we also show the same values but restricted to the 20 benchmarks whose analysis takes more time. It can be seen that the new widening has a negative, but relatively modest impact on efficiency, which anyway is smaller than the cost of increasing the value of k. When looking at these time results, it should be considered that we are comparing a prototype implementation of the new widening with respect to a rather optimized implementation of the standard widening. It is also important to remark that the good performance degradation observed for both widenings when increasing the value of k is essentially due to the iteration strategy employed by China and should not be expected to automatically carry over to systems using other fixpoint computation techniques.

7 Improved Widening Strategies

The technique of employing an extrapolation threshold k has been traditionally implemented (and our experimental evaluation makes no exception) in a “simple way” [15], as a blind delay in the application of the widening. Namely,

for each widening operator ‘∇’, the widening operator ‘∇^{k}’ is formalized as follows, where each abstract value is a pair recording, in its second component, the iterations in which it has been computed:

⟨x, i⟩ ∇^{k} ⟨y, i + 1⟩ := \begin{cases}⟨x, i + 1⟩, & if y ⊑ x; \\ ⟨x ⊔ y, i + 1⟩, & if i < k; \\ ⟨x ∇ y, i + 1⟩, & otherwise. \end{cases}

Thus, no matter what abstract value would have been computed by the widening, the widening is never applied in the first k iteration steps and it is always applied in all the following iteration steps.

In our opinion, a better approximation strategy can be obtained by interpreting the value k as the maximum number of iterations for which the computation of the widening can be safely avoided. Thus, an abstract value is a pair carrying a number of “tokens” t, each of them allowing for the replacement of one widening application by the exact upper bound. Aiming at an improvement in the final result, each widening operator should be left free to choose when to use the available tokens. For instance, tokens should not be wasted when the widening is precise, that is, when it simply computes the least upper bound of its arguments. The following definition of ‘∇^{∘}’ (widening with tokens) formalizes this idea:

⟨x, t⟩ ∇^{∘} ⟨y, ·⟩ := \begin{cases}⟨x, t⟩, & if y ⊑ x; \\ ⟨x ∇ y, t⟩, & if x ∇ y = x ⊔ y; \\ ⟨x ⊔ y, t − 1⟩, & if t > 0; \\ ⟨x ∇ y, 0⟩, & otherwise. \end{cases}

The iteration sequence will begin with abstract values of the form ⟨x_{0}, k⟩, that is, with k tokens where k is a parameter of the analysis; the number of tokens will decrease along the iteration chain and, when there are no tokens left, the widening will always be applied. Notice that, when instantiating the above construction with our new widening operator ‘∇_{N}’ (and assuming the inclusion

hypothesis), the conditional guard for the second case of the definition of ‘∇^{∘}’ becomes P_{1} ∇_{N} P_{2} = P_{2}, which can be easily implemented by performing the test P_{1} ↷_{N} P_{2}.

Also note that more general definitions for ‘∇^{∘}’ are possible: for instance, when x ∇ y ≠ x ⊔ y and t > 0 (i.e., the widening does not compute the exact upper bound and there still are tokens available), we may nonetheless choose to apply the widening operator, provided the corresponding approximation is good enough. This way, we may preserve the tokens and use them to avoid some later approximations, which could be much coarser than the current one. Clearly, such an approach depends on the particular formalization of the notion of “good enough”, which is, along with the value of k, intrinsically application dependent.

More clever delay strategies have been proposed in the literature. As an example, in [4,23] it is suggested that, in order to mitigate the precision losses caused by irregularities in the control flow of the analyzed system, the early extrapolations can be undone and recomputed when more information is available. This happens, for instance, when a polyhedron associated to a widening point depends on another polyhedron which becomes non-empty only after the computation of some iterates. In most cases, these enhanced widening strategies are independent of the specific widening operator and abstract domain considered, so that they can be applied to the widenings obtained by instantiating the framework presented here.

As mentioned in the introduction, for the domain of polyhedra, another way to improve the precision of the standard widening is to apply the ‘widening up to’ technique [4,23]: namely, for any fixed and finite set of constraints C, the standard widening “up to C” is defined as the intersection of the polyhedron P_{1} ∇_{S} P_{2} with all the constraints in C that are satisfied by both arguments P_{1} and P_{2}. However, as the technique may add constraints, it appears that its application might interfere with the cardinality-based convergence criterion of the standard widening. Observe though that, by Definition 1, a constraint in a minimal constraint system describing P_{1} will be dropped only if it is violated by P_{2}. Hence, once a constraint in C has been dropped by the standard widening, the ‘widening up to’ technique will never restate it back. As a consequence, in an iteration sequence with the widening “up to C” applied, the number of times this technique can actually improve on the standard widening may not exceed the cardinality of C. As C is finite, any iteration sequence using this technique will always converge.

The ‘widening up to’ technique can also be combined with the new widening: being at least as precise as the standard widening, the operator ‘∇_{N}’ still satisfies the above observation, so that the convergence of the iteration sequence is preserved. In fact, in the experimental evaluation of the previous section, the ‘widening up to’ technique has been applied to both widenings so as to enforce the non-negativity constraints for the numeric variables representing the argument sizes. It should though be stressed that, in the general case, the combination of the ‘widening up to’ technique with an arbitrary widening operator may cause divergence.

8 Conclusion and Related Work

For the domain of convex polyhedra, the convergence guarantee of the fixpoint computation sequence has been traditionally obtained thanks to the widening operator proposed by Cousot and Halbwachs. Though remarkably precise, this operator does not fulfill the requirements of a number of systems’ analysis and verification applications that are particularly sensitive to the precision of the deduced numerical information. In this paper, elaborating on an idea proposed in [3], we have defined a framework for the systematic specification of new widening operators improving on the precision of an existing widening. The framework allows any upper bound operator on the abstract domain to be used as a heuristic technique for improving precision, while still ensuring the termination of the abstract computation. We have instantiated the framework on the domain of convex polyhedra with a selection of extrapolation operators, some of which embody improvements of heuristics already proposed in the literature. A first experimental evaluation has yielded promising results. The experimental work has also suggested that the well-known widening delay technique can be improved, yet retaining its overall simplicity. Our proposal is to delay the widening application only when this prevents actual (as opposed to potential) precision losses. The resulting widening would thus adapt, to some extent, to the abstract description chain being traversed.

It is worth noticing that the framework presented in this paper is indeed quite general. It is based on the specification of a computational ordering [14] that satisfies the ascending chain condition. Then a preexisting widening and any finite set of extrapolation heuristics are combined so as to ensure that the combination turns every ascending chain (with respect to the approximation ordering) into a chain for the computational ordering. We have shown that this is sufficient to ensure that the combination defines a widening. Moreover, we have also shown that the new widening so obtained is never less precise than the preexisting widening: this is an important feature for those cases, such as the one of convex polyhedra, where the preexisting widening has proved its adequacy on a number of different applications. This general idea is exploited in [40] to obtain widenings for finite powerset domains (i.e., particular refinements of an abstract domain that allow for the exact representation of finite disjunctions), and we expect it can be successfully adopted for any abstract domain.

Acknowledgments. We would like to express our gratitude to Frédéric Besson for his useful comments and observations on the ideas sketched in [3]; Fred Mesnard for the information and the discussions we had with him about the impact of precision on termination inference for Prolog programs; and the reviewers of [24] and of this paper for their careful comments that helped us improve the paper.

References

[1] P. Cousot, 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, ACM Press, Tucson, Arizona, 1978, pp. 84–96.

[2] P. Cousot, 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, ACM Press, New York, 1977, pp. 238–252.

[3] F. Besson, T. P. Jensen, J.-P. Talpin, Polyhedral analysis for synchronous languages, in: A. Cortesi, G. Filé (Eds.), Static Analysis: Proceedings of the 6th International Symposium, Vol. 1694 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, Venice, Italy, 1999, pp. 51–68.

[4] N. Halbwachs, Delay analysis in synchronous programs, in: C. Courcoubetis (Ed.), Computer Aided Verification: Proceedings of the 5th International Conference, Vol. 697 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, Elounda, Greece, 1993, pp. 333–346.

[5] N. Halbwachs, Y.-E. Proy, P. Raymond, Verification of linear hybrid systems by means of convex approximations, in: B. Le Charlier (Ed.), Static Analysis: Proceedings of the 1st International Symposium, Vol. 864 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, Namur, Belgium, 1994, pp. 223–237.

[6] T. A. Henzinger, P.-H. Ho, H. Wong-Toi, HyTech: A model checker for hybrid systems, Software Tools for Technology Transfer 1 (1+2) (1997) 110–122.

[7] Z. Manna, N. S. Bjørner, A. Browne, M. Colón, B. Finkbeiner, M. Pichora, H. B. Sipma, T. E. Uribe, An update on STeP: Deductive-algorithmic verification of reactive systems, in: R. Berghammer, Y. Lakhnech (Eds.), Tool Support for System Specification, Development and Verification, Advances in Computing Sciences, Springer-Verlag, Berlin, 1999, pp. 174–188.

[8] F. Benoy, A. King, Inferring argument size relationships with CLP(R), in: J. P. Gallagher (Ed.), Logic Program Synthesis and Transformation: Proceedings of the 6th International Workshop, Vol. 1207 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, Stockholm, Sweden, 1997, pp. 204–223.

[9] P. M. Benoy, Polyhedral domains for abstract interpretation in logic programming, Ph.D. thesis, Computing Laboratory, University of Kent, Canterbury, Kent, UK (Jan. 2002).

[10] W. Pugh, A practical algorithm for exact array dependence analysis, Communications of the ACM 35 (8) (1992) 102–114.

[11] N. Dor, M. Rodeh, S. Sagiv, Cleanness checking of string manipulations in C programs via integer analysis, in: Cousot [41], pp. 194–212.

[12] M. A. Colón, H. B. Sipma, Synthesis of linear ranking functions, in: T. Margaria, W. Yi (Eds.), Tools and Algorithms for Construction and Analysis of Systems, 7th International Conference, TACAS 2001, Vol. 2031 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, Genova, Italy, 2001, pp. 67–81.

[13] P. Cousot, R. Cousot, Static determination of dynamic properties of programs, in: B. Robinet (Ed.), Proceedings of the Second International Symposium on Programming, Dunod, Paris, France, 1976, pp. 106–130.

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

[15] P. Cousot, R. Cousot, Comparing the Galois connection and widening/narrowing approaches to abstract interpretation, in: M. Bruynooghe, M. Wirsing (Eds.), Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming, Vol. 631 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, Leuven, Belgium, 1992, pp. 269–295.

[16] P. Cousot, Semantic foundations of program analysis, in: S. S. Muchnick, N. D. Jones (Eds.), Program Flow Analysis: Theory and Applications, Prentice-Hall, Inc., Englewood Cliffs, New Jersey, 1981, Ch. 10, pp. 303–342.

[17] N. Halbwachs, Détermination automatique de relations linéaires vérifiées par les variables d’un programme, Thèse de 3^{ème} cycle d’informatique, Université scientifique et médicale de Grenoble, Grenoble, France (Mar. 1979).

[18] T. A. Henzinger, P.-H. Ho, A note on abstract interpretation strategies for hybrid automata, in: P. J. Antsaklis, W. Kohn, A. Nerode, S. Sastry (Eds.), Hybrid Systems II, Vol. 999 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1995, pp. 252–264.

[19] T. A. Henzinger, J. Preussig, H. Wong-Toi, Some lessons from the hytech experience, in: Proceedings of the 40th Annual Conference on Decision and Control, IEEE Computer Society Press, 2001, pp. 2887–2892.

[20] T. Bultan, R. Gerber, W. Pugh, Model-checking concurrent systems with unbounded integer variables: Symbolic representations, approximations, and experimental results, ACM Transactions on Programming Languages and Systems 21 (4) (1999) 747–789.

[21] G. Delzanno, A. Podelski, Model checking in CLP, in: R. Cleaveland (Ed.), Tools and Algorithms for Construction and Analysis of Systems, 5th International Conference, TACAS ’99, Vol. 1579 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, Amsterdam, The Netherlands, 1999, pp. 223– 239.

[22] F. Mesnard, U. Neumerkel, Applying static analysis techniques for inferring termination conditions of logic programs, in: Cousot [41], pp. 93–110.

[23] N. Halbwachs, Y.-E. Proy, P. Roumanoff, Verification of real-time systems using linear relation analysis, Formal Methods in System Design 11 (2) (1997) 157– 185.

[24] R. Bagnara, P. M. Hill, E. Ricci, E. Zaffanella, Precise widening operators for convex polyhedra, in: R. Cousot (Ed.), Static Analysis: Proceedings of the 10th International Symposium, Vol. 2694 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, San Diego, California, USA, 2003, pp. 337–354.

[25] N. Dershowitz, Z. Manna, Proving termination with multiset orderings, Communications of the ACM 22 (8) (1979) 465–476.

[26] T. S. Motzkin, H. Raiffa, G. L. Thompson, R. M. Thrall, The double description method, in: H. W. Kuhn, A. W. Tucker (Eds.), Contributions to the Theory of Games – Volume II, no. 28 in Annals of Mathematics Studies, Princeton University Press, Princeton, New Jersey, 1953, pp. 51–73.

[27] H. Le Verge, A note on Chernikova’s algorithm, Publication interne 635, IRISA, Campus de Beaulieu, Rennes, France (1992).

[28] N. V. Chernikova, Algorithm for finding a general formula for the non-negative solutions of system of linear equations, U.S.S.R. Computational Mathematics and Mathematical Physics 4 (4) (1964) 151–158.

[29] N. V. Chernikova, Algorithm for finding a general formula for the non-negative solutions of system of linear inequalities, U.S.S.R. Computational Mathematics and Mathematical Physics 5 (2) (1965) 228–233.

[30] N. V. Chernikova, Algorithm for discovering the set of all solutions of a linear programming problem, U.S.S.R. Computational Mathematics and Mathematical Physics 8 (6) (1968) 282–293.

[31] D. K. Wilde, A library for doing polyhedral operations, Master’s thesis, Oregon State University, Corvallis, Oregon, also published as IRISA Publication interne 785, Rennes, France, 1993 (Dec. 1993).

[32] V. Loechner, PolyLib: A library for manipulating parameterized polyhedra,

Available at http://icps.u-strasbg.fr/~loechner/polylib/, declares itself

to be a continuation of [31] (Mar. 1999).

[33] B. Jeannet, Convex Polyhedra Library, release 1.1.3c Edition, documentation of

the “New Polka” library available at http://www.irisa.fr/prive/Bertrand.
Jeannet/newpolka.html (Mar. 2002).

[34] R. Bagnara, P. M. Hill, E. Zaffanella, The Parma Polyhedra Library User’s Manual, Department of Mathematics, University of Parma, Parma, Italy, release 0.7 Edition, available at http://www.cs.unipr.it/ppl/ (Dec. 2004).

[35] R. Bagnara, E. Ricci, E. Zaffanella, P. M. Hill, Possibly not closed convex polyhedra and the Parma Polyhedra Library, in: M. V. Hermenegildo, G. Puebla (Eds.), Static Analysis: Proceedings of the 9th International Symposium, Vol. 2477 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, Madrid, Spain, 2002, pp. 213–229.

[36] T. H. Cormen, T. E. Leiserson, R. L. Rivest, Introduction to Algorithms, The MIT Press, Cambridge, MA, 1990.

[37] R. Bagnara, Data-flow analysis for constraint logic-based languages, Ph.D. thesis, Dipartimento di Informatica, Università di Pisa, Pisa, Italy, printed as Report TD-1/97 (March 1997).

[38] F. Bourdoncle, Efficient chaotic iteration strategies with widenings, in: D. Bjørner, M. Broy, I. V. Pottosin (Eds.), Proceedings of the International Conference on “Formal Methods in Programming and Their Applications”, Vol. 735 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, Academgorodok, Novosibirsk, Russia, 1993, pp. 128–141.

[39] F. Bourdoncle, Sémantiques des langages impératifs d’ordre supérieur et interprétation abstraite, PRL Research Report 22, DEC Paris Research Laboratory (1993).

[40] R. Bagnara, P. M. Hill, E. Zaffanella, Widening operators for powerset domains, in: B. Steffen, G. Levi (Eds.), Proceedings of the Fifth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2004), Vol. 2937 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, Venice, Italy, 2003, pp. 135–148.

[41] P. Cousot (Ed.), Static Analysis: 8th International Symposium, SAS 2001, Vol. 2126 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, Paris, France, 2001.