Bringing freedom in variable choice when searching counter-examples in floating point programs

2020·Arxiv

Abstract

Abstract

Program verification techniques typically focus on finding counter-examples that violate properties of a program. Constraint programming offers a convenient way to verify programs by modeling their state transformations and specifying searches that seek counter-examples. Floating-point computations present additional challenges for verifica-tion given the semantic subtleties of floating point arithmetic. This paper focuses on search strategies for CSPs using floating point numbers constraint systems and dedicated to program verification. It introduces a new search heuristic based on the global number of occurrences that outperforms state-of-the-art strategies. More importantly, it demonstrates that a new technique that only branches on input variables of the ver-ified program improve performance. It composes with a diversification technique that prevents the selection of the same variable within a fixed horizon further improving performances and reduces disparities between various variable choice heuristics. The result is a robust methodology that can tailor the search strategy according to the sought properties of the counter example.

1 Introduction

Program verification techniques typically focus on finding counter-examples that violate properties of a program. Constraint programming offers a convenient way to verify programs by modeling their state transformations and specifying searches that seek counter-examples. Floating-point computations present additional challenges for verification given the semantic subtleties of floating point arithmetic. In this context, research strategies play a key role in the effectiveness of the search for counter-examples.

Variable choice strategies and, more generally search heuristics, are a key feature in constraint programming. Those often exploit the semantics of the application or the domain to make smart decisions on what to branch on next. Classic examples of such contributions include first-fail [15], dom/deg [4], wdeg [6], IBS [28], ABS [25], Counting [26] and exploit properties of the CSP such as domain size, static, dynamic or failure-weighted degrees, impact of propagation, activity of variables or number of solutions to name just a few.

The bulk of the efforts in this space was devoted almost exclusively to fi-nite domain search strategies. Reasoning over continuous domains with intervals is well studied too. Systems such as Newton [30], Numerica [29], Icos [21] or RealPaver [14] are representative examples where the objective is to offer a conservative outer approximation of the reals. The core of the efforts there is predominantly focused on adapting consistency notions to the continuous domain and providing effective filtering operators. In contrast, little attention has been devoted to CSPs using floating point variables [24,23,27]. Yet, floating point constraint systems are commonly used in the context of program verification where one wishes to model the behavior of the system rather than conservatively approximating the reals. Floating point domains offer unique properties that could be exploited to enhance the search process. In [31], the authors introduce a collection of dedicated search strategies for program verification that effectively exploit such properties. Those heuristics focused on variable selections as well as branching schemes for splitting domains. The paper concluded that absorption and density were particularly effective variable selection heuristics and their adoption moved the state of the art forward. The empirical evaluation in [31] was based on a small set of benchmarks derived directly from C source code of test programs which were manually translated into a system of constraints expressing relationships between states and following Hoare logic [16]. The heuristics included both static and dynamic variants (whose recommendations depend on the current state of the search).

lems and investigates three issues. First, it extends the variable selection heuristics to deliver an alternative that significantly improves upon [31]. Second, it considers a simple static technique called Restrict to focus the search on important variables. The technique is particularly potent given its simplicity and effectiveness. The technique is orthogonal to the variable selection or the splitting strategy. It can, therefore, be composed with any search heuristic. Interestingly, Restrict does significantly reduce the performance gaps that exist between all the proposed heuristics. Finally, the paper amplifies Restrict with a simple dynamic diversification technique for the variable selection that is reminiscent of the diversification methods used within meta-heuristics [12].

This paper includes an evaluation of those techniques over a sizeable and realistic set of benchmarks and demonstrates the value of combining Restrict with diversification. This combination is extremely promising and deliver a simple yet potent technique that significantly outperforms the results in [31] while requiring very little implementation efforts. As a matter of facts, combining Restrict with diversification reduces drastically the gap between the different variable choice strategies and lets the user freely choose the strategy according to other criteria than speed. For instance, the user can select a strategy that promotes solutions in the neighborhood of zero or absorption according to his needs without regard to efficiency issues.

Contributions The contributions of this paper include:

– globalOCC a new search heuristic that outperforms state-of-the-art strategies introduced in [31].

– Restrict a new technique that only branches on input variables of the program to verify.

– Diversify a new technique that prevents the selection of the same variable within a fixed horizon (i.e., within a fixed depth of its last selection).

The paper is organized as follows. Section 2 reviews the properties supporting the variable selection heuristics of [31] and introduces globalOCC. Section 3 outlines the generic search procedure. Section 4 introduces Restrict. Section 5 presents Diversify to further amplify Restrict. Section 6 presents the empirical evaluation. Section 7 discusses related works.

2 Heuristic Properties

Heuristics govern variable selection strategies and order the set of variables according to weights. Two types of heuristics can be distinguished: dynamic and static (or structural) heuristics. Width, cardinality, density and absorption belong to the first family as variable weights evolve along with the search tree. On the other hand, lexicographic, degree, local occurrences and global occurrences compute variable weights once at the beginning of the search tree. Note that floating point representation has a significant impact on the behavior of classical heuristics like width or cardinality. In this section, all property definitions but definition 8 are extracted from [31].

Let the model denote a constraint satisfaction problem (CSP) defined over a set of variables X, a set of domains D (i.e., floating point intervals) and a set of constraints C. Each constraint is a relation defined over a subset of variables from X. Namely, for each represents all the variables occurring in c. Likewise, for each variable ) is the set of constraints in which x appears. Finally, an interval of floating point numbers x = [x, x] = , where F is the set of floating point numbers, represents the domain of variable x.

2.1 Width

Definition 1 (Width). Let w(x) represent the width of x, the domain of variable x from the CSP . Namely, w(x) = in which x (resp. x) is the upper (resp. lower) bound of interval x, i.e., the domain of variable x.

2.2 Cardinality

Definition 2 (Cardinality). Let card(x) represent the cardinality (i.e., the number of floating point values) of variable x. Namely,

where (resp. ) is the exponent of x (resp. x), and (resp. ) is the mantissa of x (resp. x), while p is the length of the mantissa.

Contrary to what occurs with classical domains like integers, w(x) and card(x) capture completely different quantities due to the non-uniform distribution of floating point numbers. For more details refer to [31].

2.3 Density

Definition 3 (Density). Let dens(x) represent the density of the domain of variable x from the CSP . Namely,

Observe how the domains of floating-point numbers are not uniformly distributed, e.g., about half of the floats are in [1]. Informally, dens capture the proximity of floating point in domains. Maximizing dens helps capture variables with huge numbers of values in regards to the size of the domain. Intuitively, those variables may have a larger number of values appearing in solutions.

2.4 Absorption

The semantics of floating point arithmetic can surprise developers with behaviors like absorption which is summarized as follows. When two floating point values a and are added (or subtracted), if is sufficiently small w.r.t. ’s magnitude depends on a), the result of the operation is a and in this case is absorbed by a, i.e., .

Definition 4 (Absorption). Let abs(x) represent the maximum number of floats that can be absorbed from the domain of another variable y appearing jointly with x in a constraint of the form . Namely,

where absorb(x, y) denote the number of floats of y domain’s absorbed by at least a value of x domain’s and defined by

where p is the size of the mantissa (i.e., 23 for single floating point variable and 53 for double), and is the exponent of max(|x|, |x|)

The goal of abs is to identify the variable absorbing the most over the constraints. Absorption is a behavior that often lead a program to invalidate its specification.

2.5 Lexicographic

Definition 5 (lexicographic). Let lex(x) represent the index of the variable x in the lexicographic order of declaration of the variables. Namely, ) = i where i represents the variable declared. Hence, given and two variables with i < j, then has been declared before (i.e, )).

2.6 Degree

Definition 6 (Degree). Let degree(x) denote the degree of a variable x from CSP . Namely, degree(x) is the number of constraints referring to x:

2.7 Local occurrence

Local occurrence focuses on each constraint in isolation based on how often a variable appears within the constraint when given in existential form.

Definition 7 (Local occurrence). Let ) represent the maximum number of occurrences of a variable x in the constraint set C of CSP , i.e.,

where count(x, c) is the number of occurrences of .

For instance, if c is a polynomial, count(x, c) is the sum of the degrees of x in the terms of c. Intuitively, the expression of a constraint can include multiple references to the same variable x. The property ) imputes to variable x the largest number of occurrences among all the constraints in the CSP.

= [10]with

Let us detail the computation of ) and ). Since, cstr(x) = {z = (x + and x appears twice in this constraint, ) = 2. Likewise, cstr(y) = C and y appear once in each constraint. Thus, = [1] and the local occurrence heuristic will favor variable x.

Limitation Fundamentally, the property prefers a variable with more impact within a particular constraint over a variable with impact on the whole problem. For instance, with the set C of Example 2.7, the variable x will be chosen (it occurs twice in the first constraint), even if it belongs to a single constraint. Yet, y occurs three times in the system but only once in each constraint and fixing y leads to a solution by propagation. The situation can be even worse if one ignores the first constraint. In that case, all variables appear at most once in the remaining two constraints and local occurrence will not be able to discriminate.

2.8 Global occurrence

The limitation of can be removed with a revision to the definition that takes into account the occurrences of a variable in the entire CSP.

Definition 8 (Global occurrence). Let ) represent the maximum number of occurrences of a variable x in the CSP . Namely,

where count(x, c) is borrowed from definition 7.

Intuitively, fixing the variable appearing the most in the whole program might have the most impact on the domain size of all other variables.

Example Consider again Example 2.7. The property is therefore [21]. Global occurrence overcomes the Local Impact limitation of local occurrence (i.e., the propensity to favor variables with high local impact over variables affecting constraints throughout the model).

3 Search Heuristic

The adoption of a property f to drive the variable selection heuristic and solve a CSP amounts to choose the variable that maximizes f(x). In other words, given = max), let the subset of candidate variables be

and the branching variable be drawn from ). Whenever 1, the generic strategy breaks ties with a lexicographic ordering that leverages the static order of variable declarations in the model.

All the variable selection strategies in [31] as well the new globalOCC (which implements definition 8 of section 2.8) result from the instantiation of the generic search strategy above with one of the properties given in Section 2.

4 Restriction

Exploiting the semantics of variables, domains and constraints can be quite effective to tackle hard CSPs. Yet, exploiting the semantics of the application domain itself can also prove extremely potent. This section discusses a simple technique that takes advantage of the source program being verified to identify and focus the search on a subset of critical variables for a dramatic impact on performance.

A CSP is derived through an automatic process from a C program P. This derivation process weaves the state changes of the program through constraints connecting the input variables of the function P to the output (returned value) of the program. Clearly, when the program P has inputs I with and outputs , looking for a counter-example that violates the post-condition of P amounts to execute a search procedure based on a strategy S that branches on the variables in X.

Restrict is a simple departure from this classic approach. Fundamentally, Restrict solves M by exclusively branching on the input variables of P, i.e., it only branches on I and not the entire set X. This does not jeopardize the correctness nor the completeness of the approach. Indeed, once the input variables are fixed, all the auxiliary variables get fixed by virtue of propagation alone.

It is worth noting that the implementation is straightforward and completely orthogonal to the search strategy (variable selection and branching heuristics) making it trivial to integrate restrict with any search strategy and evaluate its impact on all the alternatives that are available.

This approach seems quite natural but it is not common in program verifi-cation where most tools are based upon SMT solvers. The point is there is no notion of input variables in the SMT format even if, in the case of problems on floats, the input variables can be identified.

Formalization The derivation of is a compilation of the sequence of instructions appearing in program P. First, consider a single instruction.

Example 1 (State Derivation). Consider a 3-operand instruction of the form x = in which is a binary operator and the set of variables representing the state of the program at the start of line 2 includes , i.e.,

The assignment on line 2 introduces a fresh variable and a constraint to represent the state transformation in which is the variable holding the current state of the symbolic variable x after the instruction.

The derivation can be generalized to all instructions and applied on entire blocks of code to yield a CSP in which T contains all the temporary variables modeling the state evolution (and their domains) and C is the set of constraints connecting all the states.

Definition 9 (Verification CSP). A C function is subject to a pre-condition Pre(I) and must satisfy a post-condition Post(O). In Hoare’s terms

captures the expectations on P. Given the CSP derived from the body of P, the CSP

has a solution if and only if there exist an assignment of values to the variables in I that delivers an output O that violates the post-condition, namely, such a is a counter-example. Similarly, if F has no solution, no such counter-example exists.

Traditionally, one would solve the CSP F in search of a solution (a counter-example) and this is exactly what [31] does. Namely, it applies a branching strategy S to all the variables of F

in which solve refers to the resolution of the CSP using a search procedure based on the branching strategy S applied to the variables in F, i.e., in vars(F). Restrict is a simple departure from this classic approach. It considers the resolution of F by exclusively branching on variables from I. More formally,

Definition 10 (Restrict). Let F be the verification CSP for a program P whose inputs is I (recall that )). Restrict(F) only considers variables from I in its search procedure, namely

5 Diversiﬁcation

Diversification techniques come from meta-heuristics. A classic example is Tabu search [12] which insists on preventing the repetition of local moves that undo recent changes and induce cyclic behaviors where the same computation state is visited repeatedly. Tabu is a diversification mechanism that insists on shifting the focus to moves involving other variables, thereby driving the search in a different part of the search space. In that context, diversification is often considered in an alternating pattern alongside intensification to sample the search space more extensively and sometimes focus on areas of interest.

The idea has rarely been considered in the context of a complete search tree. Note that, there is no risk to “cycle” and revisit the same configuration in a tree search and completeness guarantees that the whole space will be inspected, explicitly or implicitly. Yet, when considering floating-point variables, the idea has a natural appeal. Consider a variable with a large domain and a simple bisection heuristic for branching. If the variable selection heuristic finds the variable appealing (e.g., because of its occurrence counter), the search may become obstinate and repeatedly branch on the variable. Since the domain density is not uniform, such obstinacy may very well lead the search to a great depth before switching to another variable. It may, therefore, be desirable to forbid the selection of this variable in the near future if it was already branched

on recently.

More formally, each time a variable x is selected for branching at some tree node n (at depth depth(n)), the search records a prohibition depth for x equal

where u sets a desired depth of search for which the variable is prohibited.

Intuitively, the search is prohibited to consider x again until the depth exceeds last(x). When the search considers a tree node n (at depth depth(n)), the selection heuristic, rather than inspecting any (free) variable in X, may instead choose to consider

where bound(y) is true if variable y is bounded.

Clearly, as the value of the parameter u increases, variables stay in “purgatory” increasingly longer after being selected. With u = 0, this strategy simply reduces to normal branching and one must always have to operate normally. Note that, as the search backtracks, the prohibition depths must be restored. Finally, observe how the heuristic S is applied to the non-prohibited variables to yield a branching recommendation.

6 Experiments

This section evaluates globalOCC, Restrict and Diversify on a significant set of benchmarks and discusses their impacts and interplay.

Benchmarks The following experiments consider 151 benchmarks with 84 benchmarks with solutions (SAT), and 67 without solution (UNSAT). Those extend significantly [31] and originate from standard program verification’s sources. More precisely, benchmarks include C code from section 6.3 of [9] (i.e., main contribution of FP Bench), and benchmarks from SMTLIB [3] where the C code is available. Specifically, they include:

– All the benchmarks described in [31].

– LeadLag, PID, Odometrie, Runge Kutta (second and fourth order) and Trapeze programs are all coming from [9]. Two versions of these programs are available: a classic and an optimized one with a reduced amount of numerical error. The benchmarks compare the difference between the classic and optimized programs and try to find input values where the square of the difference is bigger or equal to a given delta. Different benchmarks are obtained by unfolding the inner loop from 1 to 200 times.

– Other benchmarks are from the SMTLIB [3], namely add*, div*, mul*, e1 *, e2 *, newton*, sine*, square *. The benchmarks from the SMTLIB are restricted to the one with available C source.

Overall, these benchmarks have up to 2813 variables and up to 2813 constraints. With respect to variables, 40 benchmarks have between 10..100 variables, 26 benchmarks have 100..1000 variables, and 3 of them have in excess of a 1000 variables. The cardinality of the restricted set of variables reaches up to 51 variables. As a matter of fact, Restrict reduces the set of variables taken into account by the search by more than 90% for 43 benchmarks, by 50% up to 90% for 77 benchmarks and, by less than 50% for 31 benchmarks. Note that 2 benchmarks do not benefit from Restrict.

All the experiments were made on a Macbook Pro with 2.9GHz 6-core Intel Core i9 and 32GB with a timeout of one minute. Note that all experiments have been done using the split 5 way strategy described in [31].

Raw Results Tables 1 reports, for each strategy from [31] (in light gray) as well as for the new strategy globalOCC, the number of timeouts as well as the total runtime for instances that are satisfiable (SAT), unsatisfiable (UNSAT) or both (ALL). The timeout is set to 60 seconds. The four sections of the table report the results for:

Baseline the implementation in [31]. Namely, the results in the section Baseline for each strategy are from [31] evaluated on the extended benchmark collection proposed here.

Restrict the Baseline augmented with the static restriction technique only. Diversify the Baseline augmented with the dynamic diversification technique only (with u = 2).

Restrict+Diversify the Baseline augmented with both the static restriction and the dynamic diversification techniques.

Column globalOCC reports the result for the new strategy. The last column of the table conveys the standard deviation of the time ()) across the population of all strategies (i.e., 8 strategies) as well as the mean time ()).

Impact & Discussion (globalOCC) The Baseline section of table 1 highlights the benefit of globalOCC over other strategies when used with the default configuration. It improves the solving of the satisfiable benchmarks, i.e., the benchmarks which are the most sensitive to the search strategies, by a factor from 4.39 up to 24.95 depending on the variable choice heuristic while keeping ahead of unsatisfiable benchmark solving.

globalOCC better anticipates the impact of a given variable on the CSP. Contrary to other structural heuristics like degree or local occurrences that consider the local role of a variable, it weighs a variable according to its global effect on the CSP. As structural heuristics performs better than dynamic heuristics, globalOCC dominates all other heuristics.

Impact & Discussion ( Restrict) Restrict has a dramatic impact on performance. It reduces the number of instances that suffer timeouts and it cuts back on the runtime of the others significantly. While I, the subset of input variables, is contained in X, the full set of variables, I can remain sizeable. Indeed, functions whose inputs are arrays of floating points yield large numbers of input

Table 1. Full comparison

variables as there is one input variable for each entry of the array. Naturally, if |I| = 1, the problem derived from P is uninteresting from a search prospective since there is no choice to make for which variable to branch on.

Restrict delivers a second surprise as the performance gaps that exist between various heuristics when using a search on X shrink dramatically as one adopts Restrict. The gains are so significant that they erase almost entirely the advantage that the best heuristics have when considering the full set of variables X. Table 1 provides the necessary evidence. The number of timeouts from Baseline drops dramatically when Restrict is used. In aggregate (across all heuristics), Baseline delivers 244 timeouts while Restrict produces only 51. The drop in running times is equally impressive and improves for all heuristics bringing Baseline’s range of 553.79..4275.86 seconds down to 386.55..572.67 seconds. The “gap” between heuristics captured by the standard deviation across the heuristic population drops accordingly from 1323.6 seconds down to 83.5 seconds.

A natural question that arises is Why is Restrict so effective? Two situations are worth considering: satisfiable and unsatisfiable instances. Recall that satisfiable instances produce a counter-example that violates the program spec-ification. Yet, all the “internal” variables (temporaries) are functionally dependent on the input variables. As soon as the inputs are fixed, all the internal state is fixed. Focusing on the inputs is going to quickly reduce the size of the

Fig. 1. Comparison of features over all benchmarks

search space. While branching on outputs might sound attractive, the lack of may prevent any form of informed guidance.

Unsatisfiable instances may, on the contrary, look credible until one realizes that the values leading to the counter-examples are not allowable w.r.t. the pre-conditions of the program. As a result, branching on “internal” variables is liable to cause the exploration of a very large tree in which candidate solutions are ultimately rejected when the pre-condition on the inputs are finally considered.

Impact & Discussion ( Diversify) Diversify is quite simple to implement requiring minimal changes to the search. It is effectively orthogonal to the selection strategy S. As Figure 1 demonstrates, Diversify improves Baseline as well as Restrict. Yet, Diversify serves as an amplification to Restrict. Indeed, Restrict’s job is to prohibit the selection of temporaries for branching while Diversify prohibits excessive focus on the same variables during the search. Combined, they narrow the performance gaps between different heuristics, reduce the number of timeouts even further, and lower the gaps between search heuristics significantly. For instance, maxCard drops from 3764.49 seconds to 387.55 seconds. Even globalOCC benefits from this combination.

Consider the code example shown in Figure 2. Lines 2-3 of function f specify pre-conditions, and lines 7-11 corresponds to post-condition checks. Recall that the derivation builds a CSP M where post-conditions are negated. A correct solution of this program is a pair of values , both in [0] that leads the execution either to the else block (lines 9-10) or to the if block (lines 7-8) without triggering the assertion. A counter example would lead the code execution to the if block and trigger the assertion. Few counter examples exist for this program.

Fig. 2. Example of code where Diversify improves the search of a counter-example.

in a reasonable time (i.e., before the timeout). Both Diversify and Diversify +Restrict find a solution quickly. The latter explore 10 times fewer nodes than Diversify alone. On this program, Diversify refutes sub-trees substantially faster. More precisely, Diversify helps to prune branches that corresponds to 0 in 44 nodes. Whereas Restrict still struggle on the same part after almost 2 million nodes. Even the addition of 0 to the model is not enough to get Restrict or Baseline to compete.

Here, both searches first branch on variable x with D(x) = [L..U] and Mid =

branching constraints such as x = L, x = Mid and x = U and all are easily proved as finitely failed. However, when imposing , the two search heuristics exhibit different behaviors. Restrict (shown in black) favors repeatedly branching on x (because of a high value density) and dives in a large sub-tree before reaching a point where another variable y has a better density and gets branched on. Shortly after, the propagation discovers the infeasibility and backtracks. This process leads to a large refutation proof that consumes the entire runtime. In contrast, Restrict+Diversify is forced to skip over the most attractive variable (x) and instead favor a second best variable y. This alternation between x and y may repeat, but leads to sub-domains for x and y of comparable sizes for which the inconsistency is discovered at a much shallower depth. Because the height of the red tree is much smaller than , the refutation completes quickly and the search finally explores the last sub-tree where the solution lies. Benchmarks were Diversify helps often exhibit this class of behavior which suggest that further work is warranted to automatically determine a suitable value for the “tabu” parameter.

Hardness The benchmarks considered for those experiments are realistic. For instance, with Baseline, the average of total fails for each strategy exceeds 39 millions. The combination of Restrict with Diversify reduce the size of the explored search tree, yet, the search remains challenging with an average of total fails for all strategies exceeding 7.8 millions.

Summary Two key results emerge from the empirical evaluation. First, the new heuristic globalOCC outperforms the state of the art from [31]. As Table 1

Fig. 3. Restrict vs. Restrict+Diversify search trees on benchmark f23.

demonstrates, its performance exceeds all other heuristics by a significant margin, being at least 56% faster and up to 772% faster with the lowest number of timeouts. Second, both Restrict and Diversify have a significant impact on performance. In particular, Restrict speeds up all the heuristics. Both are simple to implement, carry no overhead and are orthogonal to the search heuristic. Nonetheless, the techniques are effective and Figure 1 leaves no doubt about their value. Indeed, even the worst strategy becomes competitive when Restrict and Diversify are leveraged.

7 Related works

Variable selection strategies have received much attention in finite and in continuous CSPs. Most of the strategies mentioned in the introduction are dedicated to finite domains where small sized domains are the norm. Yet, in program verification and floating point problems in particular, one must handle huge domains. For continuous domains, the most common variable selection strategy is the Largest First (LF) strategy [18,8,13]. It consists in selecting the variable with the domain of maximal width. More sophisticated approaches [13,1] rely on the Maximal Smear (MS) strategy introduced by [19,20]. Informally, the Maximal smear select the variable the projection of which has the strongest slope. While continuous domains are often large, the most interesting techniques rely on mathematical properties that do not hold in floating point arithmetic.

In contrast, search heuristics exposed in this paper exploit either of the float-ing point peculiarities (like density or absorption) or program verification features (like the Restrict set).

Floating point constraint solvers have been developed to address verification problems of programs with floating point computations [24,5]. Available floating point solvers can be divided into two categories: constraint solvers and SMT solvers. Our approach belongs to the first family of solvers as Colibri [22] does. Both solvers rely mainly on interval computations adapted to floating point arithmetic to preserve the set of solutions [23,5]. A coarse evaluationof both solvers showed that Colibri is, on average, twenty percent slower than our solver in the Baseline configuration.

SMT solvers like MathSat [7], Z3 [11] and CVC4 [2] are now able to handle floating point problems thanks to the QF FP theory. They are organized around a DPLL [10] procedure which send the floating point subproblem to a dedicated solver. SMT solvers are often built on top of SAT solvers and handle floating point arithmetic by means of bit blasting. As a result, Colibri outperforms these solvers on QF FP benchmarks. SMT solvers depend on the SMT language [3] to describe the problem. Unfortunately, this language does not permit to distinguish input and auxiliary variables.

8 Conclusion

This paper consideres floating point CSPs and offers two contributions. First, it introduces a new search heuristic that considers a global occurrence property that substantially improves the state of the art results in this domain. Second, it defines two techniques that affect the search strategies yet remain orthogonal to the variable selection or the domain splitting and are therefore composable with any heuristic. Restrict focuses the search on the subset of variables that appear in the input of the program under verification. It delivers a significant performance boost both in runtime and a dramatic reduction in the number of instances that timeout regardless of the heuristic being employed. Diversify is inspired by meta-heuristics and prevents the selection of a variable (for branching) if it has been recently branched on. The diversification amplifies the gains of Restrict with whom it composes easily. The combination of both Restrict and Diversify reduces the differences of efficiency between search strategies to almost nothing and thus, brings to the user the freedom of choosing search strategies according to other criteria. Experiments on a significant set of benchmarks are very promising.

References

1. Ignacio Araya and Bertrand Neveu. lsmear: a variable selection strategy for interval branch and bound solvers. J. Global Optimization, 71(3):483–500, 2018.

2. Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovi´c, Tim King, Andrew Reynolds, and Cesare Tinelli. CVC4. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Proceedings of the 23rd International

On the sizeable subset of identical benchmarks available for both Colibri and our

SMTCOMP 2019 (note that par4 is a portfolio of solvers) or http: //smtcomp.sourceforge.net/2018/results-QF_FP.shtml?v=1531410683 for SMTCOMP 2018.

Conference on Computer Aided Verification (CAV ’11), volume 6806 of Lecture Notes in Computer Science, pages 171–177. Springer, July 2011. Snowbird, Utah.

3. Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The SMT-LIB Standard: Ver- sion 2.6. Technical report, Department of Computer Science, The University of Iowa, 2017. Available at www.SMT-LIB.org.

4. Christian Bessi`ere and Jean Charles R´egin. MAC and combined heuristics: Two reasons to forsake FC (and CBJ?) on hard problems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 1996.

5. Bernard Botella, Arnaud Gotlieb, and Claude Michel. Symbolic execution of floating-point computations. Software Testing, Verification and Reliability, 16(2):97–121, 2006.

6. Fr´ed´eric Boussemart, Fred Hemery, Christophe Lecoutre, and Lakhdar Sais. Boost- ing systematic search by weighting constraints. Frontiers in Artificial Intelligence and Applications, 110:146–150, 2004.

7. Alessandro Cimatti, Alberto Griggio, Bastiaan Schaafsma, and Roberto Sebas- tiani. The MathSAT5 SMT Solver. In Nir Piterman and Scott Smolka, editors, Proceedings of TACAS, volume 7795 of LNCS. Springer, 2013.

8. T. Csendes and D. Ratz. Subdivision direction selection in interval methods for global optimization. SIAM J. Numer. Anal., 34(3):922–938, June 1997.

9. Nasrine Damouche. Improving the Numerical Accuracy of Floating-Point Programs with Automatic Code Transformation. PhD thesis, Perpignan, 2016.

10. Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving. Commun. ACM, 5(7), July 1962.

11. Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient smt solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’08/ETAPS’08, pages 337–340, Berlin, Heidelberg, 2008. Springer-Verlag.

12. Fred Glover. Tabu search-part I & II. ORSA Journal on computing, 1(3):190–206, 1989.

13. Laurent Granvilliers. Adaptive bisection of numerical csps. In Michela Milano, editor, Principles and Practice of Constraint Programming, pages 290–298, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg.

14. Laurent Granvilliers and Fr´ed´eric Benhamou. Algorithm 852: RealPaver: An in- terval solver using constraint satisfaction techniques. ACM Transactions on Mathematical Software, 2006.

15. Robert M. Haralick and Gordon L. Elliott. Increasing tree search efficiency for constraint satisfaction problems. Artificial Intelligence, 1980.

16. C. A.R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–580, 1969.

17. Narendra Jussien and Olivier Lhomme. The path repair algorithm. Electronic Notes in Discrete Mathematics, 4:2 – 16, 2000.

18. R. Baker Kearfott. Some tests of generalized bisection. ACM Trans. Math. Softw., 13(3):197–220, September 1987.

19. R. Baker Kearfott. Rigorous global search: continuous problems, volume 13. Kluwer Academic Publishers, Dordrecht, The Netherlands, 1996.

20. R. Baker Kearfott and Manuel Novoa III. Algorithm 681: INTBIS, a portable interval Newton/bisection package. ACM Transactions on Mathematical Software (TOMS), 16(2):152–157, June 1990.

21. Yahia Lebbah, Claude Michel, Michel Rueher, David Daney, and Jean-Pierre Mer- let. Efficient and safe global constraints for handling numerical constraint systems. SIAM Journal on Numerical Analysis, 42(5):2076–2097, 2005.

22. Bruno Marre, Fran¸cois Bobot, and Zakaria Chihani. Real Behavior of Floating Point Numbers. In The SMT Workshop, Heidelberg, Germany, July 2017. SMT 2017, 15th International Workshop on Satisfiability Modulo Theories.

23. Claude Michel. Exact projection functions for floating point number constraints. In AI&M 1-2002, Seventh international symposium on Artificial Intelligence and Mathematics (7th ISAIM), Fort Lauderdale, Floride (US), 2–4th January 2002.

24. Claude Michel, Michel Rueher, and Yahia Lebbah. Solving constraints over floating-point numbers. In Proceedings of the 7th International Conference on , LNCS 2239, pages 524–538, Paphos, Chypre, 26-1st November 2001.

25. Laurent Michel and Pascal Van Hentenryck. Activity-based search for black-box constraint programming solvers. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2012.

26. Gilles Pesant. Counting-Based Search for Constraint Optimization Problems. In 30th AAAI Conference on Artificial Intelligence, AAAI 2016, 2016.

27. Olivier Ponsini, Claude Michel, and Michel Rueher. Verifying floating-point pro- grams with constraint programming and abstract interpretation techniques. Automated Software Engineering, 23(2):191–217, June 2016.

28. Philippe Refalo. Impact-based search strategies for constraint programming. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 3258:557–571, 2004.

29. Pascal Van Hentenryck. Numerica: A modeling language for global optimization. In IJCAI International Joint Conference on Artificial Intelligence, 1997.

30. Pascal Van Hentenryck, Laurent Michel, and Fr´ed´eric Benhamou. Newton: Con- straint programming over nonlinear constraints. Science of Computer Programming, 1998.

31. Heytem Zitoun, Claude Michel, Michel Rueher, and Laurent Michel. Search strate- gies for floating point constraint systems. In Principles and Practice of Constraint Programming - 23rd International Conference, CP 2017, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, pages 707–722, 2017.