Software Tools for Technology Transfer manuscript No. (will be inserted by the editor)

Widening Operators for Powerset Domains^{⋆}

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

1 Department of Mathematics, University of Parma, Italy

e-mail: {bagnara,zaffanella}@cs.unipr.it

2 School of Computing, University of Leeds, UK

e-mail: hill@comp.leeds.ac.uk

The date of receipt and acceptance will be inserted by the editor

Abstract. The finite powerset construction upgrades an abstract domain by allowing for the representation of finite disjunctions of its elements. While most of the operations on the finite powerset abstract domain are easily obtained by “lifting” the corresponding operations on the base-level domain, the problem of endowing finite powersets with a provably correct widening operator is still open. In this paper we define three generic widening methodologies 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 that allow all the flexibility required to tune the complexity/precision trade-off. As far as we know, this is the first time that the problem of deriving non-trivial, provably correct widening operators in a domain refinement is tackled successfully. We illustrate the proposed techniques by instantiating our widening methodologies on powersets of convex polyhedra, a domain for which no non-trivial widening operator was previously known.

Key words: Abstract interpretation, abstract domain refinement, powersets, widening operators, convex polyhedra.

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 [16], 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 [16]; 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 [13,16,23].

When an abstract domain has very long or infinite ascending chains, the standard abstract iteration sequence [15]

A^{0}(0), A^{1}(0), A^{2}(0), …,  (1)

where A is the abstract semantic function and 0 is the bottom element of the domain, may converge very slowly or fail to converge altogether. This problem can be attacked by resorting to a binary operator ‘∇’ and defining an alternate abstract semantic function B such that, for each domain element d, B(d) := d ∇ (d ⊕ A(d)), where ‘⊕’ is the least upper bound operator of the domain. The following sequence is then computed instead of (1):

⋆ 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,” “Constraint Based Verification of Reactive Systems,”

and “AIDA — Abstract Interpretation: Design and Applications,”

and by a Royal Society (UK) International Joint Project (ESEP)

award.

B^{0}(0), B^{1}(0), B^{2}(0), ….  (2)

If ‘∇’ always results in an upper bound of its operands, then it is called extrapolation operator and the elements of the sequence (2) are upper approximations of the corresponding elements in (1). If, in addition, ‘∇’ ensures that (for each possible choice of the A we started with) the sequence (2) is ultimately stationary, then the (finitely computable) fixpoint of B is a post-fixpoint of A and ‘∇’ is called widening operator.

This paper focuses on the derivation of widening operators for a kind of disjunctive refinement we call finite powerset construction [2], in which finite disjunctions are implemented by explicit collections of elements of the base-level abstract domain. The enhanced abstract domain obtained by means of this construction contains ascending chains whose cardinality is greater than or equal to the cardinality of the base-level abstract domain. As a result, every large or infinite abstract domain, when enhanced by means of the finite powerset construction, results in a domain with long or infinite ascending chains whose practicality is thus dependent on the availability of suitable widening operators.

It should be stressed that what we are facing here is a dichotomy. On the one hand, the design of a successful widening is a very delicate task that is not only dependent on the considered abstract domain but also on the particular analysis or verification application and on the class of systems being analyzed or verified. A widening is successful for a class of problem instances to the extent it captures common growth patterns that do happen in practice in the class. Experimentations is all what is available today to evaluate the goodness of a widening with respect to its potential applications. On the other hand, the extreme specificity of the widening design problem must be contrasted with the complete generality of the finite powerset construction. The important contribution of this paper is constituted by three methodologies for the design of widening operators on any finite powerset domain. These methodologies make it very easy to ensure that the resulting operator is indeed a widening (a non-trivial problem, as witnessed by the fact that previous attempts at defining a widening on powersets of polyhedra have failed) while leaving enough latitude to the designer to attack the precision problem in a domain-dependent, problem-dependent way. As far as we know, this is the first time that the problem of deriving non-trivial, provably correct widening operators in a domain refinement is tackled successfully. In previous works, such as [10], the main focus was in the definition of extrapolation operators:^{1} the given examples finitely converge thanks to the adoption of ad-hoc operators and no general methodology is suggested that can turn these extrapolators into proper widenings.

In this paper, we also present specializations of our widening methodologies 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 [30,35] and its successor PolyLib [31], even though no widenings are provided. Sets of polyhedra, represented with Presburger formulas made available by the Omega library [29,32], are used in the verifier described in [11]; 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 [21], where sets of polyhedra are represented using the clp(q, r) constraint library [28].

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 shows the divergence problems that arise when upgrading any widening for the base-level domain to work on the finite powerset domain; Sections 5, 6 and 7 give three alternative strategies for solving these issues so as to obtain proper widenings for the finite powerset domain; Section 8 shows a way to control the precision/efficiency trade-off of these widenings. Section 9 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 set of all the finite multisets having elements in S is denoted by M(S). The operators working on multisets are denoted by the corresponding operators working on sets: any ambiguity will be resolved by context. The set of all the partial (resp., total) functions from set S to set T is denoted by S ↣ T (resp., S → T). The first limit ordinal is denoted by ω. A poset ⟨O, ⪯⟩ is a set O equipped with a partial order ‘⪯’. The strict version of the partial order relation is denoted by ‘≺’. Each poset ⟨O, ⪯⟩ induces a corresponding poset of finite multisets ⟨M(O), ⪯⪯⟩ where the multiset partial order ‘⪯⪯’ is defined, for all M, N ∈ M(O), as follows [22]:

M ⪯⪯ N ⟺^{def} \begin{cases}∃X, Y ∈ M(O) . N = (M \ X) ∪ Y \\ and ∀y ∈ Y : ∃x ∈ X . x ≺ y. \end{cases}

A chain over the poset ⟨O, ⪯⟩ is a totally ordered subset C ⊆ O, i.e., for each x, y ∈ C we have x ⪯ y or y ⪯ x. A poset satisfies the ascending chain condition if all its strictly increasing chains are finite. The induced poset of finite multisets ⟨M(O), ⪯⪯⟩ satisfies the ascending chain condition if and only if the base-level poset ⟨O, ⪯⟩ does [22].^{2} When the carrier of the relation is made clear from context, we will abuse terminology by saying that (the strict version of) a partial order relation satisfies the ascending chain condition to mean that the corresponding poset satisfies this property.

1 In [10], a “widening” is any extrapolation operator; the finite convergence guarantee is only achieved when considering so-called tractable representations.

We assume some familiarity with the basic notions of lattice and fixpoint theory [9].

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 [18, 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 nonessential 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 A: D → D that is sound with respect to F: C → C:

∀c ∈ C : ∀d ∈ D : c ⊑ γ(d) ⟹ F(c) ⊑ γ(A(d)). (3)

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 A^{0}(0), A^{1}(0), …, 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 [14,15,18,19] 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 [19, p. 275]).

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

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

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

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 to denote d_{1} ⊢_{∇} d and d_{1} ≠ d.

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

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

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

When trying to prove that an upper bound operator ⊞: D × D → D is indeed a widening, a possible tactic is to provide a “convergence certificate.” This is constituted by a structure that disallows indefinite growth and a way of mapping elements of D to elements of the structure, such that the application of the upper bound operator results in a strict growth: as growth cannot be indefinite, convergence is certified. Formally, a finite convergence certificate for ‘⊞’ (on D̂) is a triple (O, ⪯, μ) where ⟨O, ⪯⟩ is a poset satisfying the ascending chain condition and μ: D → O, which is called level mapping, is such that

2 Note the systematic replacement of the notion of well-founded poset, adopted in [22], by the dual notion of poset satisfying the ascending chain condition, which is more standard in the field of Abstract Interpretation.

∀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, ⪯, μ).

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 of concrete domain is the complete lattice

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

The domain Â_{n} is the one commonly adopted in semantic constructions for imperative programs, whereas the domain B̂_{n} is useful when modelling those constraint programming languages where affine inequalities (i.e., convex polyhedra) can be used as a first class datatype.

The abstract domain ℂ̂ℙ_{n}, which is a join-semilattice, is related to the domains Â_{n} and B̂_{n} by the concretization functions γ^{A} : ℂℙ_{n} → ℘(ℝ^{n}) and γ^{B} : ℂℙ_{n} → ℘(ℂℙ_{n}) defined as follows, for each P ∈ ℂℙ_{n}:

γ^{A}(P) := P,  (4)
γ^{B}(P) := ↓ P := { Q ∈ ℂℙ_{n} | Q ⊆ P }.  (5)

These functions are trivially monotonic and injective.

For each choice of concrete domain carrier C, that is C ∈ {℘(ℝ^{n}), ℘(ℂℙ_{n})}, the continuous semantic function F: C → C and the corresponding monotonic abstract semantic function A: ℂℙ_{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 [20] and refined in [25]. 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 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 halfspaces ⟨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.

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 or (⟨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})[β_{2}/β_{1}]) \end{matrix} \}

and repr_{≥}(C_{1})[β_{2}/β_{1}] := (repr_{≥}(C_{1}) \ {β_{1}}) ∪ {β_{2}}.

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

We now define a finite convergence certificate for the standard widening ‘∇_{s}’: the basic intuition is that a standard widening application will either result in an increase of the dimension of the polyhedron (which happens when some equalities are turned into inequalities or dropped altogether) or, if the dimension is unchanged, in a decrease of the number of constraints.

Definition 3. ((O_{s}, ⪯_{s}, μ_{s}).) Let O_{s} = (ℕ, ℕ) and ‘⪯_{s}’ denote the lexicographic ordering for O_{s} that uses ‘≥’ for the individual ordering of the components. A certificate for ‘∇_{s}’ is (O_{s}, ⪯_{s}, μ_{s}) where the level mapping μ_{s}: ℂℙ_{n} → O_{s}, for each P = con(C) ∈ ℂℙ_{n} such that C is either inconsistent or in minimal form, is defined by

μ_{s}(P) := \begin{cases}(n + 1, 0), & if P = ∅; \\ (n − dim(P), # C), & otherwise. \end{cases}

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 [16]. In this section, we present the finite powerset operator [2], which is a domain refinement similar to disjunctive completion [16] and is obtained by a variant of the down-set completion construction presented in [17]. The following notation and definitions are mainly borrowed from [2, Section 6].

Definition 4. (Non-redundancy.) Let us consider a join-semilattice D̂ = ⟨D, ⊢, 0, ⊕⟩. 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 a finite set into its nonredundant counterpart is defined, for each S ∈ ℘_{f}(D), by

Ω_{D}^{⊢}(S) := S \ { d ∈ S | d = 0 or ∃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 join-semilattice. 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}.

In abstract interpretation terms, this states that each element of S_{1} is correctly approximated by some elements of S_{2}; hence S_{1} is correctly approximated by S_{2}.

A sort of Egli-Milner partial order relation^{3} 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}.

This states that every element of S_{2} serves the purpose of approximating some elements of S_{1}.

An (Egli-Milner) connector for D̂_{P}, denoted by ‘ ⊞_{EM}’ is any upper bound operator for the partial order ‘⊢_{EM}’ on ℘fn^{⊢}(D). The reason we call such an operator a “connector” is because it will typically work by joining (connecting) elements in its arguments so as to ensure that all the resulting elements approximate an element in the arguments. 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 [17] is that we are dropping the assumption about the complete

3 Note that ‘⊢_{EM}’ is similar to, but formally different from the partial order defined on the Egli-Milner powerdomain [1], since in its specification we consider the non-redundant elements only.

O  Q_{1}  Q_{2} Q_{3} P_{1}  P_{2} P_{3}

Fig. 1. The collection of Q_{i} approximates the collection of P_{i}.

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 [17], 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.

An abstract semantic function A_{P} : ℘fn^{⊢}(D) → ℘fn^{⊢}(D) on the finite powerset domain may be provided by an ad-hoc definition, which needs to be matched by a corresponding proof of correctness. More often, if the concrete semantic function F: C → C satisfies suitable hypotheses, A_{P} can be safely induced from the abstract semantic function A: D → D. For instance, if F is additive, we can define A_{P} as follows [16,23]:

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

3.1 The Finite Powerset Domain of Polyhedra

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

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

Example 1. Consider the polyhedra in Figure 1 and let

T_{0} := {P_{1}, P_{2}, P_{3}},
T_{1} := {P_{1}, Q_{1}, Q_{2}, Q_{3}},
T_{2} := {Q_{1}, Q_{2}, Q_{3}},
T_{3} := {Q_{1}, Q_{2}}.

Then T_{0}, T_{2}, T_{3} ∈ ℘fn^{⊆}(ℂℙ_{2}), but T_{1} ∉ ℘fn^{⊆}(ℂℙ_{2}) since

P_{1} ⊂ Q_{1} is redundant in T_{1}, so that T_{2} = Ω_{ℂℙ_{2}}^{⊆}(T_{1}). Moreover, T_{0} ⊢_{P} T_{2} but T_{0} ⊬_{EM} T_{2}, because Q_{3} approximates none of the P_{i}’s. Finally, T_{0} ⊢_{EM} T_{3}.

Let γ_{P}^{A} and γ_{P}^{B} denote the (powerset) concretization functions induced by the functions γ^{A} and γ^{B} defined by Eqs. (4) and (5), 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 [33]. On the other hand, since γ_{P}^{B} is injective, ‘≡_{γ_{P}^{B}}’ coincides with the identity congruence relation.

4 Extrapolation Operators on 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. Following the spirit underlying the domain refinement methodology, one may try and lift any widening operator ∇: D × D ↣ D defined on the base-level abstract domain D̂ so as to be applied to elements of the finite powerset domain D̂_{P}.^{4} Unfortunately, unless suitable counter-measures are taken, most of the lifting heuristics will break the convergence guarantee, resulting in an extrapolation operator for the finite powerset domain. Here we introduce a very general class of extrapolation operators lifting the base-level widening ‘∇’.

Definition 6. (Extrapolation heuristics.) An operator h∇_{P} : ℘fn^{⊢}(D) × ℘fn^{⊢}(D) ↣ ℘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});  (6)
∀d ∈ h∇_{P}(S_{1}, S_{2}) \ S_{2} : ∃d_{1} ∈ S_{1} . d_{1} ⊩_{∇} d. (7)

Informally, condition (6) 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 (7) ensures that any element in the result that is not in S_{2} must originate from an application of ‘∇’ to an element of S_{1}.

It is straightforward to construct an algorithm for computing an extrapolation heuristics for any given baselevel widening ‘∇’. The basic idea was proposed in [11] for an abstract domain encoding a set of integer vectors by means of a Presburger formula. Informally, for all pairs (d_{1}, d_{2}) ∈ S_{1} × S_{2} that can be built using the two arguments S_{1} and S_{2}, return d_{1} ∇ d_{2} if defined and return d_{2} if not.

4 We assume the base-level abstract domain D̂ is provided with at least one widening operator, as is the case for most abstract domains used in the context of static analysis. If D̂ satisfies the ascending chain condition, 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 ‘⊕’.

Definition 7. (H∇_{P}.) 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}^{⊢}(S) where

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

Proposition 1. The H∇_{P} operator is an extrapolation heuristics for D̂_{P}.

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

Example 2. To see that the heuristics H∇_{P} is not a widening for (ℂ̂ℙ_{n})_{P}, consider the strictly increasing sequence T_{0} ⊢_{P} T_{1} ⊢_{P} ⋯ in ℂℙ_{1} defined by^{5}

T_{j} := { {x = i} | i ∈ ℕ, 0 ≤ i ≤ j }.

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.

The iteration sequence in Example 2 is diverging because there is no finite upper bound on the cardinality of the iterates. To overcome this problem, the operator sketched in [11], which uses the H∇_{P} heuristics of Definition 7, assumes that a further approximation is applied whenever the cardinality of the set to be widened exceeds a fixed bound k ∈ ℕ. However, no matter how this further approximation step is defined, this approach is not enough to obtain a proper widening, so that termination cannot be guaranteed. In fact, the following example shows that the extrapolation heuristics H∇_{P} may result in an infinite increasing sequence on D̂_{P} whose elements all have bounded cardinality.

Example 3. Consider the extrapolation heuristics H∇_{P} for (ℂ̂ℙ_{2})_{P}, as specified in Definition 7, with ‘∇_{s}’ as the widening on the base-level abstract domain ℂ̂ℙ_{2} (so that H∇_{P} is the one used in [11]). 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}.

O  T_{2} = {P_{2}, P_{3}} P_{3} P_{2}  O  T_{3} = {P_{2}, P_{4}} P_{4} P_{2}^{O  U_{3} = {P′_{0}} T_{0} = {P_{0}} P_{0}  P′_{0}}  ^{O  T_{1} = {P_{1}, P_{3}} P_{3} P_{1}}
Fig. 2. The iterates T_{0}, T_{1}, T_{2}, T_{3} and U_{3} in Example 3.

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}},
T_{3} = {P_{2}, P_{4}},

as shown in Figure 2. 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 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, 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, letting

P′_{0} := P_{3} ∇_{s} P_{4}

= {0 ≤ x ≤ 8, 0 ≤ y ≤ 8, x + y ≤ 14, x − y ≥ −6}, we obtain

5 In this and the following examples, we abuse notation by writing a constraint system C to denote the polyhedron P = con(C).

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

5 Powerset Widenings using Set Cardinality

The first methodology we propose shares with [11] the idea of posing constraints on the cardinality of the arguments of the widening. As observed in the previous section, this approximation on its own is insufficient to ensure the operator is a widening. A closer inspection of the iterates in Example 3 shows that divergence is actually caused by the reduction function Ω_{D}^{⊢}, which interferes with the cardinality control mechanism by removing redundant elements, so that the cardinality threshold is never reached. The problem caused by Ω_{D}^{⊢} is avoided by requiring the extrapolation heuristics h∇_{P} being used by the widening to satisfy an additional property.

Definition 8. (∇-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.  (8)

Although H∇_{P} of Definition 7 is not ∇-covered,^{6} a ∇- covered extrapolation heuristics for D̂_{P} can be obtained for any widening ‘∇’ on the base-level domain D̂ by selectively replacing the standard reduction map Ω_{D}^{⊢} with 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, the map Ω_{D}^{∇} replaces both d and d′ by d ∇ d′.

Definition 9. (∇-reduction map, Ω_{D}^{∇}.) A function Ω_{D}^{∇}: ℘_{f}(D) → ℘fn^{⊢}(D) is called ∇-reduction map if it satisfies the following property: for all S ∈ ℘_{f}(D), if Ω_{D}^{∇}(S) = S′, then there exists a sequence T_{0}, …, T_{m}

H∇_{P}(T_{2}, T_{3}) = {P′_{0}}, but P_{2} ⊬_{∇} P′_{0}.

of elements of ℘_{f}(D) such that T_{0} = S, T_{m} = S′ and, for each 0 < i ≤ m, T_{i} = (T_{i−1} \ {d, d′}) ∪ {d ∇ d′}, where d, d′ ∈ T_{i−1} and d ⊩ d′. The (overloaded) operator Ω_{D}^{∇}: ℘fn^{⊢}(D) × ℘fn^{⊢}(D) → ℘fn^{⊢}(D) is defined, for all

S_{1}, S_{2} ∈ ℘fn^{⊢}(D), by

Ω_{D}^{∇}(S_{1}, S_{2}) := Ω_{D}^{∇}(S_{1} ∪ S_{2}).

Proposition 2. The Ω_{D}^{∇} operator is a ∇-covered extrapolation heuristics for D̂_{P}.

Example 4. Consider the iteration sequence of Example 3 and suppose now that, instead of using H∇_{P}, we adopt a ∇-covered extrapolation heuristics satisfying Definition 9. 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} = Ω_{D}^{∇}(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′_{0}}
= {{x ≥ 0, y ≥ 0}},

therefore breaking the divergence pattern.

In order to control the cardinality of the abstract iterates, several possible solutions could be adopted. In the following proposal, if the cardinality of the second argument of the widening 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 10. (Collapsor.) For each k ≥ 1, a unary operator ⇑_{k}: ℘fn^{⊢}(D) → ℘fn^{⊢}(D) is called a k-collapsor for D̂_{P} if, for each S ∈ ℘fn^{⊢}(D), either # S ≤ k and ⇑_{k} S = S or there exists S′ ⊆ S with # S′ > # S − k such that

⇑_{k} S = (S \ S′) ⊕_{P} {⊕S′}.

We now define a widening on the powerset domain that uses a k-collapsor with a ∇-covered extrapolation heuristics to ensure convergence of the abstract iterates.

Definition 11. (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. For all S_{1}, S_{2} ∈ ℘fn^{⊢}(D) such that S_{1} ⊩_{P} S_{2}, let

S_{1} _{k}∇_{P} S_{2} := h∇_{P}(S_{1}, ⇑_{k} S_{2}).

Then ‘_{k}∇_{P}’ is said to be a cardinality-based widening.

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

In general, the precision of this widening will depend on both the value of the parameter k and the particular heuristics used to select the subset to be collapsed.

6 In particular, in Example 3 we saw that P_{2} ∈ T_{2} and

Example 5. To illustrate the widening operator ‘_{k}∇_{P}’ for k = 2, we consider the powerset domain (ℂ̂ℙ_{1})_{P} with the standard widening ‘∇_{s}’ on ℂ̂ℙ_{1}, a ∇-covered extrapolation heuristics Ω_{D}^{∇} satisfying Definition 9 and a 2-collapsor 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 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 Ω_{D}^{∇} operator. Thus, we obtain

U_{1} = Ω_{D}^{∇}(U_{1}, ⇑_{2} T_{2})
= Ω_{D}^{∇}(U_{1}, {{x = 0}, {1 ≤ x ≤ 2}})
= Ω_{D}^{∇}({{x = 0}, {x = 1}, {1 ≤ x ≤ 2}})
= {{x = 0}, {x = 1} ∇_{s} {1 ≤ x ≤ 2}}
= {{x = 0}, {1 ≤ x}}.

In the next iteration we obtain stabilization.

6 Powerset Widenings Using Connectors

One obvious explanation for the divergence of the iteration sequence in Example 2 is that the base-level widening never comes into play. The second widening we propose is designed to avoid such situations.

To be more specific, when using the extrapolation heuristics H∇_{P} of Definition 7, the reason for divergence is that elements of S_{2} that do not cover an element in S_{1} will be included, unchanged, in H∇_{P}(S_{1}, S_{2}) without any involvement in a widening computation. To avoid this, one possibility is to replace S_{2} with S_{1} ⊞_{EM} S_{2}, where ‘ ⊞_{EM}’ is a connector for D̂_{P}, so that no such “brand new” elements can exist. Note that such a solution is not really specific for the extrapolation operator H∇_{P}. Here we specify another subclass of extrapolation heuristics that, when combined with a connector operator as described above, can be used to define a proper widening operator.

Definition 12. (∇-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). (9)

As already said, the above subclass includes the extrapolation heuristics H∇_{P} of Definition 7.

Proposition 3. The H∇_{P} operator is a ∇-connected extrapolation heuristics for D̂_{P}.

We therefore define a widening on the finite powerset domain that enforces convergence by using a connector with a ∇-connected extrapolation heuristics.

Definition 13. (The ‘_{EM}∇_{P}’ widening.) Let h∇_{P} be a ∇-connected extrapolation heuristics and ‘ ⊞_{EM}’ be a connector for D̂_{P}. For all S_{1}, S_{2} ∈ ℘fn^{⊢}(D) such that

S_{1} ⊩_{P} S_{2}, let 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}

Then ‘_{EM}∇_{P}’ is said to be a connector-based widening.

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

Clearly, the precision of this widening will depend on the chosen connector operator.

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

Consider now the powerset domain (ℂ̂ℙ_{2})_{P} and the iteration sequences T_{0} ⊢_{P} T_{1} ⊢_{P} ⋯ and U_{0} ⊢_{P} U_{1} ⊢_{P} ⋯ of Example 3. Let U′_{0} ⊢_{P} U′_{1} ⊢_{P} ⋯ be the sequence computed by using the widening operator ‘_{EM}∇_{P}’ specified above. Clearly, U′_{0} = U_{0} = T_{0}. However, by letting

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

instead of obtaining U_{1} = {T_{1}} we obtain

U′_{1} = H∇_{P}(U′_{0}, U′_{0} ⊎_{EM} T_{1})

= H∇_{P}(U′_{0}, {P_{0} ⊎ P_{1} ⊎ P_{3}})

= H∇_{P}(U′_{0}, {P_{5}})

= {P_{0} ∇_{s} P_{5}}

= {{x ≥ 0, y ≥ 0}}.

7 Powerset Widenings Using Certificates

The third widening technique we present in this paper requires a certificate (O, ⪯, μ) for the base-level widening ‘∇’. Widenings obtained in this way will be termed certificate-based. As it is used in the computation of the new widening on the powerset domain, the certificate for the base-level widening must be finitely computable, i.e., such that the partial order ‘⪯’ and the level mapping μ are both finitely computable. This means that such a certificate for ‘∇’ on D̂ cannot be simply taken as (D, ⊢_{∇}, I), where I is the identity map, since ‘⊢_{∇}’, in general, does not come with a computability guarantee.^{7}

The certificate-based widening can be seen as a variant of the framework presented in [5,6], which provided a clean and formal development for an idea originally sketched in [8]. We will use the certificate μ to define a suitable relation ‘ ↷_{P}’ on the finite powerset domain D̂_{P}. This relation will be shown to be a limited growth ordering (lgo) [5,6] on D̂_{P}, i.e., the strict version of a finitely computable preorder on ℘fn^{⊢}(D) that satisfies the ascending chain condition. Intuitively, the new widening ‘_{μ}∇_{P}’ on the finite powerset domain will be defined so that the relation ‘ ↷_{P}’ will correspond to the relation ‘ ⊩_{_{μ}∇_{P}}’.

Definition 14. (‘ ↷_{P}’.) Let (O, ⪯, μ) be a finitely computable certificate for the widening operator ‘∇’ on D̂. The relation ↷_{P} ⊆ ℘fn^{⊢}(D)×℘fn^{⊢}(D) induced by μ is such that, for each S_{1}, S_{2} ∈ ℘fn^{⊢}(D), S_{1} ↷_{P} S_{2} holds if and only if, letting d_{1} := ⨁S_{1} and d_{2} := ⨁S_{2}, one of the following holds:

μ(d_{1}) ≺ μ(d_{2});  (10)
μ(d_{1}) = μ(d_{2}) ∧ # S_{1} > 1 ∧ # S_{2} = 1;  (11)

μ(d_{1}) = μ(d_{2}) ∧ # S_{1} > 1 ∧ # S_{2} > 1 ∧ μ̃(S_{1}) ≺≺ μ̃(S_{2}), (12)

where the function μ̃: ℘fn^{⊢}(D) → M(O) is defined, for each S ∈ ℘fn^{⊢}(D), so that μ̃(S) is the multiset over O obtained by applying μ to each element in S. Namely, by μ̃(S) := { μ(d) | d ∈ S }.

Proposition 4. The ‘ ↷_{P}’ relation is finitely computable and satisfies the ascending chain condition.

Example 7. Consider the polyhedra in Figure 3 and let

T_{1} := {P_{1}, P_{2}, P_{3}, P_{4}},
T_{2} := {Q_{1}, Q_{2}, Q_{3}},

so that P = ⨄ T_{1} and Q = ⨄ T_{2}. By Definition 3, μ_{s}(P) = (0, 5) ≺_{s} (0, 4) = μ_{s}(Q) so that, by condition (10) of Definition 14, we obtain T_{1} ↷_{P} T_{2}.

O  Q_{1}  Q_{2} Q_{3} Q P_{1} P_{2}  P_{3}P_{4} P

Fig. 3. The lgo relation on collections of polyhedra.

O  Q_{1}  Q_{2} Q_{3} Q P_{1} P_{2}  P_{3} P

Fig. 4. The lgo relation on collections of polyhedra.

Now consider the polyhedra in Figure 4 and let

U_{1} := {P_{1}, P_{2}, P_{3}},
U_{2} := {Q_{1}},
U_{3} := {Q_{1}, Q_{2}, Q_{3}},

so that U_{1} ⊩_{P} U_{2} ⊩_{P} U_{3}, P = ⨄ U_{1}, Q_{1} = ⨄ U_{2}, Q = ⨄ U_{3} and μ_{s}(P) = μ_{s}(Q_{1}) = μ_{s}(Q) = (0, 4). Since # U_{2} = 1, none of the conditions of Definition 14 apply so that U_{2} ↷̸_{P} U_{3}. On the other hand, as # U_{1} = # U_{3} = 3, we have U_{1} ↷_{P} U_{2} by condition (11) of Definition 14. Finally, since

μ̃_{s}(U_{1}) = {(0, 6), (0, 4), (0, 4)}
≺≺_{s} {(0, 4), (0, 4), (0, 4)} = μ̃_{s}(U_{3}),

we obtain U_{1} ↷_{P} U_{3} using condition (12) of Definition 14.

For the sake of precision, 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 that can be trivially satisfied in case no better alternative is available.^{8}

Definition 15. (Subtraction.) A subtraction for D̂ is any partial operator ⊖: D × D ↣ D such that, for all d_{1}, d_{2} ∈ D, d_{2} ⊢ d_{1} implies that d_{1} ⊖ d_{2} is defined and both d_{1} ⊖ d_{2} ⊢ d_{1} and d_{1} = (d_{1} ⊖ d_{2}) ⊕ d_{2} hold.

7 Note that, for the domain ℂℙ_{n} of polyhedra and the standard widening ‘∇_{s}’, the certificate (O_{s}, ⪯_{s}, μ_{s}) provided in Definition 3 is finitely computable.

8 The subtraction operators defined here are very similar to the weakening operators introduced in [2, Definition 40, page 146].

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 8. The operator pdiff : ℂℙ_{n} × ℂℙ_{n} → ℂℙ_{n} is defined so that, for any P_{1}, P_{2} ∈ ℂℙ_{n}, pdiff(P_{1}, P_{2}) denotes the smallest closed and convex polyhedron containing the set difference P_{1} \ P_{2}. Then, if P_{2} ⊆ P_{1}, we have pdiff(P_{1}, P_{2}) ⊆ P_{1} and

P_{1} = (P_{1} \ P_{2}) ∪ P_{2}
= pdiff(P_{1}, P_{2}) ∪ P_{2}
= pdiff(P_{1}, P_{2}) ⊎ P_{2},

so that ‘pdiff’ is a subtraction for ℂ̂ℙ_{n}.

We now define a widening on the finite powerset domain that enforces convergence by means of a limited growth ordering induced by a certificate for the baselevel widening.

Definition 16. (The ‘_{μ}∇_{P}’ widening.) Let ‘ ↷_{P}’ be the limited growth ordering induced by the certificate μ for ‘ ∇’, let ‘ ⊞_{P}’ be any upper bound operator on D̂_{P} and ‘⊖’ be a subtraction for D̂. For all S_{1}, S_{2} ∈ ℘fn^{⊢}(D) such that S_{1} ⊩_{P} S_{2}, let

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

where S := S_{1} ⊞_{P} S_{2} and d := (⨁S_{1} ∇ ⨁S) ⊖ (⨁S). Then ‘_{μ}∇_{P}’ is said to be a certificate-based widening.

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

There are three cases in the specification of ‘_{μ}∇_{P}’ in Definition 16. In the first one, the widening simply returns the upper bound S = S_{1}⊞_{P}S_{2}, since this is enough to ensure a strict increase in the limited growth ordering relation. In the second case, the join of S_{1} is strictly more precise than the join of S, so that we apply the base-level widening ‘∇’ to them and then, using the subtraction operator, improve the obtained result, since S_{1} ↷_{P} S⊕_{P}{d} holds. In the last case, since the join of S_{1} is equivalent to the join of S, we return the singleton consisting of the join itself, as originally proposed in [16, Section 9].

Example 9. To illustrate the three cases of Definition 16, consider the finite powerset domain (ℂ̂ℙ_{2})_{P}, with the standard widening ‘∇_{s}’ for ℂ̂ℙ_{2}, certified by the level mapping μ_{s} defined in Definition 3. Let also the subtraction ‘⊖’ be defined as ‘pdiff’ and the upper bound ‘⊞_{P}’ be defined as ‘⊕_{P}’, so that, for all S_{1}, S_{2} ∈ (ℂ̂ℙ_{2})_{P} such that S_{1} ⊢_{P} S_{2}, we will have S_{1} ⊞_{P} S_{2} = S_{2}.

In particular, this means that in the first case of Definition 16, S_{1} _{μ}∇_{P} S_{2} = S_{2}. Applications of this case can

O  \begin{matrix}T_{1} = \{P_{1}, P_{2}, P_{3}\} \\ T_{2} = T_{1} ∪ \{P_{4}\} \end{matrix} P_{1} P_{2}  P_{3} P_{4}  ^{O  P_{1} P_{2}  P_{3} ⨄ T_{1} P_{4} ⨄ T_{2}} O  P_{1} P_{2}  P_{3} P_{4} ⨄ T_{2} Q = ⨄ T_{1} ∇_{s} ⨄ T_{2}  O  P_{1} P_{2}  P_{3} P_{4} P_{d}

Fig. 5. The second case of the certificate-based widening.

be observed by considering the sets of polyhedra introduced in Example 7 (see Figure 3)

{P_{1}, P_{2}, P_{3}, P_{4}}_{μ}∇_{P} {Q_{1}, Q_{2}, Q_{3}} = {Q_{1}, Q_{2}, Q_{3}}

and (see Figure 4)

{P_{1}, P_{2}, P_{3}}_{μ}∇_{P} {Q_{1}} = {Q_{1}},
{P_{1}, P_{2}, P_{3}}_{μ}∇_{P} {Q_{1}, Q_{2}, Q_{3}} = {Q_{1}, Q_{2}, Q_{3}}.

Figure 5 illustrates an application of the second case of Definition 16. Consider the computation of T_{1} _{μ}∇_{P} T_{2} where sets T_{1} and T_{2} are as shown in the top left diagram while their poly-hulls ⨄ T_{1} and ⨄ T_{2} are shown in the top right diagram. Since μ_{s}(⨄ T_{1}) = (0, 5) ⪯̸_{s} (0, 6) = μ_{s}(⨄ T_{2}), we obtain T_{1} ↷̸_{P} T_{2}, so that the first case of Definition 16 does not apply. As ⨄ T_{1} ⊂ ⨄ T_{2}, the second case applies and we use the base-level widening to compute Q = ⨄ T_{1} ∇_{s} ⨄ T_{2}, shown in the bottom left diagram. We then find the convex polyhedral difference P_{d} = pdiff(Q, ⨄ T_{2}), to obtain the widened set T_{1} _{μ}∇_{P} T_{2} = T_{2} ∪ {P_{d}} as shown in the bottom right diagram. Note that, as far as the divergence problem is concerned, it would be enough to return the singleton set {Q}, since T_{1} ↷_{P} {Q} already holds; however, by exploiting the availability of a non-trivial subtraction operator, we can usually obtain, as in this case, a more precise result.

The polyhedra shown in the top left diagram of Figure 5 can also illustrate the application of the third and last case of Definition 16. To this end, consider the set T′_{1} = {P_{1}, P_{3}, P_{4}} and the computation of T′_{1} _{μ}∇_{P} T_{2}. Since ⨄ T′_{1} = ⨄ T_{2}, the first two cases of Definition 16 do not apply, so that we compute T′_{1} _{μ}∇_{P} T_{2} = {⨄ T_{2}}.

As shown in the example above, Definition 16 does not require that the upper bound operator ‘⊞_{P}’ is based on the base-level widening ‘∇’. Moreover, the scheme of Definition 16 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 an increase 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 [11].

8 Merging Elements According to a Congruence Relation

For any powerset widening, it may be possible to merge together (i.e., join) some of the elements occurring in the second argument without compromising the finite convergence guarantee. This merging operation can be guided by a congruence relation on the finite powerset domain, 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}}’. As the purpose of this paper is to provide generic widening procedures for powersets, here we only consider congruences that may be defined independently of any particular concrete domain and the intended widening. Two such relations are the identity congruence relation, where trivial equivalence is assumed, and the ⊕-congruence relation, where sets that have the same join are equivalent. However, the identity congruence allows for no merging at all and hence has no effect at all on the iteration sequence. On the other hand, the ⊕-congruence enables a direct application of the baselevel widening on the joined elements, thereby providing a default heuristics that is likely to hasten convergence. We now define a new non-identity congruence relation for any powerset domain that refines the ⊕-congruence.

Definition 17. (‘◁’ 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),

S′_{1} ⊢_{P} S_{1} ⟹ ∃S′′_{1} ∈ ℘fn^{⊢}(D) . ⨁S′_{1} = ⨁S′′_{1} ∧ S′′_{1} ⊢_{P} S_{2}.

The same-content 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 S_{1} ⊢_{P} S_{2} implies that S_{1} ◁ S_{2} so that S ◁ {⨁S}, since S ⊢_{P} {⨁S}. Moreover, if S_{2} is a singleton, then S_{1} ⊢_{P} S_{2} if and only if S_{1} ◁ S_{2}. Hence ‘▷◁’ is a congruence relation on D̂_{P} that refines the ⊕-congruence.

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

O  T_{0} P_{2} P_{1}  P_{3}  O  T_{1} A Q_{5} Q_{1} Q_{2} Q_{3} Q_{4}

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

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 S_{1} ◁ S_{2} holds if and only if ⋃ S_{1} ⊆ ⋃ S_{2}; and hence, the same-content relation ‘▷◁’ coincides with the induced congruence relation ‘≡_{γ_{P}^{A}}’.

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

Example 10. Consider the polyhedra in Figure 6. Then P_{1} ⊎ P_{2} = P_{1} ∪ P_{2} and P_{2} ⊎ P_{3} = P_{2} ∪ P_{3} so that, as T_{0} = {P_{1}, P_{2}, P_{3}},

T_{0} ▷◁ {P_{1} ∪ P_{2}, P_{3}} ▷◁ {P_{1}, P_{2} ∪ P_{3}}.

On the other hand, since T_{1} = {Q_{1}, Q_{2}, Q_{3}, Q_{4}, Q_{5}}, letting T_{2} := {Q_{1}, Q_{2}, Q_{3}, Q_{4}}, although ⨄ T_{1} = ⨄ T_{2}, T_{1} ⋪ T_{2}. To see this, let A be an inner point of polyhedron Q_{5} and let S_{1}, S_{2}, and S′_{1} in Definition 17 be T_{1}, T_{2}, and T′_{1} = {{A}}, respectively. Then, the one and only collection of polyhedra having the same poly-hull of T′_{1} is T′_{1} itself. However, T′_{1} ⊬_{P} T_{2}, so that T_{1} ⋪ T_{2}.

We now define an operation merger for the powerset domain that replaces selected subsets by congruent singleton sets for any given congruence relation.

Definition 18. (Mergers.) Let ‘∼’ be a congruence relation on D̂_{P}. The relation merge_{∼} ⊆ ℘fn^{⊢}(D) × ℘fn^{⊢}(D) is such that merge_{∼}(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}.

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

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

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

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

For the finite powerset domain over ℂ̂ℙ_{n}, lines 1–9 of the algorithm specified in [11, Figure 8, page 773] define a merger operator ‘↑_{▷◁}’ such that, for each finite set S of polyhedra, ↑_{▷◁} S is pairwise-merged. Thus, the algorithm described in [11] is in fact the composition of three computational devices: the pairwise-merger for ‘▷◁’, the extrapolation heuristics H∇_{P} of Definition 7 and a cardinality control mechanism (which is not formally specified). Since all the abstract elements considered in Example 3 are fully-merged, even the complete algorithm is still implementing an extrapolation operator which is not a proper widening.

Example 11. To illustrate the merge relation for the finite powerset domain of polyhedra (ℂ̂ℙ_{n})_{P} with the ‘▷◁’ congruence relation, we again use the two diagrams in Figure 6. The set of polyhedra T_{0} in the left-hand diagram is not pairwise-merged since

{P_{1} ⊎ P_{2}} = {P_{1} ∪ P_{2}} ▷◁ {P_{1}, P_{2}},
{P_{2} ⊎ P_{3}} = {P_{2} ∪ P_{3}} ▷◁ {P_{2}, P_{3}}.

The sets {P_{1}∪P_{2}, P_{3}} and {P_{1}, P_{2}∪P_{3}} are fully-merged and hence pairwise-merged, and both merge_{▷◁}(T_{0}, {P_{1} ∪ P_{2}, P_{3}}) and merge_{▷◁}(T_{0}, {P_{1}, P_{2} ∪ P_{3}}) hold. The set T_{1} in the right-hand diagram is pairwise-merged but not fully-merged. Since ⨄ T_{1} = ⋃ T_{1}, the singleton set {⋃ T_{1}} is fully-merged and hence pairwise-merged and merge_{▷◁}(T_{1}, {⋃ T_{1}}) holds.

9 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 that are parametric with respect to the specification of some simpler operators: these are summarized in Table 1, where we distinguish the operators that are actually required (even though defaults are available for some of them) from those that can be optionally used to tune the precision/efficiency trade-off of the widenings. These generic constructions are, on the one hand, strong enough to enforce the convergence of the abstract iteration sequence while, on the other hand, they provide the flexibility

Widening Required  Optional
k∇_{P} ∇-covered h∇_{P} (Ω_{D}^{∇}) merger ↑_{∼}
k-collapsor ⇑_{k}
EM∇_{P}  ∇-connected h∇_{P} (H∇_{P}) merger ↑_{∼}
connector ⊞_{EM}
μ∇_{P} certificate μ merger ↑_{∼}
upper bound ⊞_{P}  other upper bounds
subtraction ⊖ (π_{1})

Table 1. The required and optional operators for the three widenings (defaults defined in the present paper in parentheses).

needed to attack the precision problem in a domaindependent, problem-dependent way.

Given three alternative methodologies for the specification of a widening, it is natural to question whether or not one is better than the others with respect to some “measure,” be it the precision of the obtained results, the expected efficiency of the overall analysis, or even the ease of implementation. Not surprisingly, the very generality of the finite powerset construction itself makes it impossible to answer such a question in general. It should also be stressed that, when comparing different widening operators, an “immediate” precision improvement does not automatically imply a corresponding “overall” precision improvement, because accurate widening operators are usually not monotonic in their arguments. Nonetheless, the following observations provide useful guidelines for the prospective widening designer.

A rather obvious remark is that all the widenings presented in this paper directly depend on the baselevel widening used for the extrapolation heuristics or the convergence certificate: there is little hope that any of the methodologies we propose will behave well if the base-level widening is inadequate for the considered application. This observation applies not only to the precision of the widening, but also (to some extent) to its efficiency.

If the finite powerset construction is applied to a reasonably precise base-level domain, such as the domain of convex polyhedra, then a certificate-based widening may be a good starting point. In fact, this methodology provides the designer with a high degree of flexibility: not only does it provide a choice between several, possibly fine-grained certificates, but it also allows the designer to experiment with a potentially wide range of upper bound operators. In such a context, the cardinalities of the collections of abstract elements are relatively small, since most of the precision of the approximation is already encoded in the base-level elements (e.g., the polyhedra). In other words, the finite powerset construction is meant to avoid the precision losses caused by a few, mainly irregular, growth patterns.

If, in contrast, the base-level domain and its widening are somehow weak, as might be the case for the abstract domain of intervals [14], then a certificate-based widening is probably not a good choice. In this case, the simplicity and efficiency of the base-level domain are better exploited by increasing the cardinality of the abstract collections of elements, so that a cardinality-based widening is likely to provide better results.

The connector-based widening can be seen as an intermediate alternative: on the one hand, it shares with the cardinality-based widening the simplicity (and ease of implementation) of the approach; on the other hand, in order to obtain reasonable precision, it requires that an adequate connector operator is identified for the application at hand.

As already stressed in the introduction, in all cases the resulting widening operator will have to undergo a thorough experimentation in order to ascertain to what extent it actually adapts to the specific class of problem instances that are of interest. For the finite powerset domain of convex polyhedra, this work has just started. We have extended the Parma Polyhedra Library (PPL) [4,7], 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 [26,27]. The current prototype, which is based on the new widening operator defined in [5,6], tries two upper bound operators for the powerset domain: the first one is the least upper bound; the second one is the extrapolation heuristics H∇_{P} (but instantiated using the widening in [5,6]). 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 [11]. By exploiting the genericity of the finite powerset construction, it was also possible to experiment with the certificate-based widening on other base-level domains provided by the PPL, including the domain of bounded difference shapes [3] and a domain of rational grids (i.e., sets defined by systems of relational congruences in the style of [24]).

In the examples previously shown and in the experiments conducted so far, the finite powerset construction has been applied only to those base-level abstract domains that encode numerical information. This was mainly for ease of presentation and also because of the availability of implementations for the chosen domains; there is nothing in the considered generic constructions that prevents one from applying them to domains that encode symbolic information. However, the reader should remember that the finite powerset construction is meant to provide a restricted form of disjunctive information, where different disjuncts are explicitly maintained as base-level abstract elements. As a consequence, it is unlikely that the finite powerset construction could really compete with ad-hoc disjunctive constructions, as provided by, e.g., BDD structures [12] or type graphs [34].

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 dataflow analysis of constraint logic-based languages. Science of Computer Programming, 30(1–2):119–155, 1998.

3. R. Bagnara, P. M. Hill, E. Mazzi, and E. Zaffanella. Widening operators for weakly-relational numeric abstractions. In C. Hankin and I. Silveroni, editors, Static Analysis: Proceedings of the 12th International Symposium, volume 3672 of Lecture Notes in Computer Science, pages 3–18, London, UK, 2005. Springer-Verlag, Berlin.

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

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

6. R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella. Precise widening operators for convex polyhedra. Science of Computer Programming, 58(1–2):28–56, 2005.

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

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

9. G. Birkhoff. Lattice Theory, volume XXV of Colloquium Publications. American Mathematical Society, Providence, Rhode Island, USA, third edition, 1967.

10. F. Bourdoncle. Abstract interpretation by dynamic partitioning. Journal of Functional Programming, 2(4):407– 435, 1992.

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

12. A. Cortesi, G. Filé, and W. Winsborough. Prop revisited: Propositional formula as abstract domain for groundness analysis. In Proceedings, Sixth Annual IEEE Symposium on Logic in Computer Science, pages 322–327, Amsterdam, The Netherlands, 1991. IEEE Computer Society Press.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

31. V. Loechner. PolyLib: A library for manipulating parameterized polyhedra. Available at http://icps.

                                                        u-strasbg.fr/^{∼}loechner/polylib/, March 1999. De-

clares itself to be a continuation of [35].

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

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

34. P. Van Hentenryck, A. Cortesi, and B. Le Charlier. Type analysis of Prolog using type graphs. Journal of Logic Programming, 22(3):179–209, 1995.

35. 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). Using the notation of Definition 6, we show that H∇_{P}(S_{1}, S_{2}) = S_{2}⊕_{P}Ω_{D}^{⊢}(S), where

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

satisfies properties (6) and (7) of Definition 6. Note that, by Definition 6, we have S_{1} ⊩_{P} S_{2}, so that S_{2} ≠ ∅.

Let S′ := S_{2} ∪ Ω_{D}^{⊢}(S); then, by Definitions 5 and 7, we obtain

H∇_{P}(S_{1}, S_{2}) = S_{2} ⊕_{P} Ω_{D}^{⊢}(S)
= Ω_{D}^{⊢}(S_{2} ∪ Ω_{D}^{⊢}(S))
= Ω_{D}^{⊢}(S′).  (13)

We will prove that

S_{2} ⊢_{P} Ω_{D}^{⊢}(S′);  (14)
∀d ∈ Ω_{D}^{⊢}(S′) : ∃d_{2} ∈ S_{2} . d_{2} ⊢ d;  (15)
∀d ∈ Ω_{D}^{⊢}(S′) \ S_{2} : ∃d_{1} ∈ S_{1} . d_{1} ⊩_{∇} d.  (16)

Then, using equation (13), property (6) of Definition 6 follows from properties (14) and (15) and property (7) of Definition 6 follows from property (16).

To prove property (14), let d_{2} ∈ S_{2}; then, since S_{2} ⊆ S′, we also have d_{2} ∈ S′; hence, by Definition 4, there exists d′_{2} ∈ Ω_{D}^{⊢}(S′) such that d_{2} ⊢ d′_{2}. Therefore property (14) holds.

To prove properties (15) and (16), let d ∈ Ω_{D}^{⊢}(S′)\S_{2}; then, by Definition 4, d ∈ S′ and, as d ∉ S_{2}, again by Definition 4, d ∈ S. Thus there exist d_{1} ∈ S_{1} and d_{2} ∈ S_{2} such that d = d_{1} ∇ d_{2} and hence d_{1} ⊩_{∇} d. Therefore property (16) holds. Moreover, as ‘∇’ is a widening on D̂, d_{2} ⊢ d. Therefore property (15) holds. ⊓ ⊔

Proof (of Proposition 2). Assuming the notation and hypothesis introduced in Definition 9, we show that Ω_{D}^{∇}(S_{1}, S_{2}) satisfies properties (6) and (7) of Definition 6 and property (8) of Definition 8. Let S = S_{1} ∪S_{2}, so that Ω_{D}^{∇}(S_{1}, S_{2}) = Ω_{D}^{∇}(S). By Definition 9, there exist m ∈ ℕ and a sequence T_{0}, …, T_{m} in ℘_{f}(D) where T_{0} = S, T_{m} = Ω_{D}^{∇}(S) and, for each 0 < i ≤ m, there exist 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};  (17)
∀d_{i} ∈ T_{i} : ∃d ∈ S_{2} . d ⊢ d_{i};  (18)
∀d_{i} ∈ T_{i} \ S : ∃d ∈ S_{1} . d ⊩_{∇} d_{i};  (19)
∀d ∈ S_{1} : ∃d_{i} ∈ T_{i} . d ⊢_{∇} d_{i}.  (20)

Letting i = m in properties (17) and (18) we obtain S_{2} ⊢_{EM} Ω_{D}^{∇}(S), so that property (6) 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 (19), we obtain that property (7) in Definition 6 holds. Thus Ω_{D}^{∇} is an extrapolation heuristics for D̂_{P}. Moreover, letting i = m in property (20), we obtain that property (8) in Definition 8 holds, so that Ω_{D}^{∇} 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, we have m > 0 and assume that i > 0. By Definition 9, if d_{i−1} ∈ T_{i−1}, then there exists d_{i} ∈ T_{i} such that either d_{i−1} = d_{i} or there exists d′_{i−1} ∈ T_{i−1} such that d_{i−1} ⊩ d′_{i−1} ≠ d_{i} and d_{i} = d_{i−1} ∇ d′_{i−1}; in both cases, d_{i−1} ⊢_{∇} d_{i}. Thus, assuming properties (17), (18), (19) and (20) hold for i − 1, they also hold for i. ⊓ ⊔

Proof (of Theorem 1). We first prove condition (1) of Definition 1, i.e., S_{2} ⊢_{P} S_{1} _{k}∇_{P} S_{2}. Assume the notation and the hypotheses introduced in Definition 11 and let T := S_{1} _{k}∇_{P} S_{2} = h∇_{P}(S_{1}, ⇑_{k} S_{2}). By Definition 10, S_{2} ⊢_{P} ⇑_{k} S_{2} and, by Definition 6, ⇑_{k} 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 sequence defined by U_{0} := T_{0} and, for each i > 0,

U_{i} := U_{i−1} _{k}∇_{P} T′_{i},

where T′_{i} = U_{i−1} ⊕_{P} T_{i}. Suppose that i > 0. By Definition 5, U_{i−1} ⊢_{P} T′_{i}. By the first part of the proof, 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).

Consider any j ≥ 0 such that U_{j} ≠ ∅ and suppose d_{j} ∈ U_{j}. By Definition 11, we have U_{j+1} = h∇_{P}(U_{j}, ⇑_{k} T′_{j}). By condition (8) in Definition 8, 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 d_{j} ⊢_{∇} d_{m} and, for all i ≥ m, d_{m} ∈ U_{i}.

Reasoning towards a contradiction, suppose that the widened sequence does not converge in a finite number of steps. Then, by the point above, there exists ℓ ∈ ℕ and U ∈ ℘fn^{⊢}(D) where # U > k and U ⊆ U_{i} for all i ≥ ℓ. In particular, we have U ⊆ U_{ℓ} ∩ U_{ℓ+1}. By condition (7) in Definition 6, U ⊆ ⇑_{k} T′_{ℓ+1} so that #(⇑_{k} T′_{ℓ+1}) > k contradicting Definition 10. Thus the widened sequence converges in a finite number of steps. ⊓ ⊔

Proof (of Proposition 3). By Proposition 1, H∇_{P} is an extrapolation heuristics for D̂_{P}. Therefore, using the notation of Definition 6, it remains to show that H∇_{P}(S_{1}, S_{2}) = S_{2} ⊕_{P} Ω_{D}^{⊢}(S) where

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

satisfies property (9) of Definition 12. In Proposition 1, we have shown that equation (13) holds.

Assume that d ∈ H∇_{P}(S_{1}, S_{2}) ∩ S_{2} and d_{1} ∈ S_{1} are such that d_{1} ⊩ d. Then d_{1} ∇ d is defined and is in S. By Definition 4, there exists d′ ∈ Ω_{D}^{⊢}(S) such that d_{1} ∇ d ⊢ d′; also, as ‘∇’ is a widening, d ⊢ d_{1} ∇ d. Again by Definition 4, there exists d′′ ∈ Ω_{D}^{⊢}(S_{2} ∪ Ω_{D}^{⊢}(S)) = H∇_{P}(S_{1}, S_{2}) such that d′ ⊢ d′′. To summarize,

d ⊢ d_{1} ∇ d ⊢ d′ ⊢ d′′.

Since we observed that both d, d′′ ∈ H∇_{P}(S_{1}, S_{2}) ∈ ℘fn^{⊢}(D), non-redundancy implies that d = d′′, so that

d = d_{1} ∇ d = d′ = d′′.

Since d′ ∈ S, we also have d ∈ S. Thus, there exist d′_{1} ∈ S_{1} and d_{2} ∈ S_{2} such that d = d′_{1} ∇ d_{2} and hence d′_{1} ⊩_{∇} d, proving property (9) of Definition 12. ⊓ ⊔

Proof (of Theorem 2). We first prove condition (1) in Definition 1, i.e., S_{2} ⊢_{P} S_{1} _{EM}∇_{P} S_{2}. Assume the notation and the hypotheses introduced in Definition 13 and let T := S_{1} _{EM}∇_{P} S_{2} = h∇_{P}(S_{1}, S′_{2}). As ‘⊞_{EM}’ is a connector, we have S_{2} ⊢_{EM} S_{1} ⊞_{EM} S_{2}. Thus, in both the cases of the definition of S′_{2}, 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 sequence defined by U_{0} := T_{0} and U_{i} := U_{i−1}_{EM}∇_{P}(U_{i−1}⊕_{P}T_{i}), for each i > 0.

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 13, 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 (6) 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 (7) of Definition 6 and (9) of Definition 12 can be rewritten to the simpler property:

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

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 (21), we have

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

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};  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 (22), ‘_{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 (22), 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 nonredundant 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. ⊓ ⊔

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

Definition 19. (‘ ↷_{L}’.) Let (O, ⪯, μ) be a finite convergence certificate for the widening operator ‘∇’ on D̂. The relation ↷_{L} ⊆ ℘fn^{⊢}(D)×℘fn^{⊢}(D) induced by μ is such that, for each S_{1}, S_{2} ∈ ℘fn^{⊢}(D), S_{1} ↷_{L} S_{2} holds 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 base-level widening operator ‘∇’, so that ⟨O, ⪯⟩ satisfies the ascending chain condition. As noted in Section 2, the induced poset ⟨M(O), ⪯⪯⟩ also satisfies the ascending chain condition. As a consequence, the lexicographic product of ‘⪯’ and ‘⪯⪯’ satisfies the ascending chain condition on the product O×M(O). Note that, by Definition 19, S_{1} ↷_{L} S_{2} holds if and only if there is a strict increase in this lexicographic product ordering, so that ‘ ↷_{L}’ satisfies the ascending chain condition. ⊓ ⊔

Proof (of Proposition 4). By hypotheses, the certificate (O, ⪯, μ) is such that both ‘⪯’ and μ are finitely computable. Thus, the finite computability of the relation ‘ ↷_{P}’ is an easy consequence of the way it is defined and the fact that we only consider finite sets and multisets.

We first show that, for all S_{i}, S_{i+1}, S_{i+2} ∈ D̂_{P},

S_{i} ↷_{P} S_{i+1} ↷_{P} S_{i+2} ⟹ (S_{i} ↷_{L} S_{i+1}) ∨ (S_{i} ↷_{L} S_{i+2}). (23)

There are three cases corresponding to the three conditions in Definition 14. If S_{i} ↷_{P} S_{i+1} holds by virtue of condition (10), then μ(⨁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 (12), then both μ(⨁S_{i}) = μ(⨁S_{i+1}) and μ̃(S_{i}) ≺≺ μ̃(S_{i+1}), which again implies S_{i} ↷_{L} S_{i+1}. Otherwise, S_{i} ↷_{P} S_{i+1} must hold by virtue of condition (11) so that μ(⨁S_{i}) = μ(⨁S_{i+1}) and # S_{i+1} = 1. However, S_{i+1} ↷_{P} S_{i+2} also holds and, as # S_{i+1} = 1, this may only happen by virtue of condition (10) so that μ(⨁S_{i+1}) ≺ μ(⨁S_{i+2}). Thus,

μ(⨁S_{i}) = μ(⨁S_{i+1}) ≺ μ(⨁S_{i+2})

and S_{i} ↷_{L} S_{i+2}.

We prove that ‘ ↷_{P}’ satisfies the ascending chain condition by contraposition; thus we suppose that there is an infinite chain S_{0} ↷_{P} S_{1} ↷_{P} ⋯ ↷_{P} S_{i} ↷_{P} ⋯ of abstract elements in the finite powerset domain D̂_{P}. Then by (23), there exists a sequence 0 ≤ j_{1} ≤ ⋯ ≤ j_{i} ≤ ⋯ such that S_{0} ↷_{L} S_{j_{1}} ↷_{L} ⋯ ↷_{L} S_{j_{i}} ↷_{L} ⋯ and, for all i ∈ ℕ, j_{i} ≥ i. Thus this sequence is also infinite which contradicts the result of Lemma 1 that ‘ ↷_{L}’ satisfies the ascending chain condition. ⊓ ⊔

Proof (of Theorem 3). Let S_{1}, S_{2} ∈ ℘fn^{⊢}(D), where S_{1} ⊩_{P} S_{2} and let T := S_{1} _{μ}∇_{P} S_{2}. Let S := S_{1} ⊞_{P} S_{2}. Then, as ‘ ⊞_{P}’ is an upper bound operator on D̂_{P} we have

S_{1} ⊩_{P} S_{2} ⊢_{P} S.  (24)

We first prove that condition (1) in Definition 1 holds, i.e., S_{2} ⊢_{P} T. Consider each of the three cases in Definition 16 separately. If the first case applies, then T = S and the result holds by (24). If the second case applies, then T = S ⊕_{P} {d} so that as ‘ ⊕_{P}’ is the least upper bound operator, the result follows again by (24). 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 4, ‘↷_{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 16. If the first case is applied, then the applicability condition trivially ensures that S_{1} ↷_{P} T.

If the second case is applied, then T = S ⊕_{P} {d}, where

d := d_{1} ⊖ d_{2};
d_{1} := ⨁S_{1} ∇ ⨁S;
d_{2} := ⨁S.

Note that the applicability condition ⨁S_{1} ⊩ ⨁S for this case ensures that the 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 15, we know that

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} ⨄ T_{1}  P_{d} \begin{matrix}T_{2} = \{P_{4}, P_{5}\} \\ U_{1} = \{⨄ T_{1}\} \\ U_{2} = \{P_{4}, P_{d}\} \end{matrix}

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

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

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

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

μ(⨁S_{1}) ≺ μ(⨁S_{1} ∇ ⨁S) = μ(⨁T ),

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

Finally, suppose that the last case is applied. Then T = {⨁S_{2}} so that ⨁T = ⨁S_{2}. It follows from (24) that ⨁S_{1} ⊢ ⨁T ⊢ ⨁S. As the condition for the second case of Definition 16 does not hold, ⨁S_{1} = ⨁S, which implies ⨁S_{1} = ⨁T and μ(⨁S_{1}) = μ(⨁T ). By (24), S_{1} ⊩_{P} T so that # S_{1} > 1. Since # T = 1, condition (11) of Definition 14 is satisfied and S_{1} ↷_{P} T. ⊓ ⊔

It should be noted that case (11) of Definition 14 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 also made necessary the addition of the extra conditions on the cardinalities of S_{1} and S_{2} in case (12) of Definition 14, since without these the relation would have violated the ascending chain condition. This is illustrated by the following example.

Example 12. 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 Definition 3 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} T_{2} ⊢_{P} ⋯ starting with elements

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

as in the three diagrams in Figure 7. Then, the first three elements of widened sequence U_{0} ⊢_{P} U_{1} ⊢_{P} U_{2} ⊢_{P} ⋯ can be computed as follows. First U_{0} := T_{0}. Then, since U_{0} ⊢_{P} T_{1}, we have U_{1} := U_{0} _{μ}∇_{P} T_{1} = T_{0} _{μ}∇_{P} T_{1}. As ⨄ T_{0} = ⨄ T_{1}, # T_{1} > 1 and

μ̃_{s}(T_{0}) = {(0, 3), (0, 3)}

⊀≺_{s} {(0, 3), (0, 3), (0, 3)} = μ̃_{s}(T_{1}),

the last case in Definition 16 applies so that U_{1} = {⨄ T_{1}}, as is indicated in the lower square in the right-hand diagram of Figure 7. Thus U_{1} ⊢_{P} T_{2}, so that the widened iterate U_{2} := U_{1} _{μ}∇_{P} T_{2} is defined. Since

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

but

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

without the extra condition # U_{1} > 1 in case (12) of Definition 14, we would apply the first case in Definition 16, obtaining T_{2} as the next element of the widened sequence. However, it can be seen that T_{2} has the same structure as U_{0} = T_{0} (the former being obtained from the latter by a suitable affine transformation) so that the sequence T_{0}, T_{1}, T_{2} and the corresponding “widened” sequence U_{0}, U_{1}, T_{2} can be extended indefinitely without obtaining convergence (in a finite number of steps). In contrast, since we do require the condition # U_{1} > 1, the second case of Definition 16 applies and we compute U_{2} = T_{2} ⊎_{P} {P_{d}} = {P_{4}, P_{d}}, where P_{d} is the (unbounded) polyhedron indicated by the dotted lines in the right-hand diagram.

Proof (of Proposition 5). 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}. By Definition 5, this implies ⋃ S′_{1} ⊆ ⋃ S_{1} so that ⋃ S′_{1} ⊆ ⋃ S_{2}. Let

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

so that, by Definitions 4 and 5, S′′_{1} ⊢_{P} S_{2}. Moreover, by Definition 4, ⋃ S′′_{1} = ⋃ S′_{1} ∩ ⋃ S_{2} which implies that ⋃ S′_{1} = ⋃ S′′_{1} so that ⨄ S′_{1} = ⨄ S′′_{1}. Thus, by Definition 17, 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 17, 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} and S′_{1} ⊬_{P} S_{2}. Moreover, if S′′_{1} ∈ ℘fn^{⊆}(ℂℙ_{n}) is such that ⨄ S′′_{1} = ⨄ S′_{1}, then we must have S′′_{1} = S′_{1} so that S′′_{1} ⊬_{P} S_{2}. Hence, by Definition 17, 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 6, 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 20. Let ‘∼’ 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_{∼}(S_{1i}, {d_{i}}) holds. Then we write merge n_{∼}(S_{1}, S_{2}) and say that S_{2} is a non-redundant merge of S_{1}.

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

Proof. As S_{1} ≠ S_{2} and merge_{∼}(S_{1}, S_{2}) holds, by Definition 18, S_{1} ⊩_{P} S_{2} so that there exists d_{2} ∈ S_{2} \ S_{1}. Therefore, also by Definition 18, there exists S′_{1} ⊆ S_{1} (so that d_{2} ∉ S′_{1}) where {d_{2}} ∼ S′_{1}. Since ‘∼’ refines the ⊕- congruence relation, we obtain d_{2} = ⨁S′_{1} so that S′_{1} ≠ {d_{2}} and # S′_{1} > 1. Let S′_{2} = (S_{1} \ S′_{1}) ⊕_{P} {d_{2}}. Then, by Definition 5, # S′_{2} < # S_{1} and, by Definition 18, merge_{∼}(S_{1}, S′_{2}) holds. 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 20, merge n_{∼}(S_{1}, S′_{2}). ⊓ ⊔

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

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