Bringing freedom in variable choice when searching counter-examples in
  floating point programs
  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. % 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 verified 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.
