Widening Operators for Powerset Domains^{⋆}

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

1 Department of Mathematics, University of Parma, Italy

                     {bagnara,zaffanella}@cs.unipr.it

2 School of Computing, University of Leeds, UK

                          hill@comp.leeds.ac.uk

Abstract. The finite powerset construction upgrades an abstract domain by allowing for the representation of finite disjunctions of its elements. In this paper we define three generic widening operators for the finite powerset abstract domain. The widenings are obtained by lifting any widening operator defined on the base-level abstract domain and are parametric with respect to the specification of a few additional operators. We illustrate the proposed techniques by instantiating our widenings on powersets of convex polyhedra, a domain for which no non-trivial widening operator was previously known.

1 Introduction

The design and implementation of effective, expressive and efficient abstract domains for data-flow analysis and model-checking is a very difficult task. For this reason, starting with [12], there continues to be strong interest in techniques that derive enhanced abstract domains by applying systematic constructions on simpler, existing domains. Disjunctive completion, direct product, reduced product and reduced power are the first and most famous constructions of this kind [12]; several variations of them as well as others constructions have been proposed in the literature.

Once the carrier of the enhanced abstract domain has been obtained by one of these systematic constructions, the abstract operations can be defined, as usual, as the optimal approximations of the concrete ones. While this completely solves the specification problem, it usually leaves the implementation problem with the designer and gives no guarantees about the efficiency (or even the computability) of the resulting operations. This motivates the importance of generic techniques whereby correct, even though not necessarily optimal, domain operations are derived automatically or semi-automatically from those of the domains the construction operates upon [9, 12, 19].

This paper focuses on the derivation of widening operators for a kind of disjunctive refinement we call finite powerset construction. As far as we know, this

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

is the first time that the problem of deriving non-trivial, provably correct widening operators in a domain refinement is tackled successfully. We also present its specialization to finite powersets of convex polyhedra. Not only is this included to help the reader gain a better intuition regarding the underlying approach but also to provide a definitely non-toy instance that is practically useful for applications such as data-flow analysis and model checking. Sets of polyhedra are implemented in Polylib [25, 29] and its successor PolyLib [26], even though no widenings are provided. Sets of polyhedra, represented with Presburger formulas made available by the Omega library [24, 27], are used in the verifier described in [8]; there, an extrapolation operator (i.e., a widening without convergence guarantee) on sets of polyhedra is described. Another extrapolation operator is implemented in the automated verification tool described in [17], where sets of polyhedra are represented using the clp(q, r) constraint library [23].

The rest of the paper is structured as follows: Section 2 recalls the basic concepts and notations needed in this paper; Section 3 defines the finite powerset construction as a disjunctive refinement for any abstract domain that is a join-semilattice; Section 4 gives three alternative strategies for upgrading any widening for the base-level domain into a proper widening for the finite powerset domain; Section 5 shows a possible way to control the precision/efficiency tradeoff of these widenings. Section 6 concludes. Appendix A contains the proofs of all the stated results.

2 Preliminaries

For a set S, ℘(S) is the powerset of S, whereas ℘_{f}(S) is the set of all the finite subsets of S; the cardinality of S is denoted by # S. The first limit ordinal is denoted by ω. Let O be a set equipped with a well-founded ordering ‘≻’. If M and N are finite multisets over O, #(n, M) denotes the number of occurrences of n ∈ O in M and M ≫ N means that there exists j ∈ O such that #(j, M) > #(j, N) and, for each k ∈ O with k ≻ j, we have #(k, M) = #(k, N). The relation ‘≫’ is well-founded [18].

2.1 Abstract Interpretation

In the literature, several abstract interpretation frameworks have been proposed that are able to establish a formal relationship between the behaviors of programs when observed at different levels of abstraction. The main difference between these frameworks usually concerns the trade-off between their general applicability and the strength of the formal results that can be established. In this paper we will adopt the framework proposed in [14, Section 7], where the correspondence between the concrete and the abstract domains is induced from a concrete approximation relation and a concretization function. Since we are not aiming at maximum generality, for the sole purpose of simplifying the presentation, we will consider a particular instance of the framework by assuming a few additional but non-essential domain properties. The resulting construction will be adequate for our purposes, since it still allows for algebraically weak abstract domains.

The concrete domain is modeled as a complete lattice of semantic properties ⟨C, ⊑, ⊥, ⊤, ⊔, ⊓⟩; as usual, the concrete approximation relation c_{1} ⊑ c_{2} holds if c_{1} is a stronger property than c_{2} (i.e., c_{2} approximates c_{1}). The concrete semantics c ∈ C of a program is formalized as the least fixpoint of a continuous (concrete) semantic function F: C → C, which is iteratively computed starting from the bottom element, so that

c = F^{ω}(⊥) := ⨆_{δ<ω}(F^{δ}(⊥)).

The abstract domain D̂ = ⟨D, ⊢, 0, ⊕⟩ is modeled as a join-semilattice (i.e., the least upper bound d_{1} ⊕ d_{2} exists for all d_{1}, d_{2} ∈ D). We will overload ‘⊕’ so that, for each S ∈ ℘_{f}(D), ⨁S denotes the least upper bound of S. The abstract domain D̂ is related to the concrete domain by a monotonic and injective concretization function γ: D → C. Monotonicity and injectivity mean that the abstract partial order ‘⊢’ is indeed the approximation relation induced on D by the concretization function γ. For all d_{1}, d_{2} ∈ D, we will use the notation d_{1} ⊩ d_{2} to mean that d_{1} ⊢ d_{2} and d_{1} ≠ d_{2}. We assume the existence of a monotonic abstract semantic function F^{♯}: D → D that is sound with respect to F: C → C:

∀c ∈ C : ∀d ∈ D : c ⊑ γ(d) ⟹ F(c) ⊑ γ(F^{♯}(d)).  (1)

This local correctness condition ensures that each concrete iterate can be safely approximated by computing the corresponding abstract iterate (starting from the bottom element 0 ∈ D). However, due to the weaker algebraic properties satisfied by the abstract domain, the abstract upward iteration sequence may not converge. Even when it converges, it may fail to do so in a finite number of steps, therefore being useless for the purposes of static analysis.

Widening operators [10, 11, 14, 15] provide a simple and general characterization for enforcing and accelerating convergence. We will adopt a minor variation of the classical definition of widening operator (see footnote 6 in [15, p. 275]).

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

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

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

Any widening operator ‘∇’ induces a corresponding partial ordering ‘⊢_{∇}’ on the domain D; this is defined as the reflexive and transitive closure of the relation { (d_{1}, d) ∈ D × D | ∃d_{2} ∈ D . d_{1} ⊩ d_{2} ∧ d = d_{1} ∇ d_{2} }. The relation ‘⊢_{∇}’ satisfies the ascending chain condition. We write d_{1} ⊩_{∇} d_{2} to denote d_{1} ⊢_{∇} d_{2} and d_{1} ≠ d_{2}.

It can be proved that the upward iteration sequence with widenings starting at the bottom element d_{0} := 0 and defined by

d_{i+1} := \begin{cases}d_{i}, & if F^{♯}(d_{i}) ⊢ d_{i}, \\ d_{i} ∇ (d_{i} ⊕ F^{♯}(d_{i})), & otherwise, \end{cases}

converges after a finite number j ∈ ℕ of iterations [15]. Note that the widening is always applied to arguments d = d_{i} and d′ = d_{i} ⊕ F^{♯}(d_{i}) satisfying d ⊩ d′. Also, when condition (1) holds, the post-fixpoint d_{j} ∈ D of F^{♯} is a correct approximation of the concrete semantics, i.e., F^{ω}(⊥) ⊑ γ(d_{j}).

2.2 The Abstract Domain of Polyhedra

In this section, we instantiate the abstract interpretation framework sketched above by presenting the well-known abstract domain of closed convex polyhedra. This domain will be used throughout the paper to illustrate the generic widening techniques that will be defined.

Let ℝ^{n}, where n > 0, be the n-dimensional real vector space. The set P ⊆ ℝ^{n} is a closed and convex polyhedron (polyhedron, for short) if and only if P can be expressed as the intersection of a finite number of closed affine half-spaces of ℝ^{n}. The set ℂℙ_{n} of closed convex polyhedra on ℝ^{n}, when partially ordered by subset inclusion, is a lattice having the empty set and ℝ^{n} as the bottom and top elements, respectively; the binary meet operation is set-intersection, whereas the binary join operation, denoted by ‘⊎’, is called convex polyhedral hull (poly-hull, for short). Therefore, we have the abstract domain

ℂ̂ℙ_{n} := ⟨ℂℙ_{n}, ⊆, ∅, ℝ^{n}, ⊎, ∩⟩.

This domain can be related to several concrete domains, depending on the intended application. One example of a concrete domain is the complete lattice

Â_{n} := ⟨℘(ℝ^{n}), ⊆, ∅, ℝ^{n}, ∪, ∩⟩.

Note that ℂ̂ℙ_{n} is a meet-sublattice of Â_{n}, sharing the same bottom and top elements. Another example is the complete lattice

B̂_{n} := ⟨℘_{c}(ℝ^{n}), ⊆, ∅, ℝ^{n}, ∪_{c}, ∩⟩,

where ℘_{c}(ℝ^{n}) is the set of all topologically closed and convex subsets of ℝ^{n} and the join operation ‘∪_{c}’ returns the smallest topologically closed and convex set containing its arguments. Note that ℂ̂ℙ_{n} is a sublattice of B̂_{n}. As a final example of concrete domain for some analysis, consider the complete lattice

Ĉ_{n} := ⟨℘(ℂℙ_{n}), ⊆, ∅, ℂℙ_{n}, ∪, ∩⟩.

The abstract domain ℂ̂ℙ_{n}, which is a join-semilattice, is related to the concrete domains shown above by the concretization functions γ^{A} : ℂℙ_{n} → ℘(ℝ^{n}), γ^{B} : ℂℙ_{n} → ℘_{c}(ℝ^{n}) and γ^{C} : ℂℙ_{n} → ℘(ℂℙ_{n}): for each P ∈ ℂℙ_{n}, we have both γ^{A}(P) := P and γ^{B}(P) := P, and γ^{C}(P) := ↓ P := { Q ∈ ℂℙ_{n} | Q ⊆ P }. All these concretization functions are trivially monotonic and injective.

For each choice of the concrete domain C ∈ {℘(ℝ^{n}), ℘_{c}(ℝ^{n}), ℘(ℂℙ_{n})}, the continuous semantic function F: C → C and the corresponding monotonic abstract semantic function F^{♯}: ℂℙ_{n} → ℂℙ_{n}, which is assumed to be correct, are deliberately left unspecified. The domain ℂ̂ℙ_{n} contains infinite ascending chains having no least upper bound in ℂℙ_{n}. Thus, the convergence of the abstract iteration sequence has to be guaranteed by the adoption of widening operators.

2.3 Widening the Polyhedral Domain

The first widening on polyhedra was introduced in [16] and refined in [20]. This operator, denoted by ‘∇_{s}’, has been termed standard widening and used almost universally. Its formal specification requires some further notation and concepts related to the domain of polyhedra.

Any vector v ∈ ℝ^{n} is 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_{m}} ⊆ ℝ^{n} be a finite set of vectors. The orthogonal of V is

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

The vectors in V are said affinely independent if the only solution of the system of equations {∑_{i=1}^{m} λ_{i}v_{i} = 0, ∑_{i=1}^{m} λ_{i} = 0} is λ_{i} = 0, for each i = 1, …, m. 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.

For each vector a ∈ ℝ^{n} and scalar b ∈ ℝ, where a ≠ 0, the linear non-strict inequality constraint ⟨a, x⟩ ≥ b defines a topologically closed affine half-space of ℝ^{n}. 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). 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. Thus, each polyhedron P can be represented by a finite system of linear equality and non-strict inequality constraints C and we write P = con(C).

The subsets of equality and inequality constraints in C are denoted by eq(C) and ineq(C), respectively. When P = con(C) ≠ ∅, we say that C is in minimal form if and only if # eq(C) = n − dim(P) and there does not exist C′ ⊂ C such that con(C′) = P. All constraint systems in minimal form describing a given polyhedron have the same cardinality. For each linear constraint β of the form (⟨a, x⟩ ≥ b) or (⟨a, x⟩ = b), let slope(β) := a; for each constraint system C′, let slope(C′) := { slope(β) | β ∈ C′ }. A constraint system C is in orthogonal form if it is in minimal form and slope(ineq(C)) ⊆ slope(eq(C))^{⊥}. All constraint systems in orthogonal form describing a given polyhedron have identical sets of inequality constraints.

The following definition of 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 ∨ (⟨a, x⟩ = b) ∈ C }.

Definition 2. (Standard widening.) For i = 1, 2, let P_{i} = con(C_{i}) ∈ ℂℙ_{n}, where the constraint system C_{1} is 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(C′_{1} ∪ C′_{2}), & otherwise; \end{cases}

where

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

The constraints in C′_{1} are those that would have been selected when using the original proposal of [16], 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 second widening we summarize here is in fact a generalization of the framework presented in [4], which was based on an idea proposed in [7]. The framework is designed so that all its instances are indeed widening operators and it relies on a strict partial ordering relation on ℂℙ_{n} incorporating a notion of, so to speak, “limited growth” or “growth that cannot be indefinite” (graphically, a descending parabola).

Definition 3. (‘↷’.) For i = 1, 2, let P_{i} = con(C_{i}) ∈ ℂℙ_{n} where, if P_{i} ≠ ∅, C_{i} is in orthogonal form. The relation ↷_{s} ⊆ ℂℙ_{n} × ℂℙ_{n} is such that P_{1} ↷_{s} P_{2} if and only if P_{1} ⊂ P_{2} and either P_{1} = ∅ or at least one of the following holds:

dim(P_{1}) < dim(P_{2});  (2)
ineq(C_{1}) ⊃ ineq(C_{2}).  (3)

We denote by ‘↷’ any ordering on ℂℙ_{n} that is a refinement of ‘↷_{s}’ and satisfies the ascending chain condition.

Note that the orthogonality condition for the constraint systems of the polyhedra ensures that the relation ‘↷_{s}’ is well defined. Because of conditions (2) and (3) it can be shown that the application of ‘∇_{s}’ will always yield a polyhedron that is related to the previous iterate by any ‘↷’ ordering. That is, P_{1} ↷ P_{1} ∇_{s} P_{2} for any P_{1} ⊂ P_{2} ∈ ℂℙ_{n}.

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

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

By construction, ‘ ˜∇’ is an upper bound operator at least as precise as ‘∇_{s}’ and it still satisfies P_{1} ↷ P_{1} ˜∇ P_{2}.

In [4, 5], after defining a suitable refinement of the ‘↷_{s}’ ordering relation, an instance of the ‘ ˜∇’ widening schema is proposed that uses several extrapolation heuristics. For a formal definition of this improved widening operator, we refer the reader to [4].

3 A Disjunctive Refinement

Traditionally, semantic domains have been designed incrementally by applying suitable domain constructors to basic components. In this respect, the theory of abstract interpretation makes no exception and systematic ways of composing or enhancing abstract domains have been proposed since [12]. In this section, we present the finite powerset operator, which is a domain refinement similar to disjunctive completion [12] and is obtained by a variant of the down-set completion construction presented in [13]. The following notation and definitions are mainly borrowed from [2, Section 6].

Definition 4. (Non-redundancy.) Let D̂ = ⟨D, ⊢, 0, ⊕⟩ be a join-semilattice. The set S ∈ ℘(D) is called non-redundant with respect to ‘ ⊢’ if and only if 0 ∉ S and ∀d_{1}, d_{2} ∈ S : d_{1} ⊢ d_{2} ⟹ d_{1} = d_{2}. The set of finite non-redundant subsets of D (with respect to ‘ ⊢’) is denoted by ℘_{fn}(D, ⊢). The reduction function Ω_{D}^{⊢}: ℘_{f}(D) → ℘_{fn}(D, ⊢) mapping each finite set into its non-redundant counterpart is defined, for each S ∈ ℘_{f}(D), by

Ω_{D}^{⊢}(S) := S \ { d ∈ S | d = 0 ∨ ∃d′ ∈ S . d ⊩ d′ }.

The restriction to the finite subsets reflects the fact that here we are mainly interested in an abstract domain where disjunctions are implemented by explicit collections of elements of the base-level abstract domain. As a consequence of this restriction, for any S ∈ ℘_{f}(D) such that S ≠ {0}, Ω_{D}^{⊢}(S) is the (finite) set of the maximal elements of S.

Definition 5. (Finite powerset domain.) Let D̂ := ⟨D, ⊢, 0, ⊕⟩ be a joinsemilattice. The finite powerset domain over D̂ is the join-semilattice

D̂_{P} := ⟨℘_{fn}(D, ⊢), ⊢_{P}, 0_{P}, ⊕_{P}⟩,

where 0_{P} := ∅ and S_{1} ⊕_{P} S_{2} := Ω_{D}^{⊢}(S_{1} ∪ S_{2}).

The approximation ordering ‘⊢_{P}’ induced by ‘⊕_{P}’ is the Hoare powerdomain partial order [1], so that S_{1} ⊢_{P} S_{2} if and only if

∀d_{1} ∈ S_{1} : ∃d_{2} ∈ S_{2} . d_{1} ⊢ d_{2}.

A sort of Egli-Milner partial order relation [1] will also be useful: S_{1} ⊢_{EM} S_{2} holds if and only if either S_{1} = 0_{P} or S_{1} ⊢_{P} S_{2} and

∀d_{2} ∈ S_{2} : ∃d_{1} ∈ S_{1} . d_{1} ⊢ d_{2}.

An (Egli-Milner) connector for D̂_{P}, denoted by ‘ ⊞_{EM}’ is any upper bound operator for the Egli-Milner ordering on ℘_{fn}(D, ⊢). Note that although a least upper bound for ‘⊢_{EM}’ may not exist, a connector can always be defined; for instance, we can let S_{1} ⊞_{EM} S_{2} := {⨁(S_{1} ∪ S_{2})}.

Besides the requirement on finiteness, another difference with respect to the down-set completion of [13] is that we are dropping the assumption about the complete distributivity of the concrete domain. This is possible because our semantic domains are not necessarily related by Galois connections, so that this property does not have to be preserved.

The finite powerset domain is related to the concrete domain by means of the concretization function γ_{P} : ℘_{fn}(D, ⊢) → C defined by

γ_{P}(S) := ⨆{ γ(d) | d ∈ S }.

Note that γ_{P} is monotonic but not necessarily injective. For S_{1}, S_{2} ∈ ℘_{fn}(D, ⊢), we write S_{1} ≡_{γ_{P}} S_{2} to denote that the two abstract elements actually denote the same concrete element, i.e., when γ_{P}(S_{1}) = γ_{P}(S_{2}). It is easy to see that ‘≡_{γ_{P}}’ is a congruence relation on D̂_{P}. As noted in [13], non-redundancy only provides a partial, syntactic form of reduction. On the other hand, requiring the full, semantic form of reduction for a finite powerset domain can be computationally very expensive.

A correct abstract semantic function F ♯_{P} : ℘_{fn}(D, ⊢) → ℘_{fn}(D, ⊢) on the finite powerset domain may be provided by an ad-hoc definition. More often, if the concrete semantic function F: C → C satisfies suitable hypotheses, F ♯_{P} can be safely induced from the abstract semantic function F^{♯}: D → D. For instance, if F is additive, we can define F ♯_{P} as follows [12, 19]:

F ♯_{P}(S) := Ω_{D}^{⊢}({ F^{♯}(d) | d ∈ S }).

3.1 The Finite Powerset Domain of Polyhedra

The polyhedral domain (ℂ̂ℙ_{n})_{P}, having carrier ℘_{fn}(ℂℙ_{n}, ⊆), is the finite powerset domain over ℂ̂ℙ_{n}. The approximation ordering is ‘⊆_{P}’ where, for each S_{1}, S_{2} ∈ ℘_{fn}(ℂℙ_{n}, ⊆),

S_{1} ⊆_{P} S_{2} ⟺ ∀P_{1} ∈ S_{1} : ∃P_{2} ∈ S_{2} . P_{1} ⊆ P_{2}.

Let γ_{P}^{A}, γ_{P}^{B} and γ_{P}^{C} denote the (powerset) concretization functions induced by γ^{A}, γ^{B} and γ^{C}, respectively. Then, the relation ‘≡_{γ_{P}^{A}}’ makes two finite sets of polyhedra equivalent if and only if they have the same set-union. The general problem of deciding the semantic equivalence with respect to γ_{P}^{A} of two finite (non-redundant) collections of polyhedra is known to be computationally hard [28]. For γ_{P}^{B}, the relation ‘≡_{γ_{P}^{B}}’ makes two finite sets of polyhedra equivalent if and only if they have the same poly-hull, so that the powerset construction provides no benefit at all. Finally, γ_{P}^{C} is injective so that ‘≡_{γ_{P}^{C}}’ coincides with the identity congruence relation.

Example 1. For the polyhedral domain (ℂ̂ℙ_{1})_{P}, let^{3}

T_{0} := {{0 ≤ x ≤ 2}, {1 ≤ x ≤ 2}, {3 ≤ x ≤ 4}, {4 ≤ x ≤ 5}},
T_{1} := {{0 ≤ x ≤ 2}, {3 ≤ x ≤ 4}, {4 ≤ x ≤ 5}},
T_{2} := {{0 ≤ x ≤ 1}, {1 ≤ x ≤ 2}, {3 ≤ x ≤ 5}}.

Then T_{0} ∉ ℘_{fn}(ℂℙ_{1}, ⊆), but T_{1} = Ω_{ℂℙ_{1}}^{⊆}(T_{0}) ∈ ℘_{fn}(ℂℙ_{1}, ⊆). Also, T_{1} ≡_{γ_{P}^{A}} T_{2}.

4 Widening the Finite Powerset Domain

If the domain refinement of the previous section is meant to be used for static analysis, then a key ingredient that is still missing is a systematic way of ensuring the termination of the analysis. In this section, we describe three widening strategies that rely on the existence of a widening ∇: D × D ↣ D on the baselevel abstract domain. Note that this assumption is satisfied by most abstract domains used in the context of static analysis.^{4} We start by proposing a very general specification of an extrapolation operator that lifts this ‘∇’ operator to the powerset domain.

Definition 6. (h∇_{P}.) A partial operator h∇_{P} : ℘_{fn}(D, ⊢)^{2} ↣ ℘_{fn}(D, ⊢) is an extrapolation heuristics for D̂_{P} if, for all S_{1}, S_{2} ∈ ℘_{fn}(D, ⊢) such that S_{1} ⊩_{P} S_{2}, h∇_{P}(S_{1}, S_{2}) is defined and satisfies the following conditions:

S_{2} ⊢_{EM} h∇_{P}(S_{1}, S_{2});  (4)
∀d ∈ h∇_{P}(S_{1}, S_{2}) \ S_{2} : ∃d_{1} ∈ S_{1} . d_{1} ⊩_{∇} d.  (5)

Informally, condition (4) ensures that the result is an upper approximation of S_{2} in which every element covers at least one element of S_{2} (i.e., the heuristics cannot add elements that are unrelated to S_{2}); condition (5) ensures that in the resulting set, each element that was not already in S_{2} originates from an application of ‘∇’ to an element of S_{1}.

3 In this and the following examples, we will abuse notation by writing a constraint

system C to denote the polyhedron P = con(C). 4 If the base-level abstract domain D̂ is finite or Noetherian, so that it is not necessarily

endowed with an explicit widening operator, then a dummy widening can be obtained by considering the least upper bound operator ‘⊕’.

4.1 Powerset Widenings Using Egli-Milner Connectors

For the first widening, we require an additional property for the extrapolation heuristics; together with the previous conditions, this will ensure that each element of the resulting set that cover an element of the first argument S_{1} originates from an application of ‘∇’ to a (possibly different) element of S_{1}.

Definition 7. (∇-connected heuristics.) The extrapolation heuristics ‘h∇_{P}’ is said to be ∇-connected if, for all S_{1}, S_{2} ∈ ℘_{fn}(D, ⊢) where S_{1} ⊩_{P} S_{2}, we have

∀d ∈ h∇_{P}(S_{1}, S_{2}) ∩ S_{2} : ((∃d_{1} ∈ S_{1} . d_{1} ⊩ d) → (∃d′_{1} ∈ S_{1} . d′_{1} ⊩_{∇} d)). (6)

It is straightforward to construct an algorithm for computing a ∇-connected extrapolation heuristics for any given base-level widening ‘∇’. The basic idea was proposed in [8] for an abstract domain encoding a set of integer vectors by means of a Presburger formula. Intuitively, for all pairs (d_{1}, d_{2}) ∈ S_{1} × S_{2} that can be built using the two arguments S_{1} and S_{2}, we compute d_{1} ∇ d_{2}, provided this operation happens to be defined; otherwise, we simply take d_{2}.

Proposition 1. For all S_{1}, S_{2} ∈ ℘_{fn}(D, ⊢) such that S_{1} ⊢_{P} S_{2}, let

h∇_{P}(S_{1}, S_{2}) := S_{2} ⊕_{P} Ω_{D}^{⊢}({ d_{1} ∇ d_{2} ∈ D | d_{1} ∈ S_{1}, d_{2} ∈ S_{2}, d_{1} ⊩ d_{2} }).

Then ‘ h∇_{P}’ is a ∇-connected extrapolation heuristics for D̂_{P}.

For the finite powerset domain over ℂ̂ℙ_{n}, lines 10–15 of the algorithm specified in [8, Figure 8, page 773] provide an implementation of the heuristics ‘h∇_{P}’ defined in Proposition 1, instantiated with the standard widening, ‘∇_{s}’, on ℂ̂ℙ_{n}.

Example 2. To see that the ‘h∇_{P}’ defined in Proposition 1 is not a widening for (ℂ̂ℙ_{n})_{P}, consider the strictly increasing sequence T_{0} ⊆_{P} T_{1} ⊆_{P} ⋯ in ℂℙ_{1} defined by T_{j} := { P_{i} | 0 ≤ i ≤ j }, where P_{i} := {x = i}, for i ∈ ℕ. Then, no matter what the specification for ‘∇’ is, we obtain h∇_{P}(T_{j}, T_{j+1}) = T_{j+1}, for all j ∈ ℕ. Thus, the “widened” sequence is diverging.

Example 2 shows that, when computing h∇_{P}(S_{1}, S_{2}), divergence is caused by those elements of S_{2} that cover none of the elements occurring in S_{1}, i.e., when S_{1} ⊬_{EM} S_{2}. Thus, stabilization can be obtained by replacing S_{2} with S_{1} ⊞_{EM} S_{2}, where ‘ ⊞_{EM}’ is a connector for D̂_{P}. We therefore define a simple widening operator on the finite powerset domain that uses a connector to ensure termination.

Definition 8. (The ‘_{EM}∇_{P}’ widening.) Let ‘ h∇_{P}’ be a ∇-connected extrapolation heuristics and ‘ ⊞_{EM}’ be a connector for D̂_{P}. Let also S_{1}, S_{2} ∈ ℘_{fn}(D, ⊢), where S_{1} ⊩_{P} S_{2}. Then S_{1} _{EM}∇_{P} S_{2} := h∇_{P}(S_{1}, S′_{2}), where

S′_{2} := \begin{cases}S_{2}, & if S_{1} ⊢_{EM} S_{2}; \\ S_{1} ⊞_{EM} S_{2}, & otherwise. \end{cases}

Theorem 1. The ‘_{EM}∇_{P}’ operator is a widening on D̂_{P}.

Example 3. To illustrate the widening operator ‘_{EM}∇_{P}’ we consider the powerset domain (ℂ̂ℙ_{1})_{P}, with the standard widening ‘∇_{s}’ on ℂ̂ℙ_{1} and the trivial connector ‘⊎_{EM}’ returning the singleton poly-hull of its arguments. Consider the sequence T_{0} ⊆_{P} T_{1} ⊆_{P} ⋯ of Example 2 and the widened sequence U_{0} ⊆_{P} U_{1} ⊆_{P} ⋯ where U_{0} = T_{0} and U_{i} = U_{i−1} _{EM}∇_{P} (U_{i−1} ⊎_{P} T_{i}), for each i > 0. When computing U_{1}, the second argument of the widening is U_{0} ⊎_{P} T_{1} = T_{1}. Note that U_{0} ⊢_{EM} T_{1} does not hold so that the connector is needed. Thus, we obtain

U_{1} = h∇_{P}(U_{0}, U_{0} ⊎_{EM} T_{1}) = h∇_{P}(U_{0}, {{0 ≤ x ≤ 1}}) = {{0 ≤ x}}.

In the next iteration we obtain stabilization. Clearly, in general the precision of this widening will depend on the chosen connector operator.

4.2 Powerset Widenings using Set Cardinality

In the iteration sequence in Example 2, there is no finite upper bound on the cardinality of the set being widened. So in the second cardinality-based widening specified here, if the cardinality of the given set S_{2} exceeds a fixed bound k by some ℓ > 0, we first collapse S_{2} to a smaller set S′_{2} by replacing a subset of cardinality ℓ + 1 by its join (so that # S′_{2} ≤ k and S_{2} ⊢_{EM} S′_{2}).

Definition 9. (Collapsor.) The relation collapse_{k} ⊆ ℘_{fn}(D, ⊢) × ℘_{fn}(D, ⊢) is defined, for each k ≥ 1, so that collapse_{k}(S, S′) holds if and only if

S′ := \begin{cases}S, & if # S ≤ k; \\ (S \ S′′) ⊕_{P} \{⊕S′′\}, & otherwise, where S′′ ⊆ S and # S′′ > # S − k. \end{cases}

A unary operator ⇑_{k}: ℘_{fn}(D, ⊢) → ℘_{fn}(D, ⊢) is called a k-collapsor for D̂_{P} if collapse_{k}(S, ⇑_{k}(S)) holds.

The operator sketched in [8], which uses the ‘h∇_{P}’ heuristics defined in Proposition 1, is similar to the widening ‘_{EM}∇_{P}’ for the polyhedral domain ℂ̂ℙ_{n} but, instead of using a connector in the otherwise case in Definition 8, it assumes the use of an operator like the collapsor to limit the cardinality of the sets. However, such an approach is not enough to obtain a widening and, even when the cardinality of the set to be widened is fixed so that the collapsor is not required, termination cannot be guaranteed (see Example 11 in Appendix A). We therefore define a particular subclass of extrapolation heuristics for the cardinality-based widening that avoids the problem.

Definition 10. (∇-covered heuristics.) The extrapolation heuristics ‘ h∇_{P}’ is said to be ∇-covered if, for all S_{1}, S_{2} ∈ ℘_{fn}(D, ⊢) such that S_{1} ⊩_{P} S_{2}, we have

∀d_{1} ∈ S_{1} : ∃d ∈ h∇_{P}(S_{1}, S_{2}) . d_{1} ⊢_{∇} d.  (7)

A ∇-covered extrapolation heuristics can be obtained for any widening ‘∇’ on the base-level domain D̂. One possibility is to selectively replace the standard reduction map ‘Ω_{D}^{⊢}’ by a non-standard, widening-based reduction map ‘Ω_{D}^{∇}’. The idea being that if, in a set in ℘_{f}(D), one element d entails another d′, then instead of just removing the redundant element d, ‘Ω_{D}^{∇}’ replaces both d and d′ by their widening d ∇ d′.

Definition 11. (∇-reduction map.) An operator Ω_{D}^{∇}: ℘_{f}(D) → ℘_{fn}(D, ⊢) is a ∇-reduction map if, for all S ∈ ℘_{f}(D), there exists a sequence S_{0}, …, S_{m} of elements of ℘_{f}(D) such that S_{0} = S, S_{m} = Ω_{D}^{∇}(S) ∈ ℘_{fn}(D, ⊢) and, for each 0 < i ≤ m, S_{i} = (S_{i−1} \ {d, d′}) ∪ {d ∇ d′}, where d, d′ ∈ S_{i−1} and d ⊩ d′.

Proposition 2. For all S_{1}, S_{2} ∈ ℘_{fn}(D, ⊢) such that S_{1} ⊢_{P} S_{2}, let h∇_{P}(S_{1}, S_{2}) := Ω_{D}^{∇}(S_{1} ∪ S_{2}). Then ‘ h∇_{P}’ is a ∇-covered extrapolation heuristics for D̂_{P}.

We can now define the cardinality-based widening ‘_{k}∇_{P}’.

Definition 12. (The ‘_{k}∇_{P}’ widening.) Let ‘ h∇_{P}’ be a ∇-covered extrapolation heuristics and ‘ ⇑_{k}’ be a k-collapsor for D̂_{P}, for some k ≥ 1. Let also S_{1}, S_{2} ∈ ℘_{fn}(D, ⊢), where S_{1} ⊩_{P} S_{2}. Then S_{1} _{k}∇_{P} S_{2} := h∇_{P}(S_{1}, S′_{2}), where

S′_{2} := \begin{cases}S_{2}, & if # S_{2} ≤ k; \\ ⇑_{k}(S_{2}), & otherwise. \end{cases}

Theorem 2. The ‘_{k}∇_{P}’ operator is a widening on D̂_{P}.

Example 4. To illustrate the widening operator ‘_{k}∇_{P}’ for k = 2, we consider the powerset domain (ℂ̂ℙ_{1})_{P} with the standard widening ‘∇_{s}’ on ℂ̂ℙ_{1} and a 2collapsor that, given a non-redundant and finite set of intervals on the x-axis, reduces its cardinality to 2 by taking the poly-hull of all the intervals but the one having the smallest lower bound. Consider again the sequence T_{0} ⊆_{P} T_{1} ⊆_{P} ⋯ of Example 2 and the widened sequence U_{0} ⊆_{P} U_{1} ⊆_{P} ⋯ where U_{0} = T_{0} and U_{i} = U_{i−1} _{2}∇_{P} (U_{i−1} ⊎_{P} T_{i}), for each i > 0. As U_{0} ⊂ T_{1}, and # T_{1} = 2, we obtain U_{1} = T_{1}. Again U_{1} ⊂ T_{2}. As # T_{2} = 3, we compute ⇑_{2}(T_{2}) before applying an ‘h∇_{P}’ operator. Thus, we obtain

U_{1} = h∇_{P}(U_{1}, ⇑_{2}(T_{2})) = h∇_{P}(U_{1}, {{x = 0}, {1 ≤ x ≤ 2}}) = {{x = 0}, {1 ≤ x}}.

In the next iteration we obtain stabilization. Clearly, the precision of this widening will depend on the value of k.

4.3 Powerset Widenings Using Finite Convergence Certificates

When trying to prove that an upper bound operator ⊞: D × D → D is indeed a widening on the abstract domain D̂, a possible tactic is to provide a “convergence certificate.” Formally, a finite convergence certificate for ‘⊞’ (on D̂) is a triple (O, ≻, μ) where (O, ≻) is a well-founded ordered set and μ: D → O, which is called level mapping, is such that

∀d_{1}, d_{2} ∈ D : d_{1} ⊩ d_{2} ⟹ μ(d_{1}) ≻ μ(d_{1} ⊞ d_{2}).

We will abuse notation by writing μ to denote the certificate (O, ≻, μ).

We now present another widening operator (denoted here by ‘_{μ}∇_{P}’) for the finite powerset domain that requires that the base-level widening ‘∇’ is provided with a finitely computable certificate μ. The computability requirement is important because we will directly use this certificate in the implementation of the new widening. This is also the reason why we cannot directly infer such a certificate from the partial order relation ‘⊢_{∇}’, which in general does not come with a computability guarantee.

Example 5. For the polyhedral domain ℂ̂ℙ_{n} and the standard widening ‘∇_{s}’, a certificate μ can be inferred from any limited growth ordering relation ‘↷’ satisfying Definition 3, by letting

μ(P) ≻ μ(Q) ⟺ P ↷ Q,
μ(P) = μ(Q) ⟺ (P ↷̸ Q) ∧ (Q ↷̸ P).

An alternative and slightly simpler certificate (O_{s}, ≻_{s}, μ_{s}) can be directly provided by taking O_{s} to be the pair (ℕ, ℕ), ‘≻_{s}’ the lexicographic ordering of the pair using > for the individual ordering of the components and μ_{s}: ℂℙ_{n} → O_{s} be defined as the level mapping

μ_{s}(P) = (n − dim(P), # C),

where C is any constraint system in minimal form defining P.

For the widening operator ‘ ˆ∇’ on ℂ̂ℙ_{n} proposed in [4], a certificate can be obtained by considering the level mapping μ_{b}: ℂℙ_{n} → O_{b} induced, as shown above, by the specific limited growth ordering relation defined in [4].

Given a certificate μ for a widening ‘∇’ on D̂, we can define a suitable limited growth ordering relation ‘↷_{P}’ for the finite powerset domain D̂_{P} that satisfies the ascending chain condition.

Definition 13. (The ‘↷_{P}’ relation.) The relation ↷_{P} ⊆ ℘_{fn}(D, ⊢)×℘_{fn}(D, ⊢) induced by the certificate μ for ‘ ∇’ is such that, for each S_{1}, S_{2} ∈ ℘_{fn}(D, ⊢), S_{1} ↷_{P} S_{2} if and only if either one of the following conditions holds:

μ(⨁S_{1}) ≻ μ(⨁S_{2});  (8)
μ(⨁S_{1}) = μ(⨁S_{2}) ∧ # S_{1} > 1 ∧ # S_{2} = 1;  (9)
μ(⨁S_{1}) = μ(⨁S_{2}) ∧ # S_{1} > 1 ∧ # S_{2} > 1 ∧ μ̃(S_{1}) ≫ μ̃(S_{2}),  (10)

where, for each S ∈ ℘_{fn}(D, ⊢), μ̃(S) denotes the multiset over O obtained by applying μ to each abstract element in S.

Proposition 3. The ‘ ↷_{P}’ relation satisfies the ascending chain condition.

Intuitively, the relation ‘↷_{P}’ will induce a certificate μ_{P} : D̂_{P} → O_{P} for the new widening. Namely, by defining μ_{P}(S_{1}) ≻_{P} μ_{P}(S_{2}) if and only if S_{1} ↷_{P} S_{2}, we will obtain μ_{P}(S_{1}) ≻_{P} μ_{P}(S_{1} _{μ}∇_{P} S_{2}).

The specification of our “certificate-based widening” assumes the existence of a subtract operation for the base-level domain. It is expected that a specific subtraction would be provided for each domain; here we just indicate a minimal specification.

Definition 14. (Subtraction.) The partial operator ⊖: D × D ↣ D is a subtraction for D̂ if, for all d_{1}, d_{2} ∈ D such that d_{2} ⊢ d_{1}, we have d_{1} ⊖ d_{2} ⊢ d_{1} and d_{1} = (d_{1} ⊖ d_{2}) ⊕ d_{2}.

A trivial subtraction operator can always be defined as d_{1} ⊖d_{2} := d_{1}. In practice, when designing a widening, the actual subtraction operator would be expected to lose as little precision as possible.

Example 6. In ℂ̂ℙ_{n}, the function diff : ℂℙ_{n} × ℂℙ_{n} → ℂℙ_{n} is defined so that, for any P, Q ∈ ℂℙ_{n}, diff(P, Q) denotes the smallest closed and convex polyhedron containing the set difference P \ Q. Then, if Q ⊆ P, we have diff(P, Q) ⊆ P and

P = (P \ Q) ∪ Q
= diff(P, Q) ∪ Q
= diff(P, Q) ⊎ Q,

so that ‘diff’ is a subtraction.

We can now define the certificate-based widening ‘_{μ}∇_{P}’.

Definition 15. (The ‘_{μ}∇_{P}’ widening.) Let ‘ ↷_{P}’ be the limited growth ordering induced by the certificate μ for ‘ ∇’ and let ‘ ⊞_{P}’ be any upper bound operator on D̂_{P}. Let S_{1}, S_{2} ∈ ℘_{fn}(D, ⊢) be such that S_{1} ⊩_{P} S_{2}. Also, if ⨁S_{1} ⊩ ⨁(S_{1} ⊞_{P} S_{2}), let d ∈ D be defined as d := (⨁S_{1} ∇ ⨁(S_{1} ⊞_{P} S_{2})) ⊖ (⨁(S_{1} ⊞_{P} S_{2})). Then

S_{1} _{μ}∇_{P} S_{2} := \begin{cases}S_{1} ⊞_{P} S_{2}, & if S_{1} ↷_{P} S_{1} ⊞_{P} S_{2}; \\ (S_{1} ⊞_{P} S_{2}) ⊕_{P} \{d\}, & if ⨁S_{1} ⊩ ⨁(S_{1} ⊞_{P} S_{2}); \\ \{⨁S_{2}\}, & otherwise. \end{cases}

In the first case, we simply return the upper bound S_{1} ⊞_{P} S_{2}, since this is enough to ensure a strict decrease in the level mapping. In the second case, the join of S_{1} is strictly more precise than the join of S_{1} ⊞_{P} S_{2}, so that we apply ‘∇’ to them and then, using the subtraction operator, improve the obtained result, since S_{1} ↷_{P} (S_{1} ⊞_{P} S_{2}) ⊕_{P} {d} holds. In the last case, since the join of S_{1} is equivalent to the join of S_{1} ⊞_{P} S_{2}, we return the singleton consisting of the join itself, as originally proposed in [12, Section 9].

Theorem 3. The ‘_{μ}∇_{P}’ operator is a widening on D̂_{P}.

Example 7. To illustrate the last two cases of Definition 15, consider the domain (ℂ̂ℙ_{1})_{P}, with the standard widening ‘∇_{s}’ for ℂ̂ℙ_{1}, certified by the level mapping μ_{s} defined in Example 5 and the upper bound ‘⊞_{P}’ defined as ‘⊕_{P}’, so that we will always have S_{1} ⊞_{P} S_{2} = S_{2}.

Let T_{1} = {{0 ≤ x ≤ 1}} and T_{2} = {{0 ≤ x ≤ 1}, {2 ≤ x ≤ 3}}. Then T_{1} ↷̸_{P} T_{2}, so that the condition for the first case in Definition 15 does not hold. The poly-hulls of T_{1} and T_{2} are {0 ≤ x ≤ 1} and {0 ≤ x ≤ 3}, respectively, so that the condition for the second case holds. Since ⨄ T_{1} ∇_{s} ⨄ T_{2} = {0 ≤ x}, then by letting the polyhedron P be the element d as specified in Definition 15, we obtain P = diff({0 ≤ x}, {0 ≤ x ≤ 3}) = {3 ≤ x}, so that

T_{1} _{μ}∇_{P} T_{2} = T_{2} ⊎_{P} {P} = {{0 ≤ x ≤ 1}, {2 ≤ x ≤ 3}, {3 ≤ x}}.

Now let T_{3} = {{x = 1}, {x = 3}} and T_{4} = {{x = 1}, {x = 2}, {x = 3}}. Then T_{3} ↷̸_{P} T_{4}, so that the condition for the first case in Definition 15 does not hold. Moreover, ⨄ T_{3} = ⨄ T_{4} = {1 ≤ x ≤ 3}, so that neither the second case applies. Thus, T_{3} _{μ}∇_{P} T_{4} = {{1 ≤ x ≤ 3}}.

As shown in the example above, Definition 15 does not require that the upper bound operator ‘⊞_{P}’ is based on the base-level widening ‘∇’. Moreover, the scheme of Definition 15 can be easily extended to any finite set of heuristically chosen upper bound operators on D̂_{P}, still obtaining a proper widening operator for the powerset domain. The simplest heuristics, already used in the example above, is the one taking ⊞_{P} := ⊕_{P}. If this fails to ensure a decrease in the level mapping, another possibility is the adoption of an extrapolation heuristics ‘h∇_{P}’ for D̂_{P}. Anyway, many variations could be defined, depending on the required precision/efficiency trade-off. In the following section, we investigate one of these possibilities, which originates as a generalization of an idea proposed in [8].

5 Merging Elements According to a Congruence Relation

When computing a powerset widening S_{1} ∇_{P} S_{2}, no matter if it is based on an Egli-Milner connector, a k-collapsor, or a finite convergence certificate, some of the elements occurring in the second argument S_{2} can be merged together (i.e., joined) without compromising the finite convergence guarantee. This merging operation can be guided by a congruence relation on the finite powerset domain D̂_{P}, the idea being that a well-chosen relation will benefit the precision/efficiency trade-off of the widening.

One option is to use semantics preserving congruence relations, i.e., refinements of the congruence relation ‘≡_{γ_{P}}’. The availability of relatively efficient but incomplete tests for semantic equivalence can thus be exploited to improve the efficiency and/or the precision of the analysis. As the purpose of this paper is to provide generic widening procedures for powersets that are independent of the underlying domains and hence, of any intended concretizations, here we define these congruences in a way that is independent of the particular concrete domain adopted. Two such relations are the identity congruence relation, where no nontrivial equivalence is assumed, and the ⊕-congruence relation, where sets that have the same join are equivalent. Note that both these have the useful property that congruent elements have the same join. However, the identity congruence allows for no merging at all and hence it will have no influence on the convergence of the iteration sequence; on the other hand, the ⊕-congruence allows for a complete merging of the abstract collection and is usually the basis of the default, roughest heuristics for ensuring termination. We now define a congruence relation that lies between these extremes and still preserves the mentioned property.

Definition 16. (‘◁’ and ‘▷◁’.) The content relation ◁ ⊆ ℘_{fn}(D, ⊢) × ℘_{fn}(D, ⊢) is such that S_{1} ◁ S_{2} holds if and only if for all S′_{1} ∈ ℘_{fn}(D, ⊢) where S′_{1} ⊢_{P} S_{1} there exists S′′_{1} ∈ ℘_{fn}(D, ⊢) such that ⨁S′_{1} = ⨁S′′_{1} and S′′_{1} ⊢_{P} S_{2}. The samecontent relation ▷◁ ⊆ ℘_{fn}(D, ⊢) × ℘_{fn}(D, ⊢) is such that S_{1} ▷◁ S_{2} holds if and only if S_{1} ◁ S_{2} and S_{2} ◁ S_{1}.

Thus, for any S, S′ ∈ ℘_{fn}(D, ⊢), we have that S ⊢_{P} S′ implies that S ◁ S′ so that S ◁ {⨁S}, since S ⊢_{P} {⨁S}. Moreover, if S is a singleton, then S′ ⊢_{P} S if and only if S′ ◁ S. Note that ‘▷◁’ is a congruence relation on D̂_{P}.

Observe that the identity congruence relation can be obtained by strengthening the conditions in the definition of ‘◁’, replacing ⨁S′_{1} = ⨁S′′_{1} with S′_{1} = S′′_{1}; and the ⊕-congruence can be obtained by weakening the conditions, replacing S′′_{1} ⊢_{P} S_{2} with ⨁S′′_{1} ⊢ ⨁S_{2}. Thus the same-content relation is a compromise between keeping all the information provided by the explicit set structure, as done by the identity congruence, and losing all of this information, as occurs with the ⊕-congruence.

For the finite powerset domain of polyhedra (ℂ̂ℙ_{n})_{P}, the content relation ‘◁’ corresponds to the condition that all the points in polyhedra in the first set are contained by polyhedra in the second set; and hence, the same-content congruence relation ‘▷◁’ coincides with the induced congruence relation ‘≡_{γ_{P}^{A}}’.

Proposition 4. For all S_{1}, S_{2} ∈ ℘_{fn}(ℂℙ_{n}, ⊆), S_{1} ▷◁ S_{2} if and only if S_{1} ≡_{γ_{P}^{A}} S_{2}.

Example 8. For T_{1}, T_{2} ∈ ℘_{fn}(ℂℙ_{1}, ⊆) as defined in Example 1, we have T_{1} ▷◁ T_{2}. Consider also T_{3}, T_{4} ∈ ℘_{fn}(ℂℙ_{1}, ⊆) where

T_{3} := {{0 ≤ x ≤ 3}, {1 ≤ x ≤ 5}},  T_{4} := {{0 ≤ x ≤ 5}}.

Then T_{3} ▷◁ T_{4} and also T_{2} ◁ T_{4} although the converse does not hold. To see this, let S_{1}, S_{2}, and S′_{2} in Definition 16 be T_{2}, T_{4}, and T′_{4} := {{x = 2.5}}, respectively. Then, if T′′_{4} is such that ⨄ T′′_{4} = ⨄ T′_{4} and T′′_{4} ⊆_{P} T′_{4}, we must have T′′_{4} = T′_{4} ⊈_{P} T_{2}; hence, although T_{4} = {⨄ T_{2}}, we have T_{4} ⋪ T_{2}.

We now define an operation merger that is parametric with respect to the congruence relation and replaces selected subsets by congruent singleton sets.

O  T P_{2} P_{1}  P_{3}  ^{O  T ′ Q_{5} Q_{1} Q_{2} Q_{3} Q_{4}}

Fig. 1. Merging polyhedra according to ‘▷◁’.

Definition 17. (Merge and mergers.) Let R be a congruence relation on D̂_{P}. Then the merge relation merge_{R} ⊆ ℘_{fn}(D, ⊢) × ℘_{fn}(D, ⊢) for R is such that merge_{R}(S_{1}, S_{2}) holds if and only if S_{1} ⊢_{P} S_{2} and

∀d_{2} ∈ S_{2} : ∃S′_{1} ⊆ S_{1} . d_{2} = ⨁S′_{1} ∧ {d_{2}} R S′_{1}.

A set S ∈ ℘_{fn}(D, ⊢) is fully-merged for R, if merge_{R}(S, S′) implies S = S′; S is pairwise-merged for R if, for all d_{1}, d_{2} ∈ S, we have that {d_{1}, d_{2}} is fully-merged. An operator ↑_{R}: ℘_{fn}(D, ⊢) → ℘_{fn}(D, ⊢) is a merger for R if merge_{R}(S, ↑_{R} S) holds.

Observe that, for all S ∈ ℘_{fn}(D, ⊢), we have S ⊢_{EM} ↑_{R} S.

As R is a congruence relation on D̂_{P}, for any merger ‘↑_{R}’ for R and S ∈ D̂_{P}, S R (↑_{R} S) holds. For any congruence relation R on D̂_{P} that refines the ⊕- congruence relation, we can always merge a set to obtain one that is fully- or pairwise-merged.

Proposition 5. Let R be congruence relation on D̂_{P} that refines the ⊕-congru-ence relation. Then there exists a merger ‘ ↑_{R}’ such that, for all S ∈ ℘_{fn}(D, ⊢), ↑_{R} S is fully-merged (resp., pairwise-merged).

For the finite powerset domain over ℂ̂ℙ_{n}, lines 1–9 of the algorithm specified in [8, Figure 8, page 773] define a merger operator ‘↑_{▷◁}’ such that, for each finite set S of polyhedra, ↑_{▷◁} S is pairwise-merged.

Example 9. Figure 1 shows two examples of sets of polyhedra. In the left-hand diagram, the set T = {P_{1}, P_{2}, P_{3}} of three squares is not pairwise-merged for ‘▷◁’ since P_{1} ∪ P_{2} and P_{2} ∪ P_{3} are convex polyhedra. Both T_{1} = {P_{1} ∪ P_{2}, P_{3}} and T_{2} = {P_{1}, P_{2} ∪ P_{3}} are fully-merged and hence pairwise-merged for ‘▷◁’, and merge_{▷◁}(T , T_{i}) holds for i = 1, 2. In the right-hand diagram, the set T′ = {Q_{1}, Q_{2}, Q_{3}, Q_{4}, Q_{5}} is pairwise-merged but not fully-merged for ‘▷◁’. Since Q′ := ⋃ T′ is a convex polyhedron, the singleton set {Q′} is fully-merged and hence pairwise-merged for ‘▷◁’ and merge_{▷◁}(T′, {Q′}) holds.

6 Conclusion

We have studied the problem of endowing any abstract domain obtained by means of the finite powerset construction with a provably correct widening operator. We have proposed three generic widening operators and we have instantiated our techniques, which are completely general, on powersets of convex polyhedra, an abstract domain that is being used for static analysis and abstract model-checking and for which no non-trivial widening operator was previously known.

We have extended the Parma Polyhedra Library (PPL) [3, 6], a modern C^{++} library for the manipulation of convex polyhedra, with a prototype implementation of the certificate-based widening and its variant employing the ‘widening up to’ technique [21, 22]. The experimental work has just started, but the initial results obtained are very encouraging as our new widening compares favorably, both in terms of precision and efficiency, with the extrapolation operator of [8].

References

1. S. Abramsky and A. Jung. Domain theory. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 3, chapter 1, pages 1–168. Clarendon Press, Oxford, UK, 1994.

2. R. Bagnara. A hierarchy of constraint systems for data-flow analysis of constraint logic-based languages. Science of Computer Programming, 30(1–2):119–155, 1998.

3. 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.5 edition, April 2003. Available at http://www.cs.unipr.it/ppl/.

4. R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella. Precise widening operators for convex polyhedra. In R. Cousot, editor, Static Analysis: Proceedings of the 10th International Symposium, volume 2694 of Lecture Notes in Computer Science, pages 337–354, San Diego, California, USA, 2003. Springer-Verlag, Berlin.

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

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

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

9. A. Cortesi, B. Le Charlier, and P. Van Hentenryck. Combinations of abstract domains for logic programming: Open product and generic pattern construction. Science of Computer Programming, 38(1–3):27–71, 2000.

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

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

12. P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Proceedings of the Sixth Annual ACM Symposium on Principles of Programming Languages, pages 269–282, New York, 1979. ACM Press.

13. P. Cousot and R. Cousot. Abstract interpretation and applications to logic programs. Journal of Logic Programming, 13(2&3):103–179, 1992.

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

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

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

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

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

19. G. Filé and F. Ranzato. The powerset operator on abstract interpretations. Theoretical Computer Science, 222:77–111, 1999.

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

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

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

23. C. Holzbaur. OFAI clp(q,r) manual, edition 1.3.3. Technical Report TR-95-09, Austrian Research Institute for Artificial Intelligence, Vienna, 1995.

24. W. Kelly, V Maslov, W. Pugh, E. Rosser, T. Shpeisman, and D. Wonnacott. The Omega library interface guide. Technical Report CS-TR-3445, Department of Computer Science, University of Maryland, College Park, MD, USA, 1995.

25. H. Le Verge. A note on Chernikova’s algorithm. Publication interne 635, IRISA, Campus de Beaulieu, Rennes, France, 1992.

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

    able at http://icps.u-strasbg.fr/~loechner/polylib/, March 1999. Declares

itself to be a continuation of [29].

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

28. D. Srivastava. Subsumption and indexing in constraint query languages with linear arithmetic constraints. Annals of Mathematics and Artificial Intelligence, 8(3– 4):315–343, 1993.

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

A Proofs

Proof (of Proposition 1 on page 10). Let S := S_{2} ∪ Ω_{D}^{⊢}(S′), where

S′ := { d_{1} ∇ d_{2} ∈ D | d_{1} ∈ S_{1}, d_{2} ∈ S_{2}, d_{1} ⊩ d_{2} }.

Then, by hypothesis, h∇_{P}(S_{1}, S_{2}) = Ω_{D}^{⊢}(S). To prove that ‘h∇_{P}’ is a ∇-connected extrapolation heuristics for D̂_{P}, we need to prove that properties (4) and (5) of Definition 6 and property (6) of Definition 7 hold.

We first show that property (4) of Definition 6 holds. Suppose d_{2} ∈ S_{2}. Then, as S_{2} ⊆ S, we have d_{2} ∈ S. By Definition 4, there exists d′_{2} ∈ Ω_{D}^{⊢}(S) such that d_{2} ⊢ d′_{2}. Thus, by Definition 5, S_{2} ⊢_{P} h∇_{P}(S_{1}, S_{2}). Suppose next that d ∈ h∇_{P}(S_{1}, S_{2}) \ S_{2}. Then d ∈ Ω_{D}^{⊢}(S′) ⊆ S′, so that there exists d_{1} ∈ S_{1} and d_{2} ∈ S_{2} such that d = d_{1} ∇ d_{2}. Since ‘∇’ is a widening on D̂, d_{2} ⊢ d. Thus, it follows that S_{2} ⊢_{EM} h∇_{P}(S_{1}, S_{2}).

Secondly we show that property (5) of Definition 6 and property (6) of Definition 7 hold. Let d ∈ h∇_{P}(S_{1}, S_{2}) and d_{1} ∈ S_{1} be such that d_{1} ⊩ d.

We first suppose that d ∈ S_{2} and show that d ∈ S′. As d_{1} ⊩ d, d_{1} ∇ d is defined and is in S′. As ‘∇’ is a widening, d ⊢ d_{1} ∇ d. By Definition 4, there exists d′ ∈ Ω_{D}^{⊢}(S′) such that d_{1} ∇ d ⊢ d′. However Ω_{D}^{⊢}(S′) ⊆ S so that, again by Definition 4, there exists d′′ ∈ Ω_{D}^{⊢}(S) = h∇_{P}(S_{1}, S_{2}) such that d′ ⊢ d′′ and hence, by transitivity of ‘⊢’, d ⊢ d′′. Since d, d′′ ∈ h∇_{P}(S_{1}, S_{2}) ∈ ℘_{fn}(D, ⊢) we must have d = d′ = d′′ so that d ∈ S′.

Since, by hypothesis, h∇_{P}(S_{1}, S_{2}) ⊆ S_{2} ∪ S′ and, by the previous paragraph, d ∈ S_{2} implies that d ∈ S′, it follows that, in all cases, we must have d ∈ S′. Thus there exists d′_{1} ∈ S_{1} and d_{2} ∈ S_{2} such that d = d′_{1} ∇ d_{2} and hence d′_{1} ⊩_{∇} d. Therefore both properties (5) of Definition 6 and (6) of Definition 7 hold. ⊓ ⊔

Proof (of Theorem 1 on page 11). We first prove that that condition (1) in Definition 1 holds, i.e., that S_{2} ⊢_{P} S_{1} _{EM}∇_{P} S_{2}. Assume the notation and the hypotheses introduced in Definition 8 and let T := S_{1} _{EM}∇_{P} S_{2} = h∇_{P}(S_{1}, S′_{2}). By definition of ‘⊞_{EM}’, we have S_{2} ⊢_{EM} S_{1} ⊞_{EM} S_{2}. Thus, in both the cases of the definition of S′_{2}, we obtain S_{2} ⊢_{EM} S′_{2}, which implies S_{2} ⊢_{P} S′_{2}. Moreover, by Definition 6, S′_{2} ⊢_{P} T so that, by transitivity of ‘⊢_{P}’, S_{2} ⊢_{P} T.

We now prove condition (2) holds in Definition 1. Suppose T_{0} ⊢_{P} T_{1} ⊢_{P} ⋯ is an increasing chain of elements in ℘_{fn}(D, ⊢) and consider the widened sequence defined by U_{0} := T_{0} and, for each i > 0, U_{i} := U_{i−1}_{EM}∇_{P} (U_{i−1} ⊕_{P} T_{i}). As we have already shown that condition (1) in Definition 1 holds, (U_{i−1}⊕_{P}T_{i}) ⊢_{P} U_{i} so that, by transitivity of ‘⊢_{P}’, U_{i−1} ⊢_{P} U_{i}. Thus U_{0} ⊢_{P} U_{1} ⊢_{P} ⋯ is another increasing chain in ℘_{fn}(D, ⊢). We need to show that the widened sequence converges in a finite number of steps.

For each i > 0, consider the successive widened iterates U_{i−1} and U_{i}, so that, according to Definition 8, we can write U_{i} = h∇_{P}(U_{i−1}, S′_{2}), where in both the cases for the definition of S′_{2} we have U_{i−1} ⊢_{EM} S′_{2}. Since ‘h∇_{P}’ is a ∇-connected extrapolation heuristics, by property (4) of Definition 6, we have S′_{2} ⊢_{EM} U_{i} and, by transitivity of ‘⊢_{EM}’, U_{i−1} ⊢_{EM} U_{i}. Moreover, in the above context, the properties (5) of Definition 6 and (6) of Definition 7 can be rewritten to the simpler property:

∀d′ ∈ U_{i} : ∃d ∈ U_{i−1} . d ⊢_{∇} d′.  (11)

Let W_{i} ⊆ D × D be defined so that (d, d′) ∈ W_{i} holds if and only if d ∈ U_{i−1}, d′ ∈ U_{i} and d ⊩_{∇} d′. Thus, by property (11), we have

∀d′ ∈ U_{i} \ U_{i−1} : ∃d ∈ U_{i−1} . (d, d′) ∈ W_{i}.  (12)

For each i ∈ ℕ, consider the finite directed graph G_{i} = (V_{i}, E_{i}), where

– the set of vertices V_{i} ⊆ D is V_{i} := ⋃{ U_{j} | 0 ≤ j ≤ i };

– the set of edges E_{i} ⊆ V_{i} × V_{i} is E_{i} := ⋃{ W_{j} | 0 < j ≤ i }.

Furthermore, consider the (a priori, possibly infinite) graph G = (V, E) such that V = ⋃_{i≥0} V_{i} and E = ⋃_{i≥0} E_{i} = ⋃_{i≥1} W_{i}. We will now show that G is a finite and acyclic graph, so that, by property (12), ‘_{EM}∇_{P}’ is a widening. Namely, we will prove the following properties for the graph G, which combined together imply that G is a finite and acyclic graph:

1. G has no infinite paths;

2. G has a finite number of connected components;

3. G is finitely branching, i.e., each vertex has finite outdegree.

To prove G has no infinite paths, suppose p := d_{0} → d_{1} → ⋯ → d_{i} → ⋯ is a (possibly infinite) path in G. By the definition of G, if (d_{k−1}, d_{k}) is an edge in p for some k > 0, then there exists an index j > 0 such that (d_{k−1}, d_{k}) ∈ W_{j}. By definition of W_{j}, we know that d_{k−1} ⊩_{∇} d_{k}. Thus, we have a strictly increasing sequence d_{0} ⊩_{∇} d_{1} ⊩_{∇} ⋯ ⊩_{∇} d_{i} ⊩_{∇} ⋯ and hence, as ‘⊩_{∇}’ satisfies the ascending chain condition, the path p must be finite.

We now prove that the graph G has a finite number of connected components. Consider, for any i > 0 the graph G_{i} = (V_{i}, E_{i}). Then, by property (12), for each vertex d_{i} in V_{i} either d_{i} ∈ V_{i−1} or there is an edge (d_{i−1}, d_{i}) in E_{i} where d_{i−1} ∈ U_{i−1} ⊆ V_{i−1}. Thus, for all i ∈ ℕ, the number of components of G_{i} is no more than the number of components of G_{i−1}. As the number of components of G_{0} is # U_{0}, the number of components of G is no more than # U_{0}.

Finally, to prove that G is finitely branching, consider any vertex d ∈ V. Suppose that, for some index i > 0, there exists (d, d′) ∈ E_{i} \ E_{i−1} (note that (d, d′) ∉ E_{0} because E_{0} = ∅). Then (d, d′) ∈ W_{i}. Thus, by definition of W_{i}, d ∈ U_{i−1} and d′ ∈ U_{i} \ U_{i−1} and d ⊩ d′. However, for all indices j ≥ i, as U_{i} ⊢_{P} U_{j}, there exists d_{j} ∈ U_{j} such that d′ ⊢ d_{j} so that d ⊩ d_{j}; as U_{j} is a non-redundant set (in the sense of Definition 4), d ∉ U_{j}. Thus all outgoing edges from d are in E_{i}. As the set E_{i} is finite, d has a finite number of outgoing edges.

⊓ ⊔

Proof (of Proposition 2 on page 12). Let S = S_{1} ∪S_{2}, so that h∇_{P}(S_{1}, S_{2}) = Ω_{D}^{∇}(S). By Definition 11, there exists m ∈ ℕ and a sequence T_{0}, …, T_{m} in ℘_{f}(D) where T_{0} = S, T_{m} = Ω_{D}^{∇}(S) ∈ ℘_{fn}(D, ⊢) and, for each 0 < i ≤ m, there exists d, d′ ∈ T_{i−1} such that d ⊩ d′ and T_{i} = (T_{i−1} \ {d, d′}) ∪ {d ∇ d′}. Thus, for all d ∈ T_{i−1} there exists d′ ∈ T_{i} such that d ⊢_{∇} d′. We prove, for all 0 ≤ i ≤ m, the following properties hold:

∀d ∈ S_{2} : ∃d_{i} ∈ T_{i} . d ⊢ d_{i};  (13)
∀d_{i} ∈ T_{i} : ∃d ∈ S_{2} . d ⊢ d_{i};  (14)
∀d_{i} ∈ T_{i} \ S : ∃d ∈ S_{1} . d ⊩_{∇} d_{i};  (15)
∀d ∈ S_{1} : ∃d_{i} ∈ T_{i} . d ⊢_{∇} d_{i}.  (16)

Letting i = m in properties (13) and (14) we obtain S_{2} ⊢_{EM} Ω_{D}^{∇}(S), so that property (4) in Definition 6 holds. Since S_{1} ⊢_{P} S_{2} and T_{m} ∈ ℘_{fn}(D, ⊢), we have T_{m} \ S = T_{m} \ S_{2}; thus, letting i = m in property (15), we obtain that property (5) in Definition 6 holds. Thus ‘h∇_{P}’ is an extrapolation heuristics for D̂_{P}. Moreover, letting i = m in property (16), we obtain that property (7) in Definition 10 holds, so that ‘h∇_{P}’ is ∇-covered.

We now prove the four properties by induction on i. For the base case, we have i = 0 and T_{0} = S = S_{1} ∪S_{2}, so that all the properties hold trivially. For the inductive case, assuming that m > 0, consider an index j such that 0 < j ≤ m and all the properties hold for all i ≥ 0 where 0 ≤ i < j; we show they also hold when i = j. By Definition 11, if d_{j−1} ∈ T_{j−1}, then there exists d_{j} ∈ T_{j} such that either d_{j−1} = d_{j} or there exists d′_{j−1} ∈ T_{j−1} such that d_{j−1} ⊩ d′_{j−1} ≠ d_{j} and d_{j} = d_{j−1} ∇ d′_{j−1}; in both cases, d_{j−1} ⊢_{∇} d_{j}. Thus, assuming properties (13), (14), (15) and (16) hold for i = j − 1, they also hold for i = j. ⊓ ⊔

Proof (of Theorem 2 on page 12). We first prove that condition (1) holds in Definition 1, i.e., that S_{2} ⊢_{P} S_{1} _{k}∇_{P} S_{2}. Assume the notation and the hypotheses introduced in Definition 12 and let T := S_{1}_{k}∇_{P} S_{2} = h∇_{P}(S_{1}, S′_{2}). By Definition 9, S_{2} ⊢_{P} ⇑_{k}(S_{2}). Thus, in both the cases of the definition of S′_{2}, we obtain S_{2} ⊢_{P} S′_{2}. Moreover, by Definition 6, S′_{2} ⊢_{P} T so that, by transitivity of ‘⊢_{P}’, S_{2} ⊢_{P} T.

We now prove condition (2) holds in Definition 1. Suppose T_{0} ⊢_{P} T_{1} ⊢_{P} ⋯ is an increasing chain of elements in ℘_{fn}(D, ⊢) and consider the widened sequence defined by U_{0} := T_{0} and, for each i > 0, U_{i} := U_{i−1} _{k}∇_{P} (U_{i−1} ⊕_{P} T_{i}). As we have already shown that condition (1) in Definition 1 holds, (U_{i−1} ⊕_{P} T_{i}) ⊢_{P} U_{i} so that, by transitivity of ‘⊢_{P}’, U_{i−1} ⊢_{P} U_{i}. Thus U_{0} ⊢_{P} U_{1} ⊢_{P} ⋯ is another increasing chain in ℘_{fn}(D, ⊢).

For each i > 0, consider the successive widened iterates U_{i−1} and U_{i}. According to Definition 12, we have U_{i} = h∇_{P}(U_{i−1}, S′_{i}), where

S_{i} := U_{i−1} ⊕_{P} T_{i};
S′_{i} := \begin{cases}S_{i}, & if # S_{i} ≤ k; \\ ⇑_{k}(S_{i}), & otherwise. \end{cases}

By Definition 9, in both the cases for the definition of S′_{i}, we have U_{i−1} ⊢_{P} S′_{i} and # S′_{i} ≤ k. For an arbitrary j ∈ ℕ, let d_{j} ∈ U_{j}. Then, by condition (7) in Definition 10, there exists d_{j+1} ∈ U_{j+1} such that d_{j} ⊢_{∇} d_{j+1}. By transitivity, for all i > j, there exists d_{i} ∈ U_{i} such that d_{j} ⊢_{∇} d_{i}. As the ‘⊩_{∇}’ relation satisfies the ascending chain condition, there exist m ∈ ℕ and d_{m} ∈ U_{m} such that, for all i ≥ m, d_{m} ∈ U_{i}.

Suppose that the widening iteration does not converge in a finite number of steps. Then, by the point above, there must exist an index ℓ ∈ ℕ such that #(U_{ℓ−1} ∩ U_{ℓ}) = k. By definition of S′_{ℓ}, we have U_{ℓ−1} ⊢_{P} S′_{ℓ} ⊢_{P} U_{ℓ} and # S′_{ℓ} ≤ k. Thus, by Definition 4, we obtain both S′_{ℓ} = U_{ℓ−1} ∩ U_{ℓ} and U_{ℓ−1} = S′_{ℓ}. By condition (4) of Definition 6, we know that S′_{ℓ} ⊢_{EM} U_{ℓ}, so that U_{ℓ} = S′_{ℓ} = U_{ℓ−1}. Thus, the widening iteration converges, contradicting the assumption made at the beginning of this paragraph. ⊓ ⊔

In order to prove Proposition 3, we first define a minor variant (a coarsening) of the ‘↷_{P}’ relation and show that it satisfies the ascending chain condition.

Definition 18. (The ‘↷_{L}’ relation.) The relation ↷_{L} ⊆ ℘_{fn}(D, ⊢)×℘_{fn}(D, ⊢) induced by the certificate μ for ‘ ∇’ is such that, for each S_{1}, S_{2} ∈ ℘_{fn}(D, ⊢), S_{1} ↷_{L} S_{2} if and only if either one of the following conditions holds:

μ(⨁S_{1}) ≻ μ(⨁S_{2});
μ(⨁S_{1}) = μ(⨁S_{2}) ∧ μ̃(S_{1}) ≫ μ̃(S_{2}).

Lemma 1. The ‘↷_{L}’ relation on D̂_{P} satisfies the ascending chain condition.

Proof. By assumption, (O, ≻, μ) is a finite convergence certificate for the baselevel widening operator ‘∇’, so that ‘≻’ is a well-founded ordering on O. As noted in Section 2, letting M(O) denote the set of all the multisets having elements in O, the (strict) multiset ordering relation ≫ ⊆ M(O) × M(O) induced by ‘≻’ is also well-founded. As a consequence, the lexicographic product of ‘≻’ and ‘≫’ is a well-founded partial order relation on the product O × M(O). Note that, by Definition 18, S_{1} ↷_{L} S_{2} holds if and only if there is a strict decrease in this lexicographic product ordering, so that ‘↷_{L}’ satisfies the ascending chain condition. ⊓ ⊔

Proof (of Proposition 3 on page 14). Let S_{0} ↷_{P} S_{1} ↷_{P} ⋯ ↷_{P} S_{i} ↷_{P} ⋯ be a chain of abstract elements in the finite powerset domain D̂_{P}. In order to prove that the chain is finite, we will show that, for all indices i ∈ ℕ there exists j ∈ {i + 1, i + 2} such that S_{i} ↷_{L} S_{j}. The result will then be a consequence of Lemma 1.

Let i ∈ ℕ. Note that, by assumption, we have S_{i} ↷_{P} S_{i+1} ↷_{P} S_{i+2}. We distinguish three cases.

If S_{i} ↷_{P} S_{i+1} holds by virtue of condition (8) of Definition 13, then we have μ(⨁S_{i}) ≻ μ(⨁S_{i+1}), which implies S_{i} ↷_{L} S_{i+1}. Similarly, if S_{i} ↷_{P} S_{i+1} holds by virtue of condition (10) of Definition 13, then we have μ(⨁S_{i}) = μ(⨁S_{i+1}) and μ̃(S_{i}) ≫ μ̃(S_{i+1}), which again implies S_{i} ↷_{L} S_{i+1}. Thus, in these two cases we can take j := i + 1.

Otherwise, S_{i} ↷_{P} S_{i+1} must hold by virtue of condition (9) of Definition 13, so that μ(⨁S_{i}) = μ(⨁S_{i+1}) and # S_{i+1} = 1. However, S_{i+1} ↷_{P} S_{i+2} also holds and, by the above condition on the cardinality of S_{i+1}, this may only happen by virtue of condition (8) of Definition 13, so that μ(⨁S_{i+1}) ≻ μ(⨁S_{i+2}). Thus, μ(⨁S_{i}) = μ(⨁S_{i+1}) ≻ μ(⨁S_{i+2}) and, by taking j := i + 2, we obtain S_{i} ↷_{L} S_{j}. ⊓ ⊔

Proof (of Theorem 3 on page 14). Let S_{1}, S_{2} ∈ ℘_{fn}(D, ⊢), where S_{1} ⊩_{P} S_{2} and let T := S_{1} _{μ}∇_{P} S_{2}. We first prove that condition (1) in Definition 1 holds, i.e., S_{2} ⊢_{P} T. Consider each of the three cases in Definition 15 separately. If the first case applies, then T = S_{1} ⊞_{P} S_{2} and the result holds because, by hypothesis, ‘⊞_{P}’ is an upper bound operator on D̂_{P}. If the second case applies, then T = (S_{1} ⊞_{P} S_{2}) ⊕_{P} {d}. Since ‘⊕_{P}’ is the least upper bound operator, the result follows once again by the hypothesis on ‘⊞_{P}’. If the third and last case applies, then T = {⨁S_{2}}, so that the result holds trivially by definition of ‘⊢_{P}’.

We now prove that condition (2) in Definition 1 holds. By Proposition 3, ‘↷_{P}’ satisfies the ascending chain condition; hence, to complete the proof it is sufficient to show that S_{1} ↷_{P} T.

Consider each of the three cases in Definition 15. If the first case is applied, then the applicability conditions trivially ensure that S_{1} ↷_{P} T.

Suppose now the second case is applied, so that T = (S_{1} ⊞_{P} S_{2})⊕_{P} {d}, where

d := d_{1} ⊖ d_{2};
d_{1} := ⨁S_{1} ∇ ⨁(S_{1} ⊞_{P} S_{2});
d_{2} := ⨁(S_{1} ⊞_{P} S_{2}).

Note that the applicability condition ⨁S_{1} ⊩ ⨁(S_{1} ⊞_{P} S_{2}) for this case ensures that the required base-level widening application in the computation of the abstract element d_{1} ∈ D is well defined. Moreover, since ‘∇’ is an upper bound operator on D̂, we have d_{2} ⊢ d_{1}, so that also the subtraction application in the computation of the abstract element d ∈ D is well defined. By Definition 14, we

O  T_{0} = {P_{1}, P_{2}} P_{1}  P_{2}^{O T_{1} = {P_{1}, P_{2}, P_{3}} P_{1}  P_{2} P_{3}}  ^{O  P_{4}  P_{5} U_{1}T_{2} = {P_{4}, P_{5}}}

Fig. 2. The condition # U_{1} > 1 is needed to obtain a proper widening.

know that d_{1} = (d_{1} ⊖ d_{2}) ⊕ d_{2}. As a consequence, we obtain

⨁T = ⨁((S_{1} ⊞_{P} S_{2}) ⊕_{P} {d})
= d ⊕ (⨁(S_{1} ⊞_{P} S_{2}))
= d ⊕ d_{2}
= (d_{1} ⊖ d_{2}) ⊕ d_{2}
= d_{1}
= ⨁S_{1} ∇ ⨁(S_{1} ⊞_{P} S_{2}).

Since ‘μ’ is a certificate for the base-level widening ‘∇’, we obtain

μ(⨁S_{1}) ≻ μ(⨁S_{1} ∇ ⨁(S_{1} ⊞_{P} S_{2})) = μ(⨁T ),

so that by condition (8) of Definition 13, S_{1} ↷_{P} T.

Finally, if the last case is applied, then T = {⨁S_{2}} so that ⨁T = ⨁S_{2}. By hypothesis, since ‘⊞_{P}’ is an upper bound operator, we have S_{1} ⊩_{P} S_{2} ⊢_{P} S_{1}⊞_{P}S_{2}, so that we obtain ⨁S_{1} ⊢ ⨁S_{2} ⊢ ⨁(S_{1}⊞_{P}S_{2}). Since the condition for the second case of Definition 15 does not hold, we have ⨁S_{1} = ⨁(S_{1} ⊞_{P} S_{2}), which implies ⨁S_{1} = ⨁S_{2} = ⨁T and μ(⨁S_{1}) = μ(⨁T ). Also note that # T = 1 and, since S_{1} ⊩_{P} S_{2} ⊢_{P} T, it must be # S_{1} > 1. Therefore condition (9) of Definition 13 is satisfied and S_{1} ↷_{P} T. ⊓ ⊔

It should be noted that case (9) of Definition 13 has been introduced so as to ensure that S_{1} ↷_{P} {⨁S_{2}} holds in the last case of the specification of ‘_{μ}∇_{P}’, therefore inducing a strict decrease in the corresponding level mapping. This made also necessary the addition of the extra conditions on the cardinalities of S_{1} and S_{2} in case (10) of Definition 13, since otherwise we would have obtained a relation violating the ascending chain condition, as illustrated by the following example.

Example 10. Consider the finite powerset domain (ℂ̂ℙ_{2})_{P}, with the standard widening ‘∇_{s}’ on the base-level domain ℂℙ_{2}, certified by the level mapping ‘μ_{s}’ defined in Example 5 and the upper bound ‘⊞_{P}’ defined as ‘⊕_{P}’, so that we will always have S_{1} ⊞_{P} S_{2} = S_{2}. Consider an iteration sequence T_{0} ⊆_{P} T_{1} ⊆_{P} ⋯ starting with the sets of polyhedra illustrated in Figure 2, where T_{0} = {P_{1}, P_{2}} is shown in the top left diagram and T_{1} = T_{0} ⊎_{P} {P_{3}} is shown in the bottom left diagram. For the widened sequence, U_{0} := T_{0} and, since U_{0} ⊆_{P} T_{1}, we have to compute U_{1} := U_{0} _{μ}∇_{P} T_{1} = T_{0} _{μ}∇_{P} T_{1}. As ⨄ T_{0} = ⨄ T_{1}, # T_{1} > 1 and^{5}

μ̃_{s}(T_{0}) = {(0, 3)^{2}} ≫̸ {(0, 3)^{3}} = μ̃_{s}(T_{1}),

the last case applies in Definition 15 so that U_{1} = {⨄ T_{1}}, as is indicated in the lower square in the right-hand diagram of Figure 2. Now let T_{2} = {P_{4}, P_{5}} consist of the two triangles bounded by solid lines in the right-hand diagram. Note that U_{1} ⊆_{P} T_{2}, so that we have to compute the widened iterate U_{2} := U_{1} _{μ}∇_{P} T_{2}. Since

μ_{s}(⨄ U_{1}) = (0, 4) = μ_{s}(⨄ T_{2})

but

μ̃_{s}(U_{1}) = {(0, 4)^{1}} ≫ {(0, 3)^{2}} = μ̃_{s}(T_{2}),

without the extra condition # U_{1} > 1 in case (10) of Definition 13, we would have U_{1} ↷_{P} T_{2}. Thus, we would apply the first case in the definition of ‘_{μ}∇_{P}’, obtaining U_{2} = T_{2}. However, it is easy to note that U_{2} = T_{2} has the same structure of U_{0} = T_{0} (the former can be obtained from the latter by a suitable affine image transformation) so that the sequence T_{i} and the corresponding “widened” sequence U_{i} can be extended indefinitely without obtaining convergence (in a finite number of steps). In contrast, since we require the condition # U_{1} > 1, the second case of Definition 15 applies and U_{1}_{μ}∇_{P} T_{2} is the (unbounded) polyhedron indicated by the dotted lines in the right-hand diagram.

Proof (of Proposition 4 on page 16). The finite powerset domain (ℂ̂ℙ_{n})_{P} is related to the concrete domain Â_{n} defined in Section 2.2 by the concretization function γ_{P}^{A} induced from γ^{A}, where γ^{A}(P) = P for each P ∈ ℂℙ_{n}. Namely, for each S ∈ ℘_{fn}(ℂℙ_{n}, ⊆), we have γ_{P}^{A}(S) = ⋃ S. Therefore, we have to show that, for all S_{1}, S_{2} ∈ ℘_{fn}(ℂℙ_{n}, ⊆), S_{1} ▷◁ S_{2} if and only if ⋃ S_{1} = ⋃ S_{2}.

First we assume that ⋃ S_{1} ⊆ ⋃ S_{2} and show that S_{1} ◁ S_{2}. Consider an arbitrary element S′_{1} ∈ ℘_{fn}(ℂℙ_{n}, ⊆) such that S′_{1} ⊢_{P} S_{1}. Let

S′′_{1} = Ω_{ℂℙn}^{⊆}({ P′_{1} ∩ P_{2} ∈ ℂℙ_{n} | P′_{1} ∈ S′_{1}, P_{2} ∈ S_{2} })

5 In this example a multiset is denoted as a set where each element carries in a superscript the corresponding number of occurrences. For instance, we write M = {a^{3}, b^{2}} to mean that element a and b occur (in multiset M) 3 and 2 times, respectively.

so that ⋃ S′′_{1} = ⋃ S′_{1} ∩ ⋃ S_{2}. By definition, S′_{1} ⊢_{P} S_{1} implies ⋃ S′_{1} ⊆ ⋃ S_{1}; also, by hypothesis, ⋃ S_{1} ⊆ ⋃ S_{2}, so that ⋃ S′_{1} ⊆ ⋃ S_{2}. Therefore ⋃ S′′_{1} = ⋃ S′_{1} and ⋃ S′′_{1} ⊆ ⋃ S_{2}. Thus, by Definition 16, S_{1} ◁ S_{2}. By a symmetric argument, we can prove that ⋃ S_{2} ⊆ ⋃ S_{1} implies S_{2} ◁ S_{1}. Thus, again by Definition 16, we obtain that S_{1} ≡_{γ_{P}^{A}} S_{2} implies S_{1} ▷◁ S_{2}.

Second we assume that ⋃ S_{1} ⊈ ⋃ S_{2} and show that S_{1} ⋪ S_{2}. By assumption, there exist a point p ∈ ℝ^{n} such that p ∈ (⋃ S_{1}) \ (⋃ S_{2}). As a consequence, there must exist a polyhedron P_{1} ∈ S_{1} such that p ∈ P_{1}. Consider now the polyhedron P′_{1} := {p} and the corresponding singleton S′_{1} = {P′_{1}}. Note that S′_{1} ⊢_{P} S_{1}. Moreover, if S′′_{1} ∈ ℘_{fn}(ℂℙ_{n}, ⊆) is such that ⨄ S′′_{1} = ⨄ S′_{1}, then we must have S′′_{1} = S′_{1}. However, since p ∉ ⋃ S_{2}, we also have ⋃ S′′_{1} ⊈ ⋃ S_{2}, which implies S′′_{1} ⊬_{P} S_{2}. Hence, by Definition 16, S_{1} ⋪ S_{2}. By a symmetric argument, we can prove that ⋃ S_{2} ⊈ ⋃ S_{1} implies S_{2} ⋪ S_{1}. Thus, reasoning by contraposition, we obtain that S_{1} ▷◁ S_{2} implies S_{1} ≡_{γ_{P}^{A}} S_{2}. ⊓ ⊔

To prove Proposition 5 on page 17, it is convenient to consider non-redundant merges, where each of the elements in the original abstract collection participates to just one join operation.

Definition 19. Let R be a congruence relation on D̂_{P}. Let S_{1}, S_{2} ∈ ℘_{fn}(D, ⊢), where S_{2} = {d_{1}, …, d_{m}} and {S_{1i}}_{i=1}^{m} is a partition of S_{1} such that, for each 1 ≤ i ≤ m, merge_{R}(S_{1i}, {d_{i}}) holds. Then we write merge n_{R}(S_{1}, S_{2}) and say that S_{2} is a non-redundant merge of S_{1}.

Lemma 2. Let R be a congruence relation on D̂_{P} that refines the ⊕-congruence relation. If S_{1}, S_{2} ∈ ℘_{fn}(D, ⊢) where S_{1} ≠ S_{2} and merge_{R}(S_{1}, S_{2}), then there exists S′_{2} ≠ S_{1} ∈ ℘_{fn}(D, ⊢) such that merge n_{R}(S_{1}, S′_{2}) and # S′_{2} < # S_{1}.

Proof. By hypothesis, merge_{R}(S_{1}, S_{2}) and S_{1} ≠ S_{2}. Thus, by Definition 17, there exists S′_{1} ⊆ S_{1} where S′_{1} R {d_{2}} and {d_{2}} ≠ S′_{1}. Since R refines the ⊕-congruence relation, we obtain d_{2} = ⨁S′_{1}. Thus # S′_{1} > 1. Let S′_{2} = (S_{1} \ S′_{1}) ⊕_{P} {d_{2}}. Then S′_{2} ≠ S_{1}, # S′_{2} < # S_{1} and, by Definition 17, merge_{R}(S_{1}, S′_{2}). If S_{1} \ S′_{1} ≠ ∅, then {S_{1} \ S′_{1}, S′_{1}} is a partition of S_{1}; otherwise, {S′_{1}} is such a partition. In both cases, by Definition 19, merge n_{R}(S_{1}, S′_{2}). ⊓ ⊔

Proof (of Proposition 5 on page 17). We first prove, by induction on # S, that there exists S′ ∈ ℘_{fn}(D, ⊢) such that merge_{R}(S, S′), S′ is fully-merged and, if S′ ≠ S, then # S′ < # S. As ‘ merge_{R}’ is reflexive, the result holds trivially if S is fully-merged. Suppose therefore that S is not fully-merged (so that # S > 1). Then there exists S′′ ∈ ℘_{fn}(D, ⊢) \ {S} such that merge_{R}(S, S′′). By Lemma 2, we can assume that S′′ is chosen so that merge n_{R}(S, S′′) and # S′′ < # S. Therefore we can apply the inductive hypothesis to S′′; there exists S′ ∈ ℘_{fn}(D, ⊢) which is fully-merged, merge_{R}(S′′, S′) and # S′ ≤ # S′′. As ‘ merge_{R}’ is transitive, we obtain merge_{R}(S, S′) and # S < # S′.

The merger ‘↑_{R}’ can thus be defined, for each S ∈ ℘_{fn}(D, ⊢), as ↑_{R} S = S, when S is already fully-merged, and ↑_{R} S = S′ as defined above, otherwise. The proof for a pairwise-merger is similar. ⊓ ⊔

O  T_{2} = {P_{2}, P_{3}} P_{3} P_{4} P_{2}  O  T_{3} = {P_{2}, P_{4}} P_{4} P_{2}^{O T_{0} = {P_{0}} P_{0}  P′_{0}}  ^{O  T_{1} = {P_{1}, P_{3}} P_{3} P_{1}}

Fig. 3. Sequence of sets of polyhedra in Example 11.

The following example shows that, in general, it is not possible to obtain a proper widening operator on the finite powerset domain by coupling an arbitrary (i.e., not ∇-covered) extrapolation heuristics ‘h∇_{P}’ with a fixed upper bound for the cardinality of abstract descriptions. It is also shown that even the addition of a merger operator for abstract descriptions, as proposed in [8], is not enough for that purpose.

Example 11. Consider the finite powerset domain (ℂ̂ℙ_{2})_{P}, with ‘∇_{s}’ as the widening on the base-level abstract domain ℂ̂ℙ_{2}, ‘h∇_{P}’ be the extrapolation heuristics for ‘∇_{s}’ defined in Proposition 1 (which is also the one used in [8]) and ‘↑_{▷◁}’ be the pairwise-merging operator defined in [8]. Let P_{0}, P_{1}, P_{2}, P_{3}, P_{4} ∈ ℂℙ_{2} be defined as

P_{0} = {0 ≤ x ≤ 4, 0 ≤ y ≤ 4, x − y ≤ 3, x + y ≥ 1},
P_{1} = {0 ≤ x ≤ 4, 0 ≤ y ≤ 4, x − y ≤ 3},
P_{2} = {0 ≤ x ≤ 4, 0 ≤ y ≤ 4},
P_{3} = {0 ≤ x ≤ 8, 0 ≤ y ≤ 8, x + y ≤ 14, x − y ≥ −6, 5x − y ≥ −2, x + 3y ≥ 3},
P_{4} = {0 ≤ x ≤ 8, 0 ≤ y ≤ 8, x + y ≤ 14, x − y ≥ −6, 4x − y ≥ −3, x + 2y ≥ 2}.

Note that P_{1} = P_{0} ∇_{s} P_{1} and P_{2} = P_{1} ∇_{s} P_{2}; moreover, for all i ∈ {0, 1, 2}, we have P_{i} ⊈ P_{3} and P_{i} ⊈ P_{4}.

Consider an increasing sequence T_{0} ⊢_{P} T_{1} ⊢_{P} T_{2} ⊢_{P} T_{3} ⊢_{P} … starting with elements T_{0} = {P_{0}}, T_{1} = {P_{1}, P_{3}}, T_{2} = {P_{2}, P_{3}}, and T_{3} = {P_{2}, P_{4}}. Then, the corresponding widened sequence U_{0} ⊢_{P} U_{1} ⊢_{P} U_{2} ⊢_{P} U_{3} ⊢_{P} …, will be computed as follows. Since U_{0} = T_{0}, in the first iteration (noting that T_{1} is fully-merged) we compute

U_{1} = h∇_{P}(U_{0}, T_{1})
= {P_{3}} ⊎_{P} {P_{0} ∇_{s} P_{1}}
= {P_{1}, P_{3}}
= T_{1}.

In the second iteration, noting that also T_{2} is fully-merged, we obtain

U_{2} = h∇_{P}(U_{1}, T_{2})
= {P_{3}} ⊎_{P} {P_{1} ∇_{s} P_{2}}
= {P_{2}, P_{3}}
= T_{2}.

In the third iteration, since also T_{3} is fully-merged, letting

P′_{0} := P_{3} ∇_{s} P_{4} = {0 ≤ x ≤ 8, 0 ≤ y ≤ 8, x + y ≤ 14, x − y ≥ −6},

we obtain

U_{3} = h∇_{P}(U_{2}, T_{3})
= {P_{2}} ⊎_{P} {P_{3} ∇_{s} P_{4}}
= {P_{3} ∇_{s} P_{4}}
= {P′_{0}}.

Note that the polyhedron P_{2} does not occur in U_{3} because it is made redundant by the polyhedron P′_{0} (i.e., P_{2} ⊆ P′_{0}).

Now, the singleton U_{3} = {P′_{0}} has the same structure as the singleton U_{0} = {P_{0}}, because the polyhedron P′_{0} can be obtained from P_{0} by a scaling (by a factor 2) followed by a rotation. As a consequence, it is possible to indefinitely extend the sequence T_{i} and the corresponding “widened” sequence U_{i} without obtaining convergence (in a finite number of steps). Since in the above computation all the abstract elements have cardinality less than or equal to 2, the addition of any (non-trivial) upper bound on the cardinality of the abstract descriptions will have no effect on termination.

Suppose now that, instead of just using the extrapolation heuristics ‘h∇_{P}’, we adopt the widening ‘_{EM}∇_{P}’ with the trivial connector:

S_{1} ⊞_{EM} S_{2} := {⨁(S_{1} ∪ S_{2})}.

Let U′_{0} ⊢_{P} U′_{1} ⊢_{P} U′_{2} ⊢_{P} U′_{3} ⊢_{P} …, be the corresponding widened sequence. Then instead of obtaining U_{1} = {T_{1}} we obtain U′_{1} = {{x ≥ 0, y ≥ 0}}. Further iterations leave this set unchanged.

Suppose now that, instead of using the extrapolation heuristics ‘h∇_{P}’ defined in Proposition 1, we adopt one that is ∇-covered, such as that defined in Proposition 2, and hence use a cardinality-based widening ‘_{k}∇_{P}’ for any k > 2. Then we obtain the widened sequence U′′_{0} ⊢_{P} U′′_{1} ⊢_{P} U′′_{2} ⊢_{P} …, where U′′_{0} = U_{0}, U′′_{1} = U_{1} and U′′_{2} = U_{2} would be computed as before. However in the third iteration we will obtain

U′′_{3} = h∇_{P}(U_{2}, T_{3})
= Ω_{D}^{∇}({P_{2}, P_{3}, P_{4}})
= Ω_{D}^{∇}({P_{2}, P_{3} ∇_{s} P_{4}})
= Ω_{D}^{∇}({P_{2}, P′_{0}})
= {P_{2} ∇_{s} P′_{o}}
= {{x ≥ 0, y ≥ 0}},

which is the same as the set U′_{1} computed using ‘_{EM}∇_{P}’.