|Authors||M. Carlier and A. Gotlieb|
|Title||Filtering by ULP Maximum|
|Afilliation||, Software Engineering|
|Publication Type||Proceedings, refereed|
|Year of Publication||2011|
|Conference Name||Proceedings of the 23rd IEEE International Conference on Tools with Artificial Intelligence (ICTAI'2011), Nov. 7-9, 2011, Boca Raton, Florida, USA|
Constraint solving over floating-point numbers is an emerging topic that found interesting applications in software analysis and testing. Even for IEEE-754 compliant programs, correct reasoning over floating-point computations is challenging and requires dedicated constraint solving approaches to be developed. Recent advances indicate that numerical properties of floating-point numbers can be used to efficiently prune the search space. In this paper, we reformulate the Marre and Michel property over floating-point addition/subtraction constraint to ease its implementation in real-world floating-point constraint solvers. We also generalize the property to the case of multiplication/division in order to benefit from its improvements in more cases.