as independent. This is manifested in the representation, that is, the choice of abstract domain, then reflected in the way computations are modelled as transformers, as well as the use of widening in handling loops. Not tracking relationships in the abstract domain gives scalability but at the cost of precision; the results are over-approximate, hence the results are safe, but possibly giving false alarms. Too many false alarms makes the verification process unusable.
Abstract domains based on polyhedra have been considered since the introduction of abstract
interpretation [
Weakly relational domains usually maintain their representations in a closed form [
This paper is about widening, and especially about the geometric challenges arising when working with a (weakly) relational numeric domain to handle some of the relationships that occur between variables.
The paper makes the following contributions: • provides a review of widening techniques for numeric domains and illustrates their application; • gives case studies to illustrate problems with the application of widening; • proposes a new way of treating widening for weakly relational domains maintained in a closed form.
The rest of the paper is structured as follows: Section 2 surveys related work and introduces relevant notation, Section 3 contains a worked example demonstrating the application of weakly relational domains and widening in a program verification context, Section 4 gives problems illustrating points of interest, and provides some tentative solutions, Section 5 concludes.
This work is concerned with widening and abstract domains consisting of sets of linear inequalities, or polyhedral domains. This section gives background on polyhedra and their subclasses, a brief history of widening, details on weakly relational domains and closure, before illustrating the problematic interaction between closure and widening.
The abstract domains of interest in this paper are lattices over sets of inequalities. Several domains are considered, varying in the form of inequalities that are allowed. The first of these is Polyhedra, Poly , the set of all linear inequalities over a set of variables . Here (and throughout this paper), coeficients and constants are rationals, but other choices are available.
Poly = {11 + ... + ≤ | 1, ..., ∈ ∧ 1, ..., , ∈ Q}
Then ⟨(Poly ), ⊑, ⊔, ⊓⟩ is a complete lattice, that is, sets of polyhedral constraints (implicitly quotiented by equivalence), or rather the solutions to those constraints, are ordered by inclusion (⊑), with greatest lower bound (meet) being geometric intersection (⊓) and least upper bound (join) being convex hull (⊔). Observe that this lattice has infinite ascending chains. The sets of inequalities below lift to lattices in the same way. As well as the lattice operations above, the projection of a set of constraints onto a set of constraints over a subset of variables is an important operation in abstract interpretation.
Abstract interpretation using the Poly domain is seen as impractical beyond small programs
as the size of the representation and the cost of performing operations such as convex hull might
become prohibitively large. Therefore abstract domains based on restricted forms of linear
inequalities have been investigated; that is, the relationships between variables that can be
expressed have been restricted. Hence, these are referred to as weakly relational domains. Many
weakly relational domains have been investigated, and those covered below are not intended to
be a complete list. These (typically) restrict inequalities so that they have at most two variables
in them. This then means that operations such as least upper bound can be calculated by a series
of planar operations; since these planar operations have good computational complexity the
intractability of full polyhedra is avoided. The most general version is then the two variables
per inequality (TVPI) abstract domain [
TVPI = { + ≤ | , ∈ ∧ , , ∈ Q}
The domain of Logahedra [
Definition 3. Log = { + ≤ | , ∈ ∧ , ∈ {− 2, 0, 2 | ∈ Z} ∧ ∈ Q}
Octagons [
Oct = { + ≤ | , ∈ ∧ , ∈ {− 1, 0, 1} ∧ ∈ Q}
Bounded diferences (sometimes also called Zones) have also been popular [
DBM = { − ≤ | , ∈ ∧ ∈ Q}
Finally, using intervals as an abstract domain loses all ability to track relations, but does result in particularly scalable algorithms.
Definition 6. Int = { ≤ | ∈ ∧ ∈ {− 1, 1} ∧ ∈ Q}
When considering intervals, ∈ [, ] is shorthand for {− ≤ − , ≤ }, whilst ∈ [, ∞] is shorthand for {− ≤ − }.
This paper primarily considers TVPI inequalities. Following [
Widening [
Where is a lattice, a widening is then a function ▽ : × → such that: i) ∀, ∈ . ⊑ ▽ ii) ∀, ∈ . ⊑ ▽ iii) for all increasing chains 0 ⊑ 1 ⊑ ..., the chain given by 0 = 0, +1 = ▽+1 is not strictly increasing.
Widening is about sequences of iterates, that is, it is about how the possible values of variables
change at a given program point as control returns to it (for example, in a loop). It is usual to
merge the original abstraction at a widening point with the new value before applying widening
(the definition hints that this is sensible), so ▽ is really ▽( ⊔ ). Notice that widening is
about more than controlled loss of precision within the representation, it is about enforcing
termination. A particularly crude widening would then be to return the top point of the lattice.
One point of interest is that by considering the topological structure of the abstract program
(in particular strongly closed components), widening need only been applied, and termination
checked, at certain nodes in the call graph [
For polyhedral analysis, widening as first introduced [
The danger with the classic approach is that it widens too aggressively, jumping past more
subtle fixpoints leading to an over-approximation that can’t verify a correctness condition.
Various alternatives have been investigated. This includes widening with thresholds [
This relies, to some extent, on the expertise and insight of the person conducting the analysis.
In addition, the technique is typically limited to intervals, that is, bounds on single variables,
and not capturing relational constraints. Another approach is to automate the selection of
thresholds, as suggested in the widening with landmarks approach of [
When using weakly relational domains based on classes of inequalities such as TVPI or Octagons for abstract interpretation, some consideration is required as to how to represent and maintain the sets of inequalities. The choice of representation impacts on the cost of the domain operations, with the choice made as a trade of between the complexity of the operations. Weakly relational domains often use a closed form, where some redundant inequalities are made explicit. After ifnding a closed system all non-redundant inequalities relating any pair of variables are made explicit. For example, suppose that { − ≤ 1, 2 − 3 ≤ 2} is a system of inequalities, then the closed system also includes the redundant inequality 2 − 3 ≤ 4. The relationship between variables , has been made explicit.
A closed system means that a variable can be projected out of a system in constant time by
simply dropping all constraints involving that variable. It also means that least upper bound
computation can be reduced to two dimensional convex hull problems, likewise satisfiability can
be computed at a planar level (plus entailment and equality are straightforward linear operations
with the closed form). These good operations are traded of against the cost of maintaining
the closed form. A typical program analysis step is to consider how a line of (abstracted) code
updates the representation. This is done incrementally, so there is interest in how to update a
closed representation upon the addition of a single new inequality (repeated applications of
this step can be used to find a closed system from an initially unclosed system). Incremental
closure for TVPI has been closely investigated in [
The following reiterates some key definitions from [
vars( + ≤ ) = ⎧⎪ ∅ ⎪ ⎪⎪⎨ ∅
{} ⎪⎪⎪⎪ {} ⎩ {, }
This allows the definition of syntactic projection of a system of inequalities onto a given set of variables: simply select those inequalities including those variables.
Definition 9. The syntactic projection, denoted for some ⊆ , of system of inequalities ⊆ TVPI is defined as () = { ∈ | vars() ⊆ }.
This is used in a formal definition of a closed system of inequalities. Notice that a closed system may include inequalities that are redundant even in a given projection (unary constraints). The entailment operation, |=, is geometric inclusion. If 1 |= 2 and 2 |= 1, then 1 ≡ 2. The definition of closed states that syntactic and semantic projection coincide:
A system ⊆
TVPI is closed if the following predicate holds: closed() ⇐⇒ ∀ ∈ TVPI . ( |= ⇒ vars()() |= )
Some inequalities in a projection might not be wanted, since they are redundant with respect to all projections. The filteroperation will be used to remove these, giving a set of inequalities that is a minimal representation equivalent to the projection (noting that unary constraints are retained, and that points and lines might have many such representations):
The mapping filter: (TVPI ) → (TVPI ) is defined:
filter() = ∪{filter ( ())| ⊆ ∧ | | ≤ 2} where: • filter () ⊆ • filter () ≡ () • for every ′ ⊂ filter (), ′ ̸≡ .
The process of generating implied inequalities is based on the result operator that eliminates a shared variable from a pair of inequalities. In the definition of complete below, result will be lifting to sets of inequalities, referring to all pairwise applications of result.
If 1 ≡ 1 + 1 ≤ 1, 2 ≡ 2 + 2 ≤ 2 and 12 < 0 then
= result(1, 2, ) = |2|1 + |1|2 ≤ | 2|1 + |1|2 otherwise result(1, 2, ) = ⊥.
At this point the function complete can be defined, that results in a minimal set of inequalities which is closed.
Definition 13. ∼= ′ if for all ⊆ such that | | ≤ 2, ( ) ≡ ( ′).
Definition 14. Let ⊆ TVPI . Put 0 = filter( ) and +1 = filter( ∪ result(, )). Then complete : (TVPI ) → (TVPI ) is defined complete( ) = where +1 ∼= and for every 0 ≤ < , +1 ̸∼= .
The following result (proved in [
Theorem 1. Consider adding 0 ∈ TVPI to ⊆ TVPI where complete() = . If ∈ complete( ∪ {0}) and ̸= false, then one of the following holds: 1. ∈ ∪ {0} 2. = result(0, 1) where 1 ∈ 3. = result(result(0, 1), 2) where 1, 2 ∈
There is a problem when using widening whilst calculating a fixpoint over weakly relational domains. Widening attempt to weaken a system of inequalities by discarding inequalities that are not displaying stability. This is syntactically calculated: consider and as sets of inequalities, then ▽ = ∩ . By maintaining a closed representation, weakly relational domains are introducing redundant inequalities into the representation. The interaction of these two is unclear, but an infinite loop of discarding an inequality that is immediately reintroduced by closure is possible.
This problem is illustrated for Octagons by Miné [
= { − ≤ + 1, − ≤ + 1, − ≤ + 1, − ≤ + 1, − ≤ 1, − ≤ 1} Suppose an initial abstraction is:
= { − ≤ 1, − ≤ 1, − ≤ 1, − ≤ 1} then
0 = complete() = { − ≤ 1, − ≤ 1, − ≤ 2, − ≤ 2, − ≤ 1, − ≤ 1} Now consider the first iteration without using widening:
1 = 0 ⊔ 0 = { − ≤ 1, − ≤ 1, − ≤ 2, − ≤ 2, − ≤ 1, − ≤ 1}
The next iteration is calculated with widening, where widening drops the unstable constraints
on , , but closure using the complete function immediately introduces new constraints on
these variables:
1 ⊔ 1 = { − ≤ 2, − ≤ 2, − ≤ 2, − ≤ 2, − ≤ 1, − ≤ 1}
1▽1 = { − ≤ 2, − ≤ 2, − ≤ 1, − ≤ 1}
2 = complete(1▽1) = { − ≤ 3, − ≤ 3, − ≤ 2, − ≤ 2, − ≤ 1, − ≤ 1}
The next iterate is then the below, noting that this time it is the constraints on , that are
unstable:
3 = complete(2▽2) = { − ≤ 3, − ≤ 3, − ≤ 4, − ≤ 4, − ≤ 1, − ≤ 1}
And so on. Closure hasn’t been accounted for in the use of stability in this definition of a
widening, and this isn’t a terminating sequence. Therefore, ▽ isn’t a widening in this context.
The solution proposed is simple [
Gange, et al [
The solution presented in [
A final point of consideration is relaxation of systems of constraints. System of constraints is said to be a relaxation of if ⊏ . Noting again that widening is about enforcing termination, it should also be noted that changing an element from an abstract domain might have another motivation, that is, to maintain a tractable size of representation in order that a fixpoint computation does not grind to a halt. The more expressive the set of constraints underlying the abstract domain is, the more this becomes an issue. The concept of relaxation is geometrical, but again interacts with the syntactic maintenance of a closed form.
This example works through the analysis of a small section of code to illustrate the use of
abstract interpretation using weakly relational domains for program verifcation. For a full
introduction to abstract interpretation see [
Consider the following implementation of a C standard library function, with line numbers: ( 1 ) ( 2 ) ( 3 ) ( 4 ) ( 5 ) ( 6 ) ( 7 ) ( 8 ) ( 9 ) c h a r ∗ s t r d u p ( c o n s t c h a r ∗ s ) { s i z e _ t n = s t r l e n ( s ) ; c h a r ∗ r e s u l t = m a l l o c ( n + 1 ) ; s i z e _ t i = 0 ; s i z e _ t j = 0 ; w h i l e ( i < n ) { r e s u l t [ j ] = s [ i ] ;
If it is known that s points to a valid C string and strlen returns its length then this is clearly memory-safe. When reading from s, ∈ [0, − 1] and when writing to ∈ [0, ]. Showing this via abstract interpretation is not as simple as it might appear.
First consider using the Int{,,} abstract domain, and assume no hidden dependencies. At the start of the loop on line (8) observe that ∈ [0, 0], ∈ [0, 0], ∈ [0, ∞], as in Figure 1 a).
Each instruction in the code has an abstract equivalent transforming the lattice point as
passed to that line. For example, on line (10) the increment on the program variable i will
correspondingly shift the polyhedron representing the program state at this point by one in the
i direction. At the end of the first iteration around the loop, at line (12) ∈ [
Repeating this will result in the intervals for the variables at line (8) increasing. However, this process will not terminate, since the values will not stabilise at a fixpoint. This necessitates widening. To accelerate (or indeed to reach) a fixpoint, information is discarded or generalised, until the abstract domain value at the merge point is stable. The classic way to apply widening is to execute the abstract loop two or three times, then to observe which constraints are stable from one iteration to the next, retaining only these. The result is a fixpoint. Note that this is often a syntactic observation, and that two semantically equivalent but syntactically diferent points might well result in widening being applied.
Using interval domain Int{,,} , for and only the lower bounds are stable across iterations,
hence widening applies:
{ ∈ [
= { ∈ [0, ∞], ∈ [0, ∞], ∈ [0, ∞]} This is a fixpoint (indeed the least fixpoint for this choice of abstract domain), but this does not verify memory safety at line (13). An analysis using this would throw a spurious warning to the developer.
The Int abstract domain does not track relations between variables. The verification failure above suggests a need to track (some) relations between variables. Equalities might make a tempting choice of abstract domain: = is a loop invariant at the head of the loop, however it is not maintained during the loop; at the start of line (11) = + 1, so something more expressive than equalities is needed.
Consider using the TVPI{,,} domain. At the first merge point considered above, the same inequalities are merged. The least upper bound calculation results in {− ≤ 0, − ≤ 0, ≤ , − ≤ 0, − ≤ 0, ≤ 1, ≤ 1}. This represents a section of plane reaching through = (see Figure 1 b)). Repeating this will result in the plane section increasing in size (as in Figure 1 c)). At the next iteration widening is applied, retaining only the stable inequalities {− ≤ 0, − ≤ 0, ≤ , − ≤ 0, − ≤ 0}. as illustrated in Figure 1 d). This fixpoint implies that ≤ (indeed in the closed representation used this will be explicit) hence the array access on line (13) can be verified. This would be the case if unrestricted polyhedra were used, but also if a less expressive weakly relational domain such as Oct{,,}, or even bounded diferences, DBM{,,}, were used.
This section works through three examples illustrating the use of widening in over-approximating ifxpoints within geometric structures. It discusses the related use of relaxation to throttle the size of representation and in particular addresses the problems that can arise whilst applying widening with weakly relational domains. 4.1. Problem 1 Consider a transfer function for sets . This translates a shape (approximation) by one unit in the -axis, and takes its join with a point half way between the top right hand corner of the translated shape and = 2, and with the original .
+1 = ∪ {(, + 1) | (, ) ∈ } ∪ {(1 + max2() , max() + 1)} With initial set 0 = {(, ) | − ≤ 0, ≤ 1, − ≤ 0}, this gives the monotonic sequence of spaces illustrated in Figure 2. 1 3
Consider applying widening to this sequence, with abstract domains Int{,}, Oct{,}, TVPI{,}.
In the first instance, each will be approximated by its bounding box. When classic widening is applied the increasing upper bounds on and will be unstable and the fixpoint {− ≤ 0, − ≤ 0} will be found. If widening with thresholds were applied and threshold = 2 were supplied then a stronger over-approximation would be found, namely {− ≤ 0, ≤ , − ≤ 0}. Repeating with Octagons, with for ≥ 1, the space can’t be precisely described, and the end result after widening would add the − ≤ 0 constraint to the fixpoint calculated with intervals (either with or without thresholds).
Analysing with TVPI, each space can be precisely described and the set of constraints will grow as in the picture, {− ≤ 0, − ≤ 0, − ≤ 0, − 2 ≤ 0.5, − 4 ≤ 1, − 8 ≤ 1.5, ...} (plus upper bounds on and ). In fact, these constraints are in Log{,}. When widening is applied, all but the final constraint (and the upper bounds) will be stable. Again, a widening with thresholds approach might add an upper bound on .
The classic widening is typically applied after two or three iterations without widening. In this example, there is an attraction in applying more iterations to get a better approximation. This presents three problems to be addressed: i) the practical question of how many inequalities to maintain, and how to relax the system to control the number of inequalities; ii) the practical question of how to determine the number of iterations to apply before using widening; iii) the theoretical question of how to recognise the bound being approached as the limit of the sequence of inequalities, and add this without relying on up front thresholds. 4.2. Problem 2 Scientific programming often uses trigonometric functions. Analysis of these can be problematic. Consider a transfer function for set of points , parameterised by constant , where is an angle. +1 = {((.cos( ) − .sin( ), (.sin( ) + .cos( )) | (, ) ∈ , ∈ [0, 2 ), ∈ Q} ⊔ This rotates the current iteration by , scaling by and taking the least upper bound with the previous iterate. Notice that if = 1 then vertices of the described space are points on the circumference of a circle; if > 1 then points diverge; if < 1 then points become closer to the centre of the circle. Figure 3 illustrates some possible iterations with 0 = {(4, 0)}, and various choices for and .
Case a) has = 3 and = 1. Here, a fixpoint describing the space is a hexagon which can be described with TVPI inequalities; this would be found assuming that the analysis was run for a suficient number of iterations without widening. Notice that if the abstract domain used were intervals or Octagons then each iterate would over-approximate the space, this space will diverge, and when widening is applied to enforce termination the result would be the top element, the whole plane.
Case b) has = 310 and = 1. This is somewhat similar to case a), although the analysis needs more iterations (and three times round the circle) to reach a fixpoint, which will be an icosagon. The diagram illustrates the approximation after seven iterations, with the arrow pointing to the point that will need to be incorporated when the next least upper bound is calculated. It isn’t − 4 − 3 − 2 − 1 − 1 1 2 3 4 3 2 1
too hard to see how can be chosen so that the fixpoint is arbitrarily complicated, or indeed non-existent. This might motivate some kind of relaxation, however, such a relaxation will always lead to an over-appoximation of the space including points from without the circle, and the space diverges, as above. The desired fixpoint is the circle, but this can’t be represented using polyhedral domains.
As noted above, if > 1 then the approximation will always diverges, hence the only fixpoint is the whole plane.
Now suppose that < 1. There is a critical value for where fixpoint behaviour changes, √ that is when = 22 . As can be seen in Figure 3 d) this is the value at which the iteration of a bounding box is contained within itself; this will be discussed further below. In Figure 3 c), √ = 4 and = 0.8 > 22 . The iterations are approximated by a spiral, leading to the fixpoint illustrated. Again, this can be modelled with TVPI constraints. Suppose instead that this was approximated using Int{,}. 1 would be overapproximated with the dashed box whose bottom right corner is (4, 0). To calculate 2 this space is translated to give the dashed box tilted by 4 and the least upper bound is calculated, resulting in the containing box. 2 contains points outside of the circle and further iterations will diverge. Once widening is applied the result will again be the plane, the top element of the lattice of Int{,}. √
Finally, consider the case illustrated in Figure 3 d). Here, = 4 and = 22 . To illustrate the point, a rather gross over-approximation of the space is given by the bounding box which translates into a subspace of itself at the next iteration, and widening need not be considered. As previously, this space can be described precisely in TVPI{,}, whilst (as shown by the dotted lines) Oct{,} can also approximate this space, reaching a fixpoint.
This discussion has illustrated some of the issue arising when computing fixpoints of iterates built using trigonometric functions. It poses several questions: i) what is the correct patience to show before performing widening? ii) when and how can polyhedral approximations be relaxed to given improved performance and fixpoints? iii) what is the right domain to use when analysing code using trigonometric (as in this case, matrix) functions? One response to the last question might be that polyhedral approximations are the wrong choice and a domain capturing circles and ellipses, such as that in [25], might be a better choice. In this case, an addition question is how do polyhedral abstract domains interact with non-polyhedral abstract domains? 4.3. Problem 3 This section returns to the example from Section 2.4, which demonstrated problematic behaviour when closure and widening interact. As noted there, the problem arises because widening is essentially a semantic notion about how (for geometric systems) the space is allowed to expand, but that it is often implemented syntactically by observing the form of constraints. To put it another way, is the lattice of polyhedra a lattice of convex spaces, or is it a lattice of sets of inequalities? Closure is a syntactic notion and the redundant inequalities introduced interfere with the straightforward correspondence, that the classic approach to widening relies upon, between stability of inequalities and the way in which they are removed.
A widening is given below that injects some semantics into the procedure, using entailment checking to determine whether or not apparently stable inequalities should be retained.
Suppose that is a closed system of TVPI inequalities, and that are the inequalities being merged at a widening point. As usual, widening takes place between and ⊔ . The widening proposed performs the classic widening on these inputs, closes the system, then uses entailment checking to remove inequalities whose apparently stability is an artefact of the closed representation maintaining redundant inequalities.
Firstly, compute the classic widening (which of course isn’t a widening in this context), giving a set of constraints ℓ:
complete(▽( ⊔ )) = {1, ..., , +1, ..., } Here, 1, ..., ∈/ (that is, are introduced by closure) and +1, ..., ∈ . Then the new widening +1 = ▽′ is given by: +1 = { | + 1 ≤ ≤ , ∖ { } ̸|= , or |= and +1, ..., − 1, +1, ..., |= } That is, stable inequalities are dropped if ∖ { } |= (they are redundant in ) and +1, ..., − 1, +1, ..., ̸|= (they are non-redundant in complete( ⊔ )). Lemma 1. Where +1 = ▽′ for closed , complete(+1) = +1 Proof. Suppose some ℓ ∈ complete(+1), but ℓ ∈/ +1. Then ℓ can be derived from inequalities in +1 using the result operation. Since +1 ⊆ , ℓ can also be derived from , hence ℓ ∈ +1 by definition.
Lemma 2. ▽′ is a widening.
Proof. Since ▽′ only retains inequalities explicit in the previous iterations, and all iterates are ifnite sets, stability is reached for a set of constraints or the empty set.
Returning to the example from Section 2.4. 0 is as before: 0 = complete() = { − ≤ 1, − ≤ 1, − ≤ 2, − ≤ 2, − ≤ 1, − ≤ 1} Next, 1 is again as before, with no widening applied:
1 = { − ≤ 1, − ≤ 1, − ≤ 2, − ≤ 2, − ≤ 1, − ≤ 1} Now compute the classic widening. Here, the constraints in , are unstable, but new constraints on these variables are introduced in closure. complete(1▽(1 ⊔1)) = { − ≤ 3, − ≤ 3, − ≤ 2, − ≤ 2, − ≤ 1, − ≤ 1} Now compute 2 and observe that
2 = { − ≤ 1, − ≤ 1} The inequalities in , are not stable, hence they are dropped. The inequalities in , are stable, but they were redundant in 1, and are not entailed by the other stable inequalities in complete(1▽(1 ⊔ 1)), hence are dropped along with the unstable inequalities. Also observe that complete(2) = 2, and that this is fixpoint.
Is this entirely satisfactory? Not necessarily, the extensive use of entailment checking might make this widening particularly expensive to apply. However, it might be that a practical implementation marks inequalities introduced by closure, which chimes with the observation that maintaining the widening point as a non-closed system allows a fixpoint to be observed.
The tension between the semantic notion of widening and the syntactic might not be problematic when the convex space has a unique representation using the syntactic representation. However, at least for constraint based systems, a potential problem exists even if a closed system is not maintained: suppose that a point is to be represented as a polyhedron over multiple variables; which constraints are used to do this, there are infinitely many choices? Two successive iterates need to choose the same representation for stability to be syntactically observed. It might be hoped, indeeded expected, that this will be the case, but this needs to be enforced.
A final problem remains. The new widening results in a closed system, but part of the working involves applying closure to the system resulting from the classic widening. This potentially means calculating closure from scratch, which is an expensive operation; what refinements are available to avoid the complete recalculation of closure?
This paper has looked at widening for polyhedral constraints, with a focus on weakly relational domains and TVPI in particular. It has illustrated the importance of capturing relations between variables whilst performing program analysis for verification. The key role of widening in this analysis has been highlighted. The application of widening is not always straightforward and some dificult cases highlighting this have been presented. The interaction between widening and the closed forms maintained in weakly relational domains has been investigated and a new widening has been introduced that gives a new way to sidestep the problem. The paper also contains a lot of questions, some of which require theoretical development of widening, others of which require empirical investigation of the performance of widening. Future work is to address these questions more fully by carrying out experimental work with real-life programs to illuminate where problematic structures occur and where the performance of widening needs to be improved.
Acknowledgements The authors would like to thank Marius Zicius for discussions on two variable per inequality constraints. (2009) 279–323. [25] J. Feret, Static Analysis of Digital Filters, in: Proceedings of the 13th European Symposium on Programming, volume 2986 of Lecture Notes in Computer Science, Springer, 2004, pp. 33–48.