Incrementally closing octagons

We summarise the contributions of our work as follows:The paper is structured as follows: Sect. 2 contextualises this study and Sect. 3 provides the necessary preliminaries. Section 4 critiques the incremental algorithm of Miné, introduces a new incremental quadratic algorithm. Section 5 shows how to recover strong closure incrementally and do so, again, in a single DBM pass. Section 6 explains how to extend incrementally to integer closure. Section 7 suggest various optimisations to the incremental algorithms including in-place update. Experimental results are presented in Sects. 8 and 9 concludes.

An octagonal constraint is a two variable inequality of the form \( \pm \, x_i \pm x_j \le d \) where \(x_i\) and \(x_j\) are variables and d is a constant. An octagon is a set of points satisfying a system of octagonal constraints. The octagon domain is the set of all octagons that can be defined over the variables \(x_0, \ldots , x_{n-1}\).

Implementations of the octagon domain reuse the machinery developed for solving difference constraints of the form \(x_i - x_j \le d\). Miné [22] showed how to translate octagonal constraints to difference constraints over an extended set of variables \(x'_0, \ldots , x'_{2n-1}\). A single octagonal constraint translates into a conjunction of one or more difference constraints as follows:A common representation for difference constraints is a difference bound matrix (DBM) which is a square matrix of dimension \(n \times n\), where n is the number of variables in the difference system. The value of the entry \(d = {\mathbf {m}}_{i,j}\) represents the constant d of the inequality \(x_i - x_j \le d\) where the indices \(i,j \in \{ 0, \ldots , n - 1 \}\). An octagonal constraint system over n variables translates to a difference constraint system over 2n variables, hence a DBM representing an octagon has dimension \(2n \times 2n\).

The interpretation of a DBM representing an octagon is different to a DBM representing difference constraints. Consequently there are two concretisations for DBMs: one for interpreting differences and another for interpreting octagons, although the latter is defined in terms of the former:

Operations on a DBM representing an octagon must maintain equality between the two entries that share the same constant of an octagonal inequality. This requirement leads to the definition of coherence:

The bar operation can be realised without a branch using \(\bar{\imath }= i\;\mathbf xor \;1\) [21, Section 4.2.2]. Care should be taken to preserve coherence when manipulating DBMs, either by carefully designing algorithms or by using a data structure that enforces coherence [21, Section 4.5]. For clarity, we abstract away from the question of how to represent a DBM by presenting all algorithms for square matrices, rather than triangular matrices as introduced in [21, Section 4.5]. One final property is necessary for satisfiability:

Intuitively, consistency means that there is not negative cycle in the DBM, which corresponds to unsatisfiability [6].

Closure properties define canonical representations of DBMs, and can decide satisfiability and support operations such as join and projection. Bellman [6] showed that the satisfiability of a difference system can be decided using shortest path algorithms on a graph representing the differences. If the graph contains a negative cycle (a cycle whose edge weights sum to a negative value) then the difference system is unsatisfiable. The same applies for DBMs representing octagons. Closure propagates all the implicit (entailed) constraints in a system, leaving each entry in the DBM with the sharpest possible constraint entailed between the variables. Closure is formally defined below:

Closure is not enough to provide a canonical form for DBMs representing octagons. Miné defined the notion of strong closure in [21, 22] to do so:

The strong closure of DBM \(\mathbf {m}\) can be computed by \(\textsc {Str}(\mathbf {m})\), the code for which is given in Fig. 4. The algorithm propagates the property that if \(x'_j - x'_{\bar{\jmath }} \le c_1\) and \(x'_{\bar{\imath }} - x'_i \le c_2\) both hold then \(x'_j - x'_i \le (c_1 +c_2)/2\) also holds. This sharpens the bound on the difference \(x'_j - x'_i\) using the two unary constraints encoded by \(x'_j - x'_{\bar{\jmath }} \le c_1\) and \(x'_{\bar{\imath }} - x'_i \le c_1\), namely, \(2x'_j \le c_1\) and \(-2x'_i \le c_2\). Note that this constraint propagation is not guaranteed to occur with a shortest path algorithm since there is not necessarily a path from a \({\mathbf {m}}_{i,\bar{\imath }}\) and \({\mathbf {m}}_{\bar{\jmath },j}\). An example in Fig. 2 shows such a situation: the two graphs represent the octagon, but a shortest path algorithm will not propagate constraints on the left graph; hence strengthening is needed to bring the two graphs to the same normal form. Strong closure yields a canonical representation: there is a unique strongly closed DBM for any (non-empty) octagon [22]. Thus any semantically equivalent octagonal constraint systems are represented by the same strongly closed DBM. Strengthening is the act of computing strong closure.

For octagonal constraints over integers, the strong closure property may result in non-integer values due to the division by two. The definition of strong closure for integer octagonal constraints thus needs to be refined. If \(x_i\) is integral then \(x_i \le c\) tightens to \(x_i \le \lfloor c \rfloor \). Since \(x_i \le c\) translates to the difference \(x'_{2i} - x'_{2i + 1} \le 2c\), tightening the unary constraint is achieved by tightening the difference to \(x'_{2i} - x'_{2i + 1} \le 2\lfloor c/2 \rfloor \).

For the integer case, a tightening step is required before strengthening. Tightening a closed DBM results in a weaker form of closure, called weak closure. Strong closure can be recovered from weak closure by strengthening [1]. Note, however, that we introduce the property for completeness of exposition because our formalisation and proofs do not make use of this notion.

Figure 3 gives a high-level overview of closure calculation. First a closure algorithm is applied to a DBM. Next, consistency is checked by observing the diagonal has non-negative entries indicating the octagon is satisfiable. If satisfiable, then the DBM is strengthened, resulting in a strongly closed DBM. Note that consistency does not need to be checked again after strengthening. The dashed lines in the figure show the alternative path taken for integer problems: to ensure that the DBM entries are integral, a tightening step is applied which is then followed by an integer consistency check and strengthening.

Figure 4 shows how this architecture can be instantiated with algorithms for non-incremental strong closure. A Floyd-Warshall all-pairs shortest path algorithm [13, 36] can be applied to a DBM to compute closure, which is cubic in n. The check for consistency involves a pass over the matrix diagonal to check for a strictly negative entry, as illustrated in the figure. (Note that CheckConsistent resets a strictly positive diagonal entry to zero as in [2, 22], but the incremental algorithms presented in this paper never relax a zero diagonal entry to a strictly positive value. Hence the reset is actually redundant for the incremental algorithms that follow.) The consistency check is linear in n. Strong closure can be additionally obtained by following closure with a single call to Str, the code for which is also listed in the figure. This is quadratic in n.

Miné designed an incremental algorithm based on the observation that a new constraint will not affect all the variables of the octagon [21, Section 4.3.4]. Without loss of generality, suppose the inequality \(x'_a - x'_b \le d\) is added to the DBM (unary constraints are supported by putting \(b = \bar{a}\)). Adding \(x'_a - x'_b \le d\) implies that the equivalent constraint \(x'_{\bar{b}} - x'_{\bar{a}} \le d\) is added too, and the entries \({\mathbf {m}}_{a,b}\) and \({\mathbf {m}}_{\bar{b},\bar{a}}\) are updated to d to reflect this. Figure 5 presents a version of the incremental algorithm of Miné, specialised for adding \(x'_a - x'_b \le d\) to a closed DBM. The algorithm relies on the observation that updating \({\mathbf {m}}_{a,b}\) and \({\mathbf {m}}_{\bar{b},\bar{a}}\) will only (initially) mutate the rows and columns for the \(x'_a,x'_b,x'_{\bar{a}}, x'_{\bar{b}}\) variables. Put \(v = \min (a, b, \bar{a}, \bar{b})\). Since \(\mathbf {m}\) was closed, despite the updates, it still follows that if \(k < v\) then \({\mathbf {m}}_{i,j} \le {\mathbf {m}}_{i,k} + {\mathbf {m}}_{k,j}\) for all \(0 \le i < 2n\) and \(0 \le j < 2n\). This is the inductive property which is established after the first v iterations of the outermost for loop of the standard Floyd-Warshall algorithm. Therefore, to restore closure it only necessary to apply the remaining \(2n - v\) iterations of Floyd-Warshall, which leads to the algorithm of Fig. 5.

The incremental closure of Fig. 5 reduces the number of \(\min \) operations from \(8n^3\) to \((2n - v)4n^2\) (notwithstanding those in Str). Prior to the updates, one could conceivably reconfigure the DBM by swapping rows and columns so that, say, \(a = 2n - 4, \bar{a}= 2n - 3, b = 2n - 2, \bar{b}= 2n - 1\). Then \(v = 2n - 4\) reducing incremental closure to \(16n^2\). However, after closure, the rows and columns would need to be swapped back to maintain a consistent representation. Observe too that \(x'_{a} - x'_{b} \le d\) and \(x'_{e} - x'_{f} \le d\) can be added to the DBM simultaneously by putting \(v = \min (a, b, \bar{a}, \bar{b}, e, f, \bar{e}, \bar{f})\) and then applying incremental closure once.

To give the intuition behind our new incremental closure algorithm, consider adding the constraint \(x'_a - x'_b \le d\) and \(x'_{\bar{b}} - x'_{\bar{a}} \le d\) to the closed DBM \(\mathbf {m}\). The four diagrams given in Fig. 6 illustrate how the path between variables \(x'_i\) and \(x'_j\) can be shortened. The distance between \(x'_i\) and \(x'_j\) is c (\({\mathbf {m}}_{i,j} = c\)), the distance between \(x'_i\) and \(x'_a\) is \(c_1\) (\({\mathbf {m}}_{i,a} = c_1\)), etc. The wavy lines denote the new constraints \(x'_a - x'_b \le d\) and \(x'_{\bar{b}} - x'_{\bar{a}} \le d\) and the heavy lines indicate short-circuiting paths between \(x'_i\) and \(x'_j\). The bottom left path of the figure illustrates how the distance between \(x'_i\) and \(x'_a\) can be reduced from \(c_1\) by the \(x'_{\bar{b}} - x'_{\bar{a}} \le d\) constraint. The same path illustrates how to shorten the distance between \(x'_{\bar{a}}\) and \(x'_j\) from \(c'_2\) using the \(x'_a - x'_b \le d\) constraint. The bottom right path of the figure gives two symmetric cases in which \(c'_1\) and \(c_2\) are sharpened by the addition of \(x'_a - x'_b \le d\) and \(x'_{\bar{b}} - x'_{\bar{a}} \le d\) respectively. Note that we cannot have the two paths from \(x'_i\) to \(x'_a\) and from \(x'_b\) to \(x'_j\) both shortened: at most one of them can change. The same holds for the two paths from \(x'_i\) to \(x'_{\bar{b}}\) and \(x'_{\bar{a}}\) to \(x'_j\). These extra paths lead to the following strategy for updating \({\mathbf {m'}}_{i,j}\):This leads to the incremental closure algorithm listed in top of Fig. 7. Quintic \(\min \) can be realised as four binary \(\min \) operations, hence the total number of binary \(\min \) operations required for IncClose is \(16n^2\), which is quadratic in n. The listing in the bottom of the figure shows how commonality can be factored out so that each iteration of the inner loop requires a single ternary \(\min \) to be computed. Factorisation reduces the number of binary \(\min \) operations to \(2n(2 + 4n)\) = \(8n^2 + 4n\) in IncCloseHoist. Moreover, this form of code hoisting is also applicable algorithms that follow (though this optimisation is not elaborated in the sequel). Furthermore, like IncClose, IncCloseHoist is not sensitive to the specific traversal order of the DBM, hence has potential for parallelisation. In additional, both IncClose and IncCloseHoist do not incur any checks.

The new incremental algorithm is justified by Theorem 4.1 which, in turn, is supported by the following lemma:

Note that unsatisfiability can be detected without applying any \(\min \) operations at all, though for brevity this is omitted in the presentation of the algorithms. Fast unsatisfiability checking is justified by the following corollary of Lemma 4.1:

An important property of IncClose is idempotence: it formalises the idea that an octagon should not change shape if it is repeatedly intersected with the same inequality. If idempotence did not hold then there would exist \(\mathbf {m'} = \textsc {IncClose}(\mathbf {m}, o)\) and \(\mathbf {m''} = \textsc {IncClose}(\mathbf {m'}, o)\) for which \(\mathbf {m'} \ne \mathbf {m''}\). This would suggest that IncClose did not properly tighten \(\mathbf {m}\) using the inequality o, but overlooked some propagation, which is the form of suboptimal behaviour we are aiming to avoid.

The classical strong closure by Miné repeatedly invokes \(\textsc {Str}\) within the main Floyd-Warshall loop, but it was later shown by Bagnara et al. [2] that this was equivalent to applying \(\textsc {Str}\) just once after the main loop. The following theorem [2, Theorem 3] justifies this tactic, though the proofs we present have been revisited and streamlined:

Theorem 5.1 states that a strongly closed DBM can be obtained by calculating closure and then strengthening. This is realised by calling \(\textsc {IncClose}\), from Fig. 7, followed by a call to \(\textsc {Str}\). Although this is conventional wisdom, it incurs two passes over the DBM: one by \(\textsc {IncClose}\) and the other by \(\textsc {Str}\). The two passes can be unified by observing that strengthening \(\mathbf {m}'\) critically depends on the entries \({\mathbf {m}}_{i,\bar{\imath }}'\) where \(i \in \{ 0, \ldots , 2n - 1 \}\). Furthermore, these entries, henceforth called key entries, are themselves not changed by strengthening because:This suggests precomputing the key entries up front and then using them in the main loop of \(\textsc {IncClose}\) to strengthen on-the-fly. This insight leads to the algorithm listed in Fig. 9. Line 3 generates the key entries which are closed by construction and unchanged by strengthening. Once the key entries are computed, the algorithm iterates over the rest of the DBM, closing and simultaneously strengthening each entry \({\mathbf {m}}_{i,j}\) at line 8.

The total number of binary \(\min \) operations required for IncStrongClose is \(8n + 10n(2n - 1) = 20n^2 - 2n\), which improves on following IncClose by Str, which requires \(16n^2 + 4n^2 = 20n^2\). Furthermore, since \(\mathbf {m}\) is coherent \({\mathbf {m}}_{i,a}+ d + {\mathbf {m}}_{b,\bar{\imath }} = {\mathbf {m}}_{\bar{a},\bar{\imath }} + d + {\mathbf {m}}_{i,\bar{b}} = {\mathbf {m}}_{i,\bar{b}} + d + {\mathbf {m}}_{\bar{a},\bar{\imath }}\) so that the quintic \(\min \) on line 4 becomes quartic, reducing the \(\min \) count for \(\textsc {IncClose}\) to \(20n^2 - 4n\). Furthermore, the entry \({\mathbf {m}}_{i,\bar{\imath }}\) can be cached in a linear array \(\mathbf {a}_i\) of dimension 2n and the expression \(({\mathbf {m'}}_{i,\bar{\imath }} + {\mathbf {m'}}_{\bar{\jmath },j})/2\) in line 8 can be replaced with \((\mathbf {a}_{i} + \mathbf {a}_{\bar{\jmath }})/2\), thereby avoiding two lookups in a two-dimensional matrix. We omit the algorithm using array caching for space reasons as this is a simple change to Fig. 9.

The following theorem justifies the correctness of the new incremental strong closure algorithm:

Code is duplicated in IncStrongClose in the assignments of \({\mathbf {m'}}_{i,\bar{\imath }}\) and \({\mathbf {m'}}_{i,j}\) on lines 3 and 8 respectively. Figure 10 shows how this can be factored out in that line 3 of IncStrongCloseMotion need only consider updates stemming from \({\mathbf {m}}_{i,a} + d + {\mathbf {m}}_{b,\bar{\imath }}\). Moreover, the guard on line 7 of Fig. 9 is eliminated but moving the remainder of the \({\mathbf {m'}}_{i,\bar{\imath }}\) calculation into the main loop. This increases the \(\min \) count by 2n but reduces code size. This can potentially be a good exchange because \(\min \) is itself essentially a check (though it can be implemented as straight-line code for machine integers [35]), and eliminating the guard from the main loop avoids \(4n^2\) checks, giving a saving overall. However, putting asymptotic arguments aside, whether IncStrongCloseMotion outperforms IncStrongClose depends on the relative cost of the integer comparison on line 7 of Fig. 9 to the comparison implicit in line 3 of Fig. 10, which is performed in the underlying number system. The following result justifies this form of code motion:

The force of the above result is that \({\mathbf {m'}}_{i,j}\) is only affected by a change to \({\mathbf {m'}}_{i,\bar{\imath }}\) via \({\mathbf {m}}_{i,a} + d + {\mathbf {m}}_{b,\bar{\imath }}\) or a change to \({\mathbf {m'}}_{\bar{\jmath },j}\) via \({\mathbf {m}}_{\bar{\jmath },a} + d + {\mathbf {m}}_{b,j}\). Thus the initial loop on line 3, need only check whether \({\mathbf {m}}_{i,\bar{\imath }}\) is shortened by \({\mathbf {m}}_{i,a} + d + {\mathbf {m}}_{b,\bar{\imath }}\) in order to correctly update an arbitrary entry \({\mathbf {m}}_{i,j}\) in the loop on line 8. Note that \(\mathbf {m}\) is not just required to be closed, but also strongly closed and coherent.

Figure 13 gives an in-place version of IncClose algorithm listed in Fig. 7. At first glance one might expect that mutating the entries \({\mathbf {m}}_{i,a}\), \({\mathbf {m}}_{b,\bar{\imath }}\), \({\mathbf {m}}_{i,\bar{b}}\), \({\mathbf {m}}_{\bar{a},\bar{\imath }}\), \({\mathbf {m}}_{\bar{a},a}\) or \({\mathbf {m}}_{b,\bar{b}}\) could potentially perturb those entries of \(\mathbf {m}\) which are updated later. The following theorem asserts that this is not so. Correctness follows from Corollary 7.1 which is stated below:

The following theorem asserts that in-place update does not compromise correctness. It is telling that the correctness argument does not refer to the entries \({\mathbf {m}}_{i,a}\), \({\mathbf {m}}_{b,\bar{\imath }}\), \({\mathbf {m}}_{i,\bar{b}}\), \({\mathbf {m}}_{\bar{a},\bar{\imath }}\), \({\mathbf {m}}_{\bar{a},a}\) or \({\mathbf {m}}_{b,\bar{b}}\) at all. This is because the corollary on which the theorem is founded follows from the high-level property of idempotence. Notice too that the theorem is parameterised by the traversal order over \(\mathbf {m}\) and therefore is independent of it.

The in-place version of the incremental strong closure algorithm is presented in Fig. 14.

The following lemma shows that running incremental closure followed by strengthening refines the entries in the DBM to their tightest possible value with respect to the new octagonal constraint.

Now we move onto the theorem showing the correctness of InplaceIncStrongClose. We show that the in-place version of the algorithm produces the same DBM as the non-in place version of the algorithm. A bijective map used in the proof to process key entries first before processing non-key entries: the condition \(\forall 0 \le i< 2n. \rho (i,\bar{\imath }) < 2n\) ensures this property. Note that this is the only caveat on the order produced by the map: the order in which key entries themselves are ordered is irrelevant and similarly for non-key entries.

The in-place version of the incremental tight closure algorithm is presented in Fig. 14, the only difference with incremental strong closure is that for key entries we also run a tightening step (line 3). As in the previous section, we have a helper lemma for the main theorem, showing that incremental closure followed by tightening and strengthening refines the entries in the DBM to the tightest value with respect to the new octagonal constraint.

The following theorem is analogous to the theorem for in-place strong closure (Fig. 15):

The Apron library [17] supports various number systems, such as single precision floating-point numbers and GNU multiple-precision (GMP) rationals. The default number system for the OCaml bindings is rationals, but it must be appreciated that the computational overhead of allocating memory for the rationals dominates the runtime, potentially masking the benefits of IncStrongClose over IncClose. (Recall that IncStrongClose saves a separate pass over the DBM relative to IncClose, avoiding counter increments and integer comparisons.)

In Apron, numbers are represented by a type bound_t, which depending on compile-time options, will select a specific header file containing concrete implementations of operations involving numbers extended to the symbolic values of \(-\,\infty \) and \(+\,\infty \). Every bound_t object has to be initialised via a call to bound_init, which in the case of rationals will invoke malloc and initialise space for the rational number. DBMs are stored taking advantage of the half-matrix nature of octagonal DBMs which follows by the definition of coherence. An array of bound_t objects is then used to represent the half-matrix, as shown in Fig. 16, subfigure (1). If \(i\ge j\) or \(i=\bar{\jmath }\) then the entry at (i, j) in the DBM is stored at index \(j + \lfloor i^2 / 2\rfloor \) in the array. Otherwise (i, j) is stored at the array element reserved for entry \((\bar{\jmath }, \bar{\imath })\). A DBM of size n requires an array of size \(2n(n+1)\) which gives a significant space reduction over a naive representation of size \(4n^2\).

Unexpectedly, initial experiments with Frama-C suggested that much of its runtime was spent in memory management rather than the domain operations themselves. Further investigation using Callgrind showed that 36% of all function calls emanated from malloc-like routines. In response, the underlying DBM data structure was refactored to ensure that this undesirable memory management feature did not artificially perturb the experiments. The refactoring is fully described in a separate work [9], but to keep the paper self-contained the main idea is summarised in the following paragraph.

The DBM representation was changed from a matrix storing numbers to a matrix storing pointers to numbers stored in a cache. This reduces the amount of memory used by a DBM as shown in Fig. 16. The modified data structure has been dubbed a compact DBM or CoDBM for short. The cache is an array initialised to contain \(\infty \) as its first entry, augmented with an ordered table which enables the pointer for any given number to be found (if it exists) in the cache using the bisection search method. As new numbers are created they are added to the cache, and the table is extended in sync. This representation which, crucially, factors out the overhead of storing a number repeatedly, has a significant impact on the memory usage of the Apron library. It also rebalances the proportion of time spend in domain operations. Further performance debugging of Frama-C, for instance to speed up parsing, would only increase the fraction of time spend on the domain operations and closure in particular.

Each micro-benchmark suite was a collection of 10 problems, each problem consisting of a random octagon and a randomly generated octagonal constraint. Each random octagon was generated from a prescribed number of octagonal constraints, so as to always contain the origin, for a given number for variables. Each octagon was then closed. A single randomly generated octagonal constraint, not necessarily containing the origin, was then added to the closed octagon using incremental closure. IncClose and IncStrongClose where then timed and compared against the Apron version for DBMs over rationals. The resulting DBMs were then all checked for equality against Close. All timings were averaged over 10 runs and, moreover, all algorithms were exercised on exactly the same collection of problems. Figure 17 presents timings for the micro-benchmark suites. The results show that IncClose outperforms the original Apron implementation by a factor of 3–4 and IncStrongClose offers an additional 4–9% speedup over IncClose.

The EVA plugin of Frama-C implements an abstract interpreter over the internal intermediate language used by Frama-C. The plugin uses the Apron library to perform an octagon domain analysis, and so by modifying Apron, Frama-C can make direct use of IncClose and IncStrongClose (and specially their IncCloseHoist and IncStrongCloseMotion variants). Table 1 lists the benchmark programs passed to EVA to interpret the programs over the octagon domain. It should be noted that EVA is a prototype (which may explain its memory behaviour) and as such does not use widely used heuristics and optimisations such as variable packing [8, 16] or localisation techniques [5, 25] to enable the analysis to scale. Nonetheless, the octagon analysis successfully terminated over the selected benchmarks.

Figure 18 gives the timings of benchmarks for rational (above) and floating point arithmetic (below), normalised to the time required by the Apron implementation. For rationals, normalised timings are given for both DBMs and CoDBMs. The relative speedup obtained from deploying IncClose and IncStrongClose over Apron algorithm is variable, ranging from a large speedup for taes to a modest slowdown for qlz. Table 2 amplifies the relative timings presented in the bar chart, giving the exact timings in seconds. The table shows that the longest running analyses (which correspond to those employing the largest DBMs) are best served by IncClose and IncStrongClose.

Cachegrind [23] profiling sheds light on qlz: some of the refined incremental algorithms actually increase the number of first-level data cache misses, giving a net slowdown. This cache anomaly might arise because the DBMs generated by qlz are tiny. Cachegrind also suggests this is the exception, revealing that the large speedup on bzip, mod and taes for CoDBMs over DBMs stems from a reduction in the number of misses to level 3 unified data and instruction cache. In fact, for bzip, mod and taes, the number of level 3 cache misses is reduced to zero. This validates the CoDBM data-structure. It also illustrates that optimisations which match the architecture can have surprising impact.

Floating point arithmetic is much faster than rationals, so the proportion of the overall execution time spent in closure is decreased, hence one would expect the relative speedup from IncClose and IncStrongClose over Apron to be likewise reduced. Figure 18 and Table 2 shows that this is the general pattern. CoDBMs timings are not given for floats because floats have a much denser representation than GMP rationals. Nevertheless, the longest running analysis, which arises on taes, significantly benefits from both IncClose and IncStrongClose.

The AbSolute constraint solver [26] applies principles from abstract interpretation to continuous constraint programming. Continuous constraint programming uses interval approximations to approximate solutions to continuous constraints: in essence a solution enclosed by a single interval is successively refined to a set of intervals covering the solution (provided one exists).

The AbSolute solver deploys octagons rather than intervals to obtain a more precise and scalable solver. It uses Apron to implement its abstract domain operations, working over floats rather than rationals. The benchmarks selected to exercise AbSolute are a strict subset of those contained in the AbSolute repository (some problems fail to parse while others contain trigonometric functions not supported by the Apron library).

Figure 19 summaries the relative performance of Apron, IncClose and IncStrongClose; Table 3 gives the exact timings in seconds. All but one benchmarks show an improvement with IncClose and IncStrongClose, even though the size of the DBMs are small compared to those that arise in the Frama-C benchmarks.