Precise Widening Operators for Convex Polyhedra^{⋆}

Roberto Bagnara^{1}, Patricia M. Hill^{2}, Elisa Ricci^{1}, and Enea Zaffanella^{1}

1 Department of Mathematics, University of Parma, Italy

           {bagnara,ericci,zaffanella}@cs.unipr.it

2 School of Computing, University of Leeds, UK

                    hill@comp.leeds.ac.uk

Abstract. 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 convergence of the fixpoint computation. 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 and precise widening operators for convex polyhedra. The framework is then instantiated so as to obtain a new widening operator that combines several heuristics and uses the standard widening as a last resort so that it is never less precise. A preliminary experimental evaluation has yielded promising results.

1 Introduction

An ability to reason about numerical quantities is crucial for increasing numbers 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 [19], constitute the most used abstract domain among those capturing numerical, relational information. They have been used to solve, by abstract interpretation [16], several

⋆ This work has been partly supported by MURST projects “Aggregate- and numberreasoning for computing: from decision algorithms to constraint programming with multisets, sets, and maps” and “Constraint Based Verification of Reactive Systems”.

important data-flow analysis problems such as array bound checking, compiletime 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 [7, 24] and of linear hybrid automata (an extension of finite-state machines that models time requirements) [25, 28], for the computer-aided formal verification of concurrent and reactive systems based on temporal specifications [30], for inferring argument size relationships in logic languages [5, 6], for the automatic parallelization of imperative programs [32], for detecting buffer overflows in C [22], and for the automatic generation of the ranking functions needed to prove progress properties [11].

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

1. for each x, y ∈ L such that x∇y is defined, we have x ⊑ x∇y 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} ∇ y_{i+1}, for i ∈ ℕ, 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 ensure the existence of the approximations of concrete elements when considering abstract domains that are algebraically weak [17]. Thus a widening does not need to be a total function, the only requirement is that its domain of definition be compatible with the 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 dynamically switching from one to another [13].

For the domain of convex polyhedra, the first widening operator was proposed by Cousot and Halbwachs in [19] and further refined in [23]. 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 systems 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 guarantees). For instance, in [27], 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 [29]: “This operator is tighter than (and therefore less aggressive than) both the widening operator of [24] and the extrapolation operator of [27], which is not monotone in its second argument.” Other extrapolation operators based on similar approaches have been sketched in [7]. Still in the field of automatic verification, the need for more precision than warranted by the standard widening is remarked in both [10] and [20]; 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 fullyautomatic 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 ∈ ℕ [13]. 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 [5, 6]. One application of this idea is in termination inference [31]. 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 a widening, while still ensuring termination, is described in [24, 26] and named ‘widening up to’. This is meant to recover from those extrapolations that go beyond the limits specified by a fixed set of constraints, which are specific of the application domain under consideration or have been obtained by a previous static analysis step.

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 [7], we present a framework for the systematic definition of new and precise widening operators for convex polyhedra, which is based on the definition of a suitable relation on convex polyhedra satisfying the ascending chain condition. The framework makes it particularly easy to combine several heuristics and prove that the resulting operator is indeed a widening. Here we instantiate it with a selection of extrapolation operators —some of which embody improvements of heuristics already proposed in the literature— and the standard widening so that the new widening operator is always at least as precise as the standard one for a single application. 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.

The paper is structured as follows: Section 2 recalls the required concepts and notations; Section 3 introduces the standard widening, highlighting a few important aspects of its formal definition that are often overlooked; Section 4 presents a framework for the systematic definition of new widening operators improving upon the standard widening; Section 5 instantiates this framework by considering several variants of extrapolations 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 concludes. The proofs of all the stated results can be found in [3].

2 Preliminaries

The cardinality of a set 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 ≫ N means that there exists j ∈ ℕ such that #(j, M) > #(j, N) and, for each k ∈ ℕ with k > j, we have #(k, M) = #(k, N). The relation ≫ satisfies the ascending chain condition [21]. The set of non-negative reals is denoted by ℝ_{+}.

Any vector v ∈ ℝ^{n} is also regarded as a matrix in ℝ^{n×1} so that it can be manipulated with the usual matrix operations of addition, multiplication (both by a scalar and by another matrix), and transposition, which is denoted by v^{T}. For each i = 1, … n, the i-th component of the vector v ∈ ℝ^{n} is denoted by v_{i}. The scalar product of v, w ∈ ℝ^{n}, denoted ⟨v, w⟩, is v^{T}w = ∑_{i=1}^{n} v_{i}w_{i}. The vector of ℝ^{n} having all components equal to zero is denoted by 0.

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: (1) positive (or conic), if λ_{i} ∈ ℝ_{+} for i = 1, …, k; (2) affine, if ∑_{i=1}^{k} λ_{i} = 1; (3) convex, if it is both positive and affine. 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 is V^{⊥} := { w ∈ ℝ^{n} | ∀v ∈ V : ⟨v, w⟩ = 0 }; the set { −v ∈ ℝ^{n} | v ∈ V } is denoted by −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.

We say that P ∈ ℂℙ_{n} has dimension k, and we write dim(P) = k, if k ≤ n is the dimension of the affine subspace aff.hull(P). If P ≠ ∅, the characteristic cone of P is given by the set

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 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.

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 ‘⪯’ 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_{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_{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 such that gen(G′) = gen(G).

Let c = (⟨a, x⟩ ▷◁ b) be a linear constraint, where ▷◁ ∈ {≥, =}. We say that a point (resp., a ray or a line) v saturates constraint c 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 ∈ C | p saturates c }; for each constraint c and generator system G = (L, R, P), we define the generator system sat gen(c, G) := (L′, R′, P′), where L′ := { l ∈ L | l saturates c }, R′ := { r ∈ R | r saturates c } and P′ := { p ∈ P | p saturates c }.

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 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 c = (⟨a, x⟩ ▷◁ b), let c_{a} = a. A constraint system C is in orthogonal form if it is in minimal form and I ⊆ E^{⊥}, where I := { c_{a} ∈ ℝ^{n} | c ∈ ineq(C) } and E := { c_{a} ∈ ℝ^{n} | c ∈ 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 polyhedra was introduced in [19]. 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 [23]. This operator, termed standard widening, has indeed been used almost universally. The specification in [23] requires that each equality constraint is split into the two corresponding 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.) [23, Définition 5.3.3, p. 57] For i = 1, 2, let P_{i} ∈ ℂℙ_{n} be such that P_{i} = con(C_{i}) [and let C_{1} be either inconsistent or in minimal form]. The polyhedron P_{1} ∇ P_{2} ∈ ℂℙ_{n} is defined by P_{1} ∇ P_{2} := P_{2} if P_{1} = ∅, and P_{1} ∇ P_{2} := con(C′_{1} ∪ C′_{2}) otherwise, where

C′_{1} := { β ∈ repr_{≥}(C_{1}) | P_{2} ⊆ con({β}) },
C′_{2} := { γ ∈ repr_{≥}(C_{2}) | ∃β ∈ repr_{≥}(C_{1}) . P_{1} = con((repr_{≥}(C_{1}) \ {β}) ∪ {γ}) }.

The constraints in C′_{1} are those that would have been selected when using the original proposal of [19], whereas the constraints in C′_{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 representations).

The condition in square brackets that C_{1}, when consistent, should be in minimal form, was implicit from the context of [23, 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 redundant (i.e., not minimal) constraint description is taken into account, then not only is the widening operator not well defined (see Example 1), but also the chain condition may be violated (see Example 2).

Example 1. 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 [23, Définition 5.3.3, p. 57] verbatim, without enforcing minimization, we would obtain the polyhedron con({x ≥ 0, y ≥ 0}). In contrast, by applying Definition 1, i.e., by enforcing minimization, we obtain the polyhedron con({y ≥ 0}).

Example 2. For each k ∈ ℕ, consider P_{k} := con(C_{k}) ∈ ℂℙ_{1}, where

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

Note that no C_{k} is in minimal form 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. It is simple to observe that, when computing the standard widening without enforcing minimization, for the infinite chain Q_{0} := P_{0}, …, Q_{k+1} := Q_{k} ∇ P_{k+1}, …, we have Q_{n} = P_{n} for each n ∈ ℕ, so that the chain condition is violated. This is because, by taking β = (x ≤ 2) ∈ C_{k}, any constraint γ ∈ C_{k+1} can replace β in C_{k} still obtaining polyhedron P_{k}.

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 [23] and later reported in [26], is to replace the expensive test in the specification of C′_{2} in Definition 1 with an appropriate saturation condition to be checked on any generator system for P_{1}. The algorithm here is an improved version over these proposals since neither the addition of the set of constraints C′_{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 [6, Chapter 6].

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

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

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

Example 3. 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 C′_{1} = C′_{2} = ∅, so that P_{1} ∇ 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 is P_{2}, which is different from P_{1} ∇ P_{2} and it is not an upper approximation of P_{1}.

To avoid problems such as the one above, in the following we adopt a minor variant of the classical definition of the widening operator given in Section 1 (see the footnote in [18, p. 275]).

Definition 2. 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. x ⊑ y implies y ⊑ x ∇ y for each x, y ∈ L;

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

It can be proved that, for any continuous operator F: L → L, the upward iteration sequence with widenings starting at x_{0} ∈ L 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 after a finite number of iterations [18]. Note that the widening is always applied to arguments x = x_{i} and y = x_{i} ⊔ F(x_{i}) satisfying x ⊑ y and x ≠ y. Thus, without loss of generality, in the following we will assume that the two argument polyhedra satisfy the strict inclusion hypothesis P_{1} ⊂ P_{2}.

4 Defining More Precise Widenings

In this section, elaborating on an idea originally proposed in [7], we will present a framework for the systematic definition of new and precise widening operators for polyhedra. In particular, we will state the theoretical result that will be used to ensure that all the instances of the framework are indeed widening operators. In order to do that, we need the following definition.

Definition 3. (Number of non-null coordinates of a vector.) Let 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 the relation ↷ ⊆ ℂℙ_{n} × ℂℙ_{n} incorporating a notion of, so to speak, “limited growth” or “growth that cannot be indefinite” (graphically, a descending parabola).

Definition 4. (↷ ⊆ ℂℙ_{n} × ℂℙ_{n}.) Let P_{1}, P_{2} ∈ ℂℙ_{n} be two polyhedra. Then P_{1} ↷ P_{2} if and only if P_{1} ⊂ P_{2} and either P_{1} = ∅ or at least one of the following conditions holds, where, for i = 1, 2, P_{i} is given by means of a constraint system C_{i} in minimal form and a generator system G_{i} = (L_{i}, R_{i}, P_{i}) in orthogonal form:

dim(P_{1}) < dim(P_{2});  (1)
dim(lin.space(P_{1})) < dim(lin.space(P_{2}));  (2)
# C_{1} > # C_{2};  (3)
# C_{1} = # C_{2} ∧ # P_{1} > # P_{2};  (4)
# C_{1} = # C_{2} ∧ # P_{1} = # P_{2} ∧ κ(R_{1}) ≫ κ(R_{2}).  (5)

Note that the ‘↷’ relation is well defined, since it does not depend on the particular constraint and generator representations chosen; in particular, the requirement that the G_{i} are in orthogonal form ensures that the computation of κ(R_{i}) is not ambiguous (see Section 2).

The next result incorporates the basic idea behind the overall approach.

Theorem 1. Let P_{0} ↷ P_{1} ↷ ⋯ ↷ P_{i} ↷ ⋯ be a chain of polyhedra in ℂℙ_{n}. Then the chain is finite.

The ‘↷’ relation is a variant of a similar notion of limited growth defined in [7, Theorem 3]. These two proposals are not formally comparable since neither relation refines the other. On one hand, in Definition 4, there are convergence criteria that were not considered in [7], namely conditions (3) and (5); on the other hand, to ensure that the relation satisfies the ascending chain condition, condition (4) also requires that the number of constraints is not increasing.

From a more practical point of view, the relation defined in [7] is unsatisfactory, since neither the standard widening ∇, nor the heuristics informally sketched in [7] ensure that consecutive iterates satisfy the given notion of limited growth. In summary, the overall approach does not define a widening operator in the precise sense of Definition 2 [F. Besson, personal communication, 2002]. By contrast, the introduction of condition (3) ensures that applications of ∇ always yield polyhedra that are related to previous iterates by the ‘↷’ relation.

Theorem 2. Let P_{1} ⊂ P_{2} ∈ ℂℙ_{n}. Then P_{1} ↷ P_{1} ∇ P_{2}.

This result provides a secure foundation for the definition of new widening operators such as the one proposed here. In fact, the next result, which is an easy consequence of Theorems 1 and 2, shows how any upper bound operator can be used as the basis of a new widening that improves on the standard one.

Theorem 3. Let h: ℂℙ_{n}^{2} → ℂℙ_{n} be an upper bound operator and

P_{1} ˜∇ P_{2} := \begin{cases}h(P_{1}, P_{2}), & if P_{1} ↷ h(P_{1}, P_{2}) ⊂ P_{1} ∇ P_{2}; \\ P_{1} ∇ P_{2}, & otherwise. \end{cases}

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

The above scheme is easily extended to any finite set of heuristic techniques that are upper bound operators, still obtaining a widening operator. In the following section we will consider several possible heuristic techniques: the simplest one, also adopted in [7], was actually suggested in [18]; the second one is based on an idea informally sketched in [7]; the third one is a minor variant of the extrapolation operator of [27]; the fourth and last one is new to this paper.

5 Improving the Standard Widening by Heuristics

First Technique: Do Not Widen. The simplest heuristic technique, already suggested in [18], 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} ↷ P_{2}. Consequently, all other techniques considered here will be applied to polyhedra P_{1} and P_{2} only if P_{1} ↷̸ P_{2} so that, by the inclusion hypothesis, dim(P_{1}) = dim(P_{2}) and dim(lin.space(P_{1})) = dim(lin.space(P_{2})).

Second Technique: Combining Constraints. When defining a widening operator on an abstract domain, a common tactic is to split the current abstract description into several components and look at each one in isolation so as to identify what has changed with respect to the previous iteration. Intuitively, the information provided by stable components should be propagated to the next iteration, whereas the information of components that have changed should be extrapolated according to a hypothetical “change pattern”. For instance, in the case of the widening in [19], each element of a constraint system is regarded as a separate component and the extrapolation just forgets about the constraints that have changed. The second heuristics, which is a variant of a similar one sketched in [7], 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^{3} 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 two points p and q in Figure 1. For each such point, the technique forces the presence of an inequality constraint that is saturated by the point, so that it lies on the boundary of the result.

Definition 5. (Combining constraints.) Let P_{1}, P_{2} ∈ ℂℙ_{n} be two polyhedra 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} ∇ P_{2} = con(C_{∇}), where the constraint

3 In this context, a “boundary point” is any point of P ∩ lin.space(P)^{⊥} which is not a relatively interior point for P. Namely, we abstract from both the affine hull and the lineality space of the polyhedron.

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

Fig. 1. The heuristics h_{c} improving on the standard widening.

systems C_{2} and C_{∇} and the generator system G_{1} = (L_{1}, R_{1}, P_{1}) are in orthogonal form. Let also

C_{⊕} := \{ ⊕(C_{p}) | \begin{matrix}p ∈ P_{1}, sat con(p, ineq(C_{∇})) = ∅, \\ C_{p} = 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_{∇} ∪ 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 considered representations.

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 [7] 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 C_{p} 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 condition (3) of Definition 4 will be met. Actually, this attempt at reducing the number of constraints is the main difference between the technique presented in Definition 5 and the extrapolation operator proposed in [29, Section 3.3], which could itself be included in the current framework as a more refined widening heuristics.

Third Technique: Evolving Points. Our third heuristic technique is a variant of the extrapolation operator ‘∝’ defined in [27]. 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 toward infinity, therefore generating the ray having direction p_{2} − p_{1}. The new ray will subsume point p_{2}, so that it is likely that the convergence condition (4) of Definition 4 will be met. Notice that any ray that violates a constraint of the standard widening is dropped.

Definition 6. (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} ∇ 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.

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 ‘↷’ relation and one can fail the ‘↷’ convergence criteria when the other succeeds.

Fourth Technique: Evolving Rays. We now introduce a fourth widening heuristics that tries to extrapolate the way rays 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 the convergence condition (5) of Definition 4 will be met. Intuitively, the new ray will reach one of the boundaries of the orthant where r_{2} lies, without trespassing it.

Definition 7. (evolve.) The function evolve: ℝ^{n}×ℝ^{n} → ℝ^{n} is defined, for each v, w ∈ ℝ^{n}, as evolve(v, w) := v′, where

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

To understand this definition consider a pair of coordinates i and j and suppose that the vectors v and w 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 (v_{i}, v_{j})^{T} with respect to the vector (w_{i}, w_{j})^{T} by using the well-known cross-product test [12, Chapter 35]; the direction is clockwise if cw := v_{i} · w_{j} − v_{j} · w_{i} > 0 and anti-clockwise when cw < 0. Moreover, vector (v_{i}, v_{j})^{T} lies inside the first or third quadrant when q := v_{i} ·v_{j} > 0 and it lies inside the second or fourth quadrant when q < 0. Then, the condition cw · q < 0 states that the evolution is clockwise and (v_{i}, v_{j})^{T} is in the second or fourth quadrant or the evolution is anti-clockwise and (v_{i}, v_{j})^{T} is in the first or third quadrant: in all these cases, the evolution is toward the j

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

Fig. 2. The heuristics h_{r} improving on the standard widening.

axis. Thus, for a fixed i, if there exists j such that the evolution is toward the j axis, then we define v′_{i} = 0. Otherwise, we let v′_{i} = v_{i}. We are now ready to define our last widening heuristics.

Definition 8. (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} ∇ P_{2}).

Figure 2 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} ∇ P_{2} contains the intersection of the boundaries of P_{1} and P_{2}, so that the ‘combining constraints’ technique is not applicable. Neither the ‘evolving points’ technique can be applied, since P_{1} and P_{2} have the same set of non-redundant 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 the same number of non-redundant constraints and points, so that P_{1} ↷ h_{r}(P_{1}, P_{2}) holds by condition (5) of Definition 4.

The New Widening. In order to use the above heuristic techniques in the general framework we have defined in the previous section, each of them needs to be an upper bound operator. This is trivial for the first technique. The same result holds, by construction, for the other three heuristics.

Proposition 2. 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} ∇ P_{2}.

The new widening operator tries to apply the four heuristics, stopping as soon as we obtain a result which ensures convergence and actually improves on the standard widening. As far as the choice of the particular order of application is concerned, in principle, the more precise heuristic techniques should be tried before the others; thus, the ‘do not widen’ technique has to be tried first. A preliminary experimental evaluation (which is not reported here) has shown that better results are obtained if the ‘combining constraints’ technique is tried before the ‘evolving points’ and ‘evolving rays’ techniques, whereas the ordering of the latter two is almost immaterial.

Definition 9. (The ˆ∇ widening.) Let P_{1}, P_{2} ∈ ℂℙ_{n}, where P_{1} ⊂ P_{2}. Then

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

It can be seen that ˆ∇ is an instance of the framework proposed in the previous section: in particular, when applying the first heuristics, the omission of the applicability condition P_{2} ⊂ P_{1} ∇ P_{2} is a simple and inconsequential optimization. Thus the following result is a direct consequence of Theorem 3 and Proposition 2.

Proposition 3. The ˆ∇ operator is a widening at least as precise as ∇.

Proposition 3 is not strong enough to ensure that the final results of upward iteration sequences using the new widening are uniformly more precise than those obtained by using the standard widening. It is well known, in fact, that the standard widening (and thus the new widening) is not a monotonic operator [19]. However, the experimental evaluation of the next section shows that, in practice, precision degradations are actually rare.

6 Experimental Evaluation

We have extended the Parma Polyhedra Library (PPL) [2, 4], a modern C^{++} library for the manipulation of convex polyhedra, with a prototype implementation of the widening of Definition 9. In particular, the operator ⊕ used for ‘combining constraints’ is the simple (i.e., non-normed) average: as the library uses arbitrary precision integers, the computation of norms may generate constraints having huge coefficients and it is therefore avoided. The PPL has been integrated with the China analyzer [1] for the purpose of detecting linear argument size relations [5]. 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 noted that China employs a sophisticated chaotic iteration strategy proposed in [8, 9] that, among other benefits, greatly reduces the number of widenings’ applications.^{4} This is an important point, since it would be quite easy

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

to improve on an iteration strategy applying widenings “everywhere or improperly” [8]. Also note that the polyhedra yielded by application of each of the two widening operators are strengthened by enforcing non-negativity constraints on all of the vector space dimensions, since the sizes of arguments cannot be negative: this further improvement is implemented by adopting the ‘widening up to’ technique of [24, 26]. The results of this experimental evaluation are summarized in Table 1, 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.

Precision  Time
# programs # predicates std ∇_{k} new ˆ∇_{k}
k (delay) improve degr incomp improve degr incomp all top 20 all top 20
0  121 0  2  1340 3  2 1.00 0.72 1.05 0.77
1  34 0  0  273 0  0 1.09 0.79 1.11 0.80
2  29 0  0  222 0  0 1.16 0.83 1.18 0.84
3  28 0  0  160 0  0 1.23 0.88 1.25 0.89
4  25 0  2  126 2  0 1.32 0.95 1.34 0.95
10  25 0  0  124 0  0 1.82 1.23 1.85 1.24

Table 1. Precision and time comparisons.

The part of the table headed ‘Precision’ shows the obtained precision improvements and degradations (in the columns labeled ‘improve’ and ‘degr’, respectively), 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 [5], 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 [13] maintains its validity: even though the new widening is less sensitive to the amount of delay applied, delaying still improves some of the results.

The part of the table headed ‘Time’ 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 Conclusion

For the domain of convex polyhedra, the convergence of the fixpoint computation sequence has been typically 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 applications in the fields of analysis and verification that are particularly sensitive to the precision of the deduced numerical information. In this paper, elaborating on an idea proposed in [7], we have defined a framework for the systematic specification of new widening operators improving on the precision of the standard widening. The framework allows any upper bound operator on the domain of convex polyhedra to be transformed into a proper widening operator, therefore ensuring the termination of the computation. We have instantiated the framework 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.

Acknowledgments. We would like to express our gratitude to Frédéric Besson for his useful comments and observations on the ideas sketched in [7]; 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 for their careful comments that helped us improve the paper.

References

1. R. Bagnara. Data-Flow Analysis for Constraint Logic-Based Languages. PhD thesis, Dipartimento di Informatica, Università di Pisa, Pisa, Italy, March 1997. Printed as Report TD-1/97.

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

3. R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella. Precise widening operators for convex polyhedra. Quaderno 312, Dipartimento di Matematica, Università di

    Parma, Italy, 2003. Available at http://www.cs.unipr.it/Publications/.

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. F. Benoy and A. King. Inferring argument size relationships with CLP(R). In J. P. Gallagher, editor, Logic Program Synthesis and Transformation: Proceedings of the 6th International Workshop, volume 1207 of Lecture Notes in Computer Science, pages 204–223, Stockholm, Sweden, 1997. Springer-Verlag, Berlin.

6. P. M. Benoy. Polyhedral Domains for Abstract Interpretation in Logic Programming. PhD thesis, Computing Laboratory, University of Kent, Canterbury, Kent, UK, January 2002.

7. F. Besson, T. P. Jensen, and J.-P. Talpin. Polyhedral analysis for synchronous languages. In A. Cortesi and G. Filé, editors, Static Analysis: Proceedings of the 6th International Symposium, volume 1694 of Lecture Notes in Computer Science, pages 51–68, Venice, Italy, 1999. Springer-Verlag, Berlin.

8. F. Bourdoncle. Efficient chaotic iteration strategies with widenings. In D. Bjørner, M. Broy, and I. V. Pottosin, editors, Proceedings of the International Conference on “Formal Methods in Programming and Their Applications”, volume 735 of Lecture Notes in Computer Science, pages 128–141, Academgorodok, Novosibirsk, Russia, 1993. Springer-Verlag, Berlin.

9. 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.

10. T. Bultan, R. Gerber, and 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):747–789, 1999.

11. M. A. Colón and H. B. Sipma. Synthesis of linear ranking functions. In T. Margaria and W. Yi, editors, Tools and Algorithms for Construction and Analysis of Systems, 7th International Conference, TACAS 2001, volume 2031 of Lecture Notes in Computer Science, pages 67–81, Genova, Italy, 2001. Springer-Verlag, Berlin.

12. T. H. Cormen, T. E. Leiserson, and R. L. Rivest. Introduction to Algorithms. The MIT Press, Cambridge, Mass., 1990.

13. P. Cousot. Semantic foundations of program analysis. In S. S. Muchnick and N. D. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 10, pages 303–342. Prentice-Hall, Inc., Englewood Cliffs, New Jersey, 1981.

14. P. Cousot, editor. Static Analysis: 8th International Symposium, SAS 2001, volume 2126 of Lecture Notes in Computer Science, Paris, France, 2001. Springer-Verlag, Berlin.

15. 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. Dunod, Paris, France, 1976.

16. 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.

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

18. 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.

19. 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.

20. G. Delzanno and A. Podelski. Model checking in CLP. In R. Cleaveland, editor, Tools and Algorithms for Construction and Analysis of Systems, 5th International Conference, TACAS ’99, volume 1579 of Lecture Notes in Computer Science, pages 223–239, Amsterdam, The Netherlands, 1999. Springer-Verlag, Berlin.

21. N. Dershowitz and Z. Manna. Proving termination with multiset orderings. Communications of the ACM, 22(8):465–476, 1979.

22. N. Dor, M. Rodeh, and S. Sagiv. Cleanness checking of string manipulations in C programs via integer analysis. In Cousot [14], pages 194–212.

23. 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, March 1979.

24. N. Halbwachs. Delay analysis in synchronous programs. In C. Courcoubetis, editor, Computer Aided Verification: Proceedings of the 5th International Conference, volume 697 of Lecture Notes in Computer Science, pages 333–346, Elounda, Greece, 1993. Springer-Verlag, Berlin.

25. N. Halbwachs, Y.-E. Proy, and P. Raymond. Verification of linear hybrid systems by means of convex approximations. In B. Le Charlier, editor, Static Analysis: Proceedings of the 1st International Symposium, volume 864 of Lecture Notes in Computer Science, pages 223–237, Namur, Belgium, 1994. Springer-Verlag, Berlin.

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

27. T. A. Henzinger and P.-H. Ho. A note on abstract interpretation strategies for hybrid automata. In P. J. Antsaklis, W. Kohn, A. Nerode, and S. Sastry, editors, Hybrid Systems II, volume 999 of Lecture Notes in Computer Science, pages 252– 264. Springer-Verlag, Berlin, 1995.

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

29. T. A. Henzinger, J. Preussig, and H. Wong-Toi. Some lessons from the hytech experience. In Proceedings of the 40th Annual Conference on Decision and Control, pages 2887–2892. IEEE Computer Society Press, 2001.

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

31. F. Mesnard and U. Neumerkel. Applying static analysis techniques for inferring termination conditions of logic programs. In Cousot [14], pages 93–110.

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