Embedded systems, and IoT devices in general, produce, analyze and consume significant volumes of data from arrays of sensors to carry out various control functions. Anti-lock breaking systems (ABS) offer a classic example of an embedded system that senses breaking actuation signals and wheel blockage to dynamically adapt the pressure on pads and prevent wheels from locking up and causing skidding. It is a cornerstone in modern automotive and the correctness of the control algorithm is paramount to the safety of vehicles. Such control systems play critical roles in sensitive devices in domains such as aerospace, transportation, health or even energy. Interestingly, the signals fed to the controllers are often represented as floating point numbers that are used in key calculations to decide how to actuate the device. It is common knowledge that programmers often assume that floating point semantics (even IEEE 754 [16]) are so similar to real numbers that one can use the former while assuming the semantics of the latter. It is, unfortunately, not the case and examples abound of erroneous controllers that caused significant losses [11,26].

Program verification is undoubtedly a natural response to verify the correctness of controllers and ensure that calculations carried out over floating point values do not induce undesirable behaviors. Bounded model checking (BMC) (e.g., [7]) was successfully used with a constraint programming framework to verify programs that used integer computations. Extending BMC to account for floating point is still a challenging problem.

Satisfiability-Modulo-Theory (SMT) solvers are a natural extension of SAT solvers and are applied with success to the verification of floating point programs. Solvers such as Z3 [9], MathSAT [6], CVC4 [1] and SONOLAR [19] are leading examples in this space. Fundamentally, SMT solvers decompose their task by delegating to specific theories (e.g., arithmetic, arrays, bit vectors, float-ing point,...) the task to reason about combinatorial or otherwise complex constraints for which the SAT encoding would be cumbersome or ineffective. The logical core of the problem remains in clausal form and is entrusted with a SAT solver that orchestrates the entire resolution. The resolution proceeds by doing inference and branching in the SAT solver (and the theory solvers) until a contradiction is detected. Upon reaching a contradiction, the responsible theory is tasked with producing a clause that precludes the repetition of decisions that yield the same contradiction. It is essential to realize that SMT solvers entrust the search responsibility entirely to the SAT solver and limit the responsibilities of the theories to produce inferences and learn clausal cuts. Some SMT solver may choose to “ bit blast” some (or all) constraints to encode them in clausal form as well. It is undeniable that this decomposition and encoding processes lead to the obfuscation of the high-level constraints and a loss of information on the structure of the combinatorial model. It is also clear that decomposition and encoding can cause the proliferation of a large number of elementary constraints on the bit level structures rather than the high-level representations. Such issues are critical when it comes to solving floating point verification problems that emphasize the use of complex nonlinear expressions.

Constraint Programming is an area of Artificial Intelligence with successes in a number of areas within combinatorial optimization. It is a de facto leading technology for scheduling and planning where commercial tools such as (Ilog [18],CHIP [10],...) are market leaders. Constraint Programming owes its successes to its ability to leverage strong inference capabilities within a flexi-ble and programmable search framework. Search procedures dedicated to finite-domain CP solvers include weighted degree [2], Impact-based search [28], Activitybased search [23] or counting search [27] to name just a few. All those exploit the

semantics of the application or the domain to make smart branching decisions. While distinctively different, floating point domains also offer unique properties that are exploitable to enhance the search process. Density [32], for instance, features a concentration of values that is not constant along the unit line and can be an indicator to focus (or not) on a variable. The promises of Constraint Programming are based on three prongs: First, semantic structures are preserved, exposed in the model, and exploitable by both the propagation engine and the search procedure. Second, propagation algorithms tailored to specific structures offer stronger filtering and faster inferences. Third, flexible search procedures can exploit the semantics of variables and the constraint network to prune doomed sub-trees and better branch on variables.

The crux of this paper is the composition of two key techniques to expose and exploit semantic structures. First, a symbolic phase is charged with rewriting each SMTLIBinstance to expose elementary constraints for which dedicated propagators exists. It also contributes to the elimination of auxiliary variables whose presence can negatively impact the search process. Second, a diversifi-cation technique within the search procedure steers it away from costly enumerations in unproductive areas of the search space. The empirical evaluation demonstrates that a Constraint Programming Solver is competitive on computationally challenging floating point benchmarks that induce significant search efforts even for other CP solvers. It highlights that the ability to harness both inference and search is critical. Indeed, ObjCP-FP yields a factor 3 improvement over Colibri [20] (another CP solver) which uses a simple search procedure and is up to 10 times faster than SMT solvers. The evaluation was conducted over 214 benchmarks (The Griggio suite) which is a standard within SMTLIB.

Contributions This paper offers a novel constraint programming approach to solve floating point verification problems expressed with the SMT language of SMTLIB with the express purpose of exposing and exploiting structures. The implementation is compared to several state-of-the-art tools including the SMT solvers Z3, MathSAT, CVC4 and SONOLAR. It is also compared to Colibri, a CP solver with a strong inference engine designed specifically for floating point verification.

The paper is organized as follows. Section 2 briefly recalls the foundation of constraint programming and specific details relevant in the context of floating point program verification. Section 3 briefly recalls the state of the art in this space and positions CP technologies w.r.t. SMT solving. Section 4 discusses the symbolic reformulation techniques used to improve the encoding obtained from the SMTLIB specification and reveal substructures present in the model whose semantics can be exploited within the propagation engine. Section 5 reviews the heuristics (variable selection and domain splitting) as well as a key diversifica-tion strategy with a dramatic impact on performance. Section 6 discusses the empirical evaluation and section 7 concludes the paper.

Constraint programming derives its strength from the adoption of the mantra

Indeed, CP solvers feature a declarative model dedicated to the specification of decision variables and the model constraints with a rich language featuring logical, arithmetic and combinatorial constraints. Unlike SAT [13] (or even MIP [25]) it is not limited to Boolean clauses or linear inequalities. Each constraint present in the model is supported by a dedicated filtering algorithm that exploits the semantics of the constraint to achieve strong filtering results with high efficiency. CP solvers also feature a powerful search component that is often used to author sophisticated search procedures that exploit specificities of the problem that are delicate to express in the model. While generic reusable searches exist, e.g., [28,23,2,27], examples of domain specific searches are commonplace, e.g., [29].

This section briefly reviews a few core concepts and their instantiation in the context of floating-point program verification.

Definition 1 (Constraint Satisfaction Problem or CSP). A CSP is a triplet where X is a set of decision variables, D is the Cartesian product of their domains, and C is a set of constraints defined over subsets of X. The domain of a decision variable x is denoted by D(x). Note that D = ) when .

Definition 2 (Floating-Point Domain). A domain = [] denotes the set of floating points with and where F is the set of floating point values.

Definition 3 (Decision Variable). A decision variable is associated to a domain D denoted and it is instantiated if and only if = 1.

Definition 4 (Constraint). A constraint of arity n is a relation defined over a subset of n variables from X called its scope and denoted by vars(c) (namely, |vars(c)| = n).

Given a CSP , the task of a constraint solver is to find a domain that delivers an instantiation of all variables. To do so, the solver engages in a search that alternates branching (by splitting the domain of a variable) with propagation to infer all the domain reductions that logically follow from the branching. Formally, at each node of such a search tree, the solver creates 2 or more sub-problems with the addition of branching constraints and establishes 2B-consistency [15] within each sub-problem. A satisfiable CSP yields a domain in which every variable is instantiated in . An unsatisfiable CSP yields a refutation of the existence of an instantiated domain satisfying all constraints .

Achieving 2B-consistency for a fixed constraint c can be done with a dedicated algorithm that exploits the semantics of c. For instance, an elementary constraint such as with vars(c) = {x, y, z} uses projection functions to compute new domains and . Constraint programming solvers usually offer a rich collection of elementary constraints to express arithmetic relationships. It is essential to preserve such relationships when deriving a CSP from the program to be verified. Indeed, the introduction of auxiliary variables and the repetition of shared structure can weaken the strength of the propagation leading to the production of 2B-consistent domains that are bigger than strictly necessary.

Adaptation of these principles to floating point arithmetic has its roots in the work of [21] who introduced dedicated floating point projection functions.

Satisfiability Modulo Theories (SMT). SMT solvers are widely used in program verification. They had great success especially in bounded model checking of integer programs. SMT solvers can be seen as an extension of SAT solvers to decision procedures. Indeed, modern SAT solvers are very efficient thanks to conflict clause learning.

Brillout et al [5] introduced a bit blasting procedure to handle floating point verification problems in CBMC. It consists in modeling each floating point operation as a formula in propositional logic. The size of the formula is proportional to the number of operators and the width of the floating point type. Well-known SMT solvers like Z3 [31], MathSAT [3] and CVC4 [4] followed suit, and included the same bit blasting techniques.

Yet, a direct application of the bit blasting procedure often leads to an explosion of the resulting formula size as a function of the number of float-ing operations and the size of the operand type. To circumvent this problem, CBMC [5] uses relaxations of the initial problem by means of under and overapproximations of each floating point operations. It generates a smaller propositional formula that may or may not be sufficient to solve the problem. As a consequence, many iterations with increasing precision and complexity might be required to determine the problem satisfiability.

As an alternative to bit blasting, MathSAT [3] also offers an interval propagation solver for floating point problems. It relies on the abstract CDCL framework to allow conflict learning from the interval solver. Like our solver, it depends on a search strategy for the sake of completeness. However, the search strategy is quite simple: it chooses variables in a round-robin order (lexical order) and splits the variable domain in two sub-intervals of the same cardinality. Roughly speaking, this approach can be seen as a tight integration of a classical floating point constraint solver in a sat solver with the benefit of clause learning thanks the abstract CDCL framework.

Floating point constraint solvers. Floating point constraints introduced in [22] filter the domains of variables through interval arithmetic alone. FPCS (Floating Point Constraint Solver) [21] improved the capability to handle floating point constraints by means of dedicated projection functions that conform to floating point arithmetic. Colibri [20] relies on the same principles to solve floating point CSP. However, it introduced distance constraints that strengthen the variable domain reduction. The 2017 version of the ObjCP-FP solver [32] retained the projection functions of FPCS to enhance the underlying solver [30,24] with float-ing point constraints. This 2017 version also focused on search strategies to solve floating point constraint problems.

Contrasting CP and SMT. CP offers a high level of flexibility as well as abstractions to efficiently solve floating point verification problems. CP searches are mainly based on variable domain exploration as opposed to the clause valuation strategies found in SMT solvers. Critically, decisions found in floating point problems are based on heavier and more complex (non-linear) computations than what can be found in other programs. A CP solver incrementally explores paths and decisions that determine a path with a higher and more precise knowledge of the computation states involved in these decisions. It thus has the potential to explore fewer paths to verify the program.

The path enumeration process found in SMT solvers build each path without having any information on the computations that affect the decisions involved along the path. Though clause learning prunes the path enumeration by avoiding exploration of paths involving learned conflict, it does so at the expense of enumerating infeasible paths to identify these conflicts. This requires solving condition affected by heavy computations and possibly, solving the same heavy computations repeatedly as they may lead to different paths. The cost of such solving increases with the bit-blasting procedures used in solvers like Z3, CVC4 or MathSAT that produce propositional formula whose size grows with the number of operations and the precision. Even the MathSAT+ACDCL SMT solver, that combines a floating point interval solver with a SAT solver, is affected by this architecture.

A CP solver with an effective search strategy avoids the enumeration of many impractical paths as it maintains knowledge on all the computations and conditions that lead to the sub-tree of paths left to explore. Doing so, it avoids repeatedly solving costly subset of expensive constraints.

The SMTLIB language enables the specification of models in a solver neutral format. While the language is loosely based on LISP and allows for the spec-ification of models that use multiple SMT theories, this paper focuses on the QF FP theory (Quantifier-Free Floating Point Theory). To illustrate, consider the C program computing a single step of the Newton method in Figure 1.

This simple program can be encoded as an SMTLIB text file (Figure 2) that captures the sequence of low-level instructions visible in an SSA-style representation of the program. Such a translation can be done by a model checker like

ESBMC [12]. For instance, lines 5 and 6 declare and as two decision variables equal to the C variables x and r at the initial state. Line 7 computes (i.e., ) using nearest rounding mode () and stores it in . Line 8 stores the constant 2 (expressed as a bit sequence) into while line 9 computes and stores it into before stating that and adding the constant 1 held in to deliver in the result of the function fp in the C code. Note how line 22 using a reified constraints to state = (== ) before forcing to be true on line 24.

It is immediately apparent that the SMTLIB encoding decomposes every statement in the program with many auxiliary variables which may adversely impact intelligent search strategies that target the variables in the original C program. Specifically and as an example, the sin2.c.2 benchmark yields a constraint graph in Figure 3 with 152 nodes (decision variables) and 242 edges to convey the connectivity between variables.

Fig. 3. Constraints graph of sin2.c.2 for the default model (152 nodes and 242 edges)

Fig. 4. Constraints graph of sin2.c.2 after CSE (82 nodes and 147 edges)

The purpose of this section is to outline the symbolic reconstruction that simplifies this graph while preserving its semantics and exposing key structures to enable the propagation engine of a CP solver to exploit those structures. On the same sin2.c.2 benchmark, the reconstruction yields a graph that is half the size of the original with only 82 nodes and 147 edges (see figure 4). Specifically, the section details the architecture of the reconstruction, its two phases and the impact it has on the filtering capabilities of the solver.

4.1 Architecture

The purpose of the reconstruction is to first recover an abstract model as close as possible to the original C formulation while starting from the SMTLIB encoding. Once an abstract model is available, it is easy to extract the set of decision variables appearing in the abstract model, and then to concretize it down so

Fig. 5. Reconstructed abstract model for Newton-1.1 via R

that it only uses elementary constraints. This final concrete model is the basis for the resolution and the search procedure focuses on the variables identified in the abstract model.

More formally, given a model , a reconstruction function R and a concretization function C, the objective is to reconstruct ) to extract its decision variables and then concretize into ) to be solved by branching on ’s variables using ’s heuristic. Formally,

4.2 Reconstruction with R

The reconstruction uses two steps that start from an initial model . Those steps are identification and inlining.

Identification Partition the constraints in into two disjoint sets and is the set of constraints defining auxiliary variables (i.e., constraints of the form in which is an arbitrary expression and x a variable) and is the remaining set of constraints.

Definition 5 (Auxiliary Variables). Given a constraint , let def(c) = {x} denote the set of auxiliary variables defined by c.

Without loss of generality, let

represents the lifted version of def over a set of constraints.

Inlining Each constraint is rewritten by simply replacing all occurrences of auxiliary variables in ) by their definitions. This substitution process S is applied until no further expansions can occur and the constraint is irreducible under S. Namely, it is the transitive closure of S. The final model drops all the auxiliary variables and their defining constraints and delivers CSP :

in which conveys domains for the variables in ). Clearly the inlining process shrinks the set of variables under consideration and eliminates all the constraints related to auxiliaries. This is the primary driver behind the reduction in model size. On the newton-1.1 example, it eliminates all but two variables (x and r) and leaves only the single constraintshown in Figure 5.

4.3 Concretization with C

This phase leans on three steps and works from the model produced by ).

Factorization The first step factors out common sub-expressions and equates each one with a fresh variable injected where the common sub-expression used to be. The composition of reconstruction and compilation can eliminate variables and simple equality constraints appearing in the SMT model such as and in Figure 2.

Decomposition Decompose each into elementary constraints. The resulting model of this step is , where variables since contains all of ’s variables plus new auxiliaries produced by the factorization.

Inequalities Cycles Occasionally, the C source induces cycles of contradictory inequalities that make the model UNSAT. Common contradictions are of the form: . The pattern typically appear when a program has multiple conditional structure. While the solver can handle such cycles numerically, this typically causes a slow convergence of the fixpoint algorithm executing at each search node. It is far better to recognize such a cycle symbolically and report the UNSAT answer without further to do.

4.4 Impact of C(R(M0))

introduces one auxiliary variable for each factor in the product, namely, two variables a and b and the constraint set:

Yet, the common sub-expression elimination introduces a single variable a = x+y and a resulting decomposition:

that a CP solver exploits since is a square constraint for which a stronger filtering exists. These subtle effects on the inference capabilities of the solver are not negligible. Indeed, stronger filtering is valuable in its own right, but it also helps heuristics such as the variable selection discussed in the next section to differentiate between variables and make a better recommendation on whom to branch on next.

This section presents the search heuristic as well as the search strategies used in ObjCP-FP. In constraint programming search heuristics cover both the variable selection heuristics as well as the domain splitting heuristics.

5.1 Variable Selection Heuristic

The variable selection heuristic is based on a measure of density of variable domain introduced in [32]. Roughly speaking, dens(x), the density of variable x, is obtained by dividing the cardinality of its domain by its width.

Note that 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 values in domains. Maximizing dens captures variables with huge numbers of values in relation to the size of the domains. Such variables may have a larger number of values appearing in solutions.

5.2 Domain Splitting Heuristic

When the search heuristic selects a variable, the solver must still divide the domain to explore the sub-problems. A 5-way split [8,32] of a variable x with domain [L..U] creates five sub-problems (except in degeneracy case) where D(x) is respectively restricted to [L..L], [U..U],[M..M],[] and [], where and denote the floating point value immediately preceding (respectively, following) v. M is the mid-point of the [L..U] interval. In this implementation, the 5-way split is enhanced to pick M differently and to allow the solver to focus on potentially interesting values by setting M = middle(L, U) with the function middle defined as

Interestingly, splitting on 1 (or 1) has the added benefit that it can split a domain in equal-sized chunks. Indeed, about half the floating point numbers are in the range [1], so with a domain equal to [0], splitting at 1 creates two sub-problems with equal-sized domains.

Blending splitting and enumeration is particularly interesting. Notably, finite domain solvers often rely solely on enumeration while MIP and continuous domain solvers are notoriously relying on splitting alone. The combination of both techniques is valuable as enumerating on interesting values (either bounds or the split point) produces the smallest possible intervals for the variable branched on and can lead to a significant level of propagation that may not occur when only splitting. Yet, enumeration alone is impractical given the sheer domain size when looked at as a discrete set.

5.3 Diversification Strategy

During the search, focusing on the same variable can be counter-productive and it may be wise to prevent the re-selection of the same variable at the next node. Focusing on the same variable at the top of the search tree can lead to a good reduction during propagation. But after a few re-selections, these reductions have less impact. Forcing the variable to change during the search leads to a more constrained problem and has a greater impact on filtering.

Diversification techniques come from meta-heuristics. A classic example is Tabu search [14] which prevents the repetition of local moves that undo recent changes. Tabu insists on shifting the focus to changes involving other variables, thereby driving the search in a different part of the search space. Tabu has rarely been considered in the context of a complete tree search. Indeed, 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, consider a variable with a large domain and a simple bisection heuristic for branching. The variable selection heuristic may find the variable appealing, and repeatedly branch on it until its domain density drops below others. Since density is not uniform, and without a Tabu block, such obstinacy may trigger a dive to a large depth before switching to another variable.

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 to

Intuitively, the search is prohibited to consider x again until the depth exceeds last(x). When the search considers a tree node n, the selection heuristic may instead choose to consider

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.

The following section evaluates ObjCP-FP and compares it to state-of-the-art solvers from the SMT community as well as Colibri, another solver from the CP community. The section discusses the benchmarks and reports on comparisons from multiple perspectives, wrapping up with an analysis of the relative merits of the two novel techniques introduced here.

6.1 Benchmarks

The framework introduced in this paper is implemented in ObjCP-FP and the evaluation uses the QF FP SMTLIB benchmarks. The evaluation focuses on the benchmark suite proposed by A.Griggio, i.e., a set of 214 benchmarks containing 117 satisfiable instances (i.e., program where a counter-example exists), and 97 unsatisfiable ones (i.e., correct programs).

All the experiments are made on a Linux machine with an Intel Xeon CPU E5-2620 2.00 GHz and 16GB with a timeout of one minute. The comparison includes the CP solver COLIBRI [20] and state-of-art SMT solvers : Mathsat [6], Z3 [9], CVC4 [1], and SONOLAR [19]. The comparison is based one the most recent (stable) version of each solver (i.e., COLIBRI v2176, Mathsat v5.5.4, Z3 v4.8.6, SONOLAR vDec2014, CVC4 v1.7).

In [32], one finds results on a collection of search heuristics for program verification that exploit properties of variables and their domain. It concludes that density are particularly effective for variable selection heuristics. While the results included on this paper focus exclusively on the use of density, all search heuristics benefit from the techniques described in this paper.

Table 1. Comparison of the different approach

6.2 Reporting and Validation

In the following tables, the time needed for symbolic processing is included in the solving time. All run times are in minutes except Table 3 which uses seconds.

Note that all results were cross-checked for correctness against SMT solvers through the injection of the solutions (in case of SAT instances) for a pure instantiation check. The conjunction of the solution and the initial model is given to other solvers to check that the resulting model is indeed correct. For UNSAT benchmarks, we check that the result is consistent with SMT solvers (also UNSAT).

6.3 Results and Discussion

The main results of the paper are reported in Table 1 which compares all solvers with the proposed approach (i.e., ObjCP-FP). The table reports the percentage of solved instances, the number of timeout and the total time (in minutes). The results are broken down into two categories for benchmarks with solutions (SAT) and benchmarks without solution (UNSAT). A last set of rows reports aggregate results (ALL).

While MathSAT-ACDCL is undeniably the strongest contender among SMT solvers, it is dominated by Colibri which is itself outperformed in all categories by ObjCP-FP. Indeed, ObjCP-FP leads in the fraction of solved instances and in the CPU time spent in doing so. The margin is also significant as ObjCP-FP is 4.2 times faster than MathSAT-ACDCL and produces 5.6 times fewer timeouts. The dominance is present in both SAT and UNSAT categories but is particularly striking on SAT instances where the best SMT solver (SONOLAR) produces 35 timeouts against only one for ObjCP-FP. Almost all SAT benchmarks except one are actually solved by our solver in less than 4 minutes. The second best solver, i.e., Colibri fails on 21 of these benchmarks and requires almost half an hour of CPU. When considering the aggregate results, it becomes quite evident that solvers that exploits the problem semantics with dedicated filtering (through a theory as MathSAT-ACDCL or via CP – Colibri and ObjCP-FP–) lead the pack. Yet, a dedicated search and an even sharper focus on exploiting structures paid off handsomely for ObjCP-FP. A second observation can be

Table 2. Comparison of all solvers over the subset of benchmarks solved by every tool

Table 3. Comparison of 5 VBS

made when contrasting the results of each solver in the SAT and UNSAT categories. All solvers except MathSAT-ACDCL do much better on SAT instances than on UNSAT instances and ObjCP-FP fits that description too (with 99.15% of SAT instances solved and 88.66% of UNSAT instances solved). MathSAT-ACDCL appears to favor UNSAT instances with 74% solved UNSAT vs. 64% solved SAT.

Comparison on Tractable Instances Table 2 focuses on the 44 benchmarks solved by every solver. This set of benchmarks includes 30 satisfiable and 14 unsatis-fiable instances. The recorded times are in seconds. Even when focusing on the set of problems solved by everyone, ObjCP-FP is still substantially faster (from 4 times faster to 60 times).

Virtual Best Solver Comparison Table 3 compares 5 different Virtual Best Solver (VBS). These virtual solvers corresponds to “solver portfolios”, i.e., for each benchmark, the result of the VBS is the result of the best solver for that particular benchmark. Five VBS are reported:

Naturally, the ALLSMT VBS that includes a solver using the semantics of constraints dominates the pure bit-blasting approaches across the board. The gains are particularly telling in the UNSAT category. Second, the CP VBS, which includes only two solvers, delivers only 6 timeouts and wraps up the entire computation in under 10 minutes or nearly 5 times faster than the SMT

Table 4. Comparison of different options for ObjCP-FP

VBS. Finally, observe how adding the SMT VBS to the CP VBS (i.e., ALL) barely improves over a CP approach. Interestingly the results from every solver but ObjCP-FP fail to improve over ObjCP-FP.

Contributions of each technique Table 4 presents the impact of each technique used by our solver. The column NONE corresponds to the 2017 version of ObjCPFP without any new techniques. DIV is ObjCP-FP augmented by diversifica-tion. CSE’s column is ObjCP-FP with common sub-expression elimination. Column DIV+CSE is ObjCP-FP with both techniques included. Finally, DIV+CSE+CY, which corresponds to the 2019 version of ObjCP-FP, adds cycle elimination to DIV+CSE. The table records the percentage of solved instances, the number of timeouts and the total time (in minutes) for each configuration (SAT, UNSAT and ALL).

CY allows to solve only one more problem. More interestingly, DIV and CSE are two effective and additive (or near additive) techniques and thus fully orthogonal. Namely, they contribute to improvements to (mostly) disjoints sets of benchmarks indicating a huge gain for doing both as shown in column DIV+CSE. Perhaps counter-intuitively, DIV is quite effective on UNSAT benchmarks where the percentage of solved instances jumps from 60% to 84.6% while the gains on SAT instances attributable to DIV are far more modest (+6%). Augmenting ObjCP-FP by diversification technique increases the percentage of solving benchmarks by 15% and reduces the required time by 30 minutes. Likewise, augmenting ObjCP-FP with common sub-expression elimination increases this percentage by 10% and reduces the total time by 24 minutes. When both are combined, 25% (15% of diversification + 10% of common sub-expression elimination) new benchmarks are now solved. The solving time is reduced by 56 minutes : more than 30 gained by diversification and 24 gained by CSE.

In this paper we have introduced the 2019 version of ObjCP-FP, a novel and effi-cient constraint programming framework for floating point verification problems expressed with the SMT language of SMTLIB. In this framework, constraints over the floats are first class objects, and thus ObjCP-FP can take advantage of the structures of floating point domains to boost the search process. The symbolic rewriting step that eliminates useless auxiliary variables and the di-versification techniques implemented within the search are two key features of this new solver. The experiments demonstrate that the abstraction level and the flexibility of constraint programming are very well adapted for solving standard floating point benchmarks of the SMT community. A detailed analysis of the experiments shows that ObjCP-FP is particularly effective on difficult problems that require significant numerical calculations, whereas SAT based solver are better on problems that require limited numerical computations. Future work could focus on a deeper analysis of the specific capabilities of the different types of solvers, and on a more accurate analysis of the complexity of the required numerical computations.

1. 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 , volume 6806 of Lecture Notes in Computer Science, pages 171–177. Springer, July 2011. Snowbird, Utah.

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

3. Martin Brain, Vijay D’Silva, Alberto Griggio, Leopold Haller, and Daniel Kroening. Deciding floating-point logic with abstract conflict driven clause learning. Formal Methods in System Design, 45(2):213–245, 2014.

4. Martin Brain, Florian Schanda, and Youcheng Sun. Building better bit-blasting for floating-point problems. In Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part I, pages 79–98, 2019.

5. Angelo Brillout, Daniel Kroening, and Thomas Wahl. Mixed abstractions for floating-point arithmetic. In Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15-18 November 2009, Austin, Texas, USA, pages 69–76, 2009.

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

7. Edmund Clarke, Armin Biere, Richard Raimi, and Yunshan Zhu. Bounded model checking using satisfiability solving. Formal Methods in System Design, 19(1):7–34, Jul 2001.

8. H´el`ene Collavizza, Claude Michel, and Michel Rueher. Searching critical values for floating-point programs. In Testing Software and Systems - 28th IFIP WG

6.1 International Conference, ICTSS 2016, Graz, Austria, October 17-19, 2016, Proceedings, pages 209–217, 2016.

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.

10. Mehmet Dincbas, Pascal Van Hentenryck, Helmut Simonis, Abderrahmane Ag- goun, Thomas Graf, and Fran¸coise Berthier. The constraint logic programming language chip. In FGCS, 1988.

11. Bo Einarsson. 1. What Can Go Wrong in Scientific Computing?, pages 3–12. Society for Industrial and Applied Mathematics, 2005.

12. Mikhail R. Gadelha, Felipe Monteiro, Lucas Cordeiro, and Denis Nicole. Esbmc v6.0: Verifying c programs using k-induction and invariant inference. In Dirk Beyer, Marieke Huisman, Fabrice Kordon, and Bernhard Steffen, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 209–213, Cham, 2019. Springer International Publishing.

13. Jes´us Gir´aldez-Cru and Jordi Levy. Generating sat instances with community structure. Artif. Intell., 238(C):119–134, September 2016.

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

15. Fran¸cois Delobel H´el`ene Collavizza and Michel Rueher. Comparing partial consis- tencies. Reliable Computing, 5:1–16, 1999.

16. IEEE. 754-2008 - ieee standard for floating-point arithmetic. 2008.

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

18. Philippe Laborie, J´erˆome Rogerie, Paul Shaw, and Petr Vil´ım. Ibm ilog cp opti- mizer for scheduling. Constraints, 23(2):210–250, April 2018.

19. Florian Lapschies. Sonolar, the solver for non-linear arithmetic, 2014.

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

21. Claude Michel. Exact projection functions for floating point number constraints. In International Symposium on Artificial Intelligence and Mathematics, AI&M 2002, Fort Lauderdale, Florida, USA, January 2-4, 2002, 2002.

22. Claude Michel, Michel Rueher, and Yahia Lebbah. Solving constraints over floating-point numbers. In Principles and Practice of Constraint Programming - CP 2001, 7th International Conference, CP 2001, Paphos, Cyprus, November 26 - December 1, 2001, Proceedings, pages 524–538, 2001.

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

24. Laurent D. Michel and Pascal Van Hentenryck. A microkernel architecture for constraint programming. Constraints, 22(2):107–151, 2017.

25. George L. Nemhauser and Laurence A. Wolsey. Integer and Combinatorial Optimization. Wiley-Interscience, New York, NY, USA, 1988.

26. U.S. Government Accountability Office. Software problem led to system failure at dhahran, saudi arabia. In US GAO Reports, report no. GAO/IMTEC-92-26., 1992.

27. Gilles Pesant. Counting-Based Search for Constraint Optimization Problems. In 30th AAAI Conference on Artificial Intelligence, AAAI 2016, 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. Edward Tsang. Constraint Based Scheduling: Applying Constraint Programming to Scheduling Problems. Journal of Scheduling, 2003.

30. Pascal Van Hentenryck and Laurent Michel. The objective-cp optimization system. In Principles and Practice of Constraint Programming: 19th International Conference, CP 2013, Uppsala, Sweden, September 16-20, 2013. Proceedings, pages 8–29, Berlin, Heidelberg, 2013.

tions for model construction. In Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19-22, 2014. Proceedings, pages 344–359, 2014.

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