Bringing freedom in variable choice when searching counter-examples in floating point programs
This work addresses verification challenges for floating-point programs, offering incremental improvements in search strategies for constraint programming.
The paper tackles the problem of efficiently finding counter-examples in floating-point program verification by introducing a new search heuristic based on global occurrences and a technique that branches only on input variables, resulting in improved performance and reduced disparities between heuristics.
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.