AuthorsM. Carlier and A. Gotlieb
TitleFiltering by ULP Maximum
Afilliation, Software Engineering
StatusPublished
Publication TypeProceedings, refereed
Year of Publication2011
Conference NameProceedings of the 23rd IEEE International Conference on Tools with Artificial Intelligence (ICTAI'2011), Nov. 7-9, 2011, Boca Raton, Florida, USA
Date Published11/2011
PublisherIEEE
Abstract

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.

Citation KeySimula.simula.880

Contact person