Searching input values hitting suspicious Intervals in programs with floating-point operations

TL;DR

This paper introduces a new constraint-based method to identify specific input values that cause floating-point computations in programs to hit suspicious intervals, addressing limitations of existing over-approximation tools.

Contribution

The paper presents a novel approach that searches for test cases within over-approximated error bounds to detect potential inappropriate behaviors caused by floating-point errors.

Findings

Successfully identifies inputs leading to suspicious floating-point behaviors

Improves precision over existing over-approximation methods

Helps developers validate floating-point program correctness

Abstract

Programs with floating-point computations are often derived from mathematical models or designed with the semantics of the real numbers in mind. However, for a given input, the computed path with floating-point numbers may differ from the path corresponding to the same computation with real numbers. A common practice when validating such programs consists in estimating the accuracy of floating-point computations with respect to the same sequence of operations in an ide-alized semantics of real numbers. However, state-of-the-art tools compute an over-approximation of the error introduced by floating-point operations. As a consequence, totally inappropriate behaviors of a program may be dreaded but the developer does not know whether these behaviors will actually occur, or not. In this paper, we introduce a new constraint-based approach that searches for test cases in the part of the over-approximation where errors due to floating-point arithmetic would lead to inappropriate behaviors.