| Authors | M. Carlier and A. Gotlieb |
| Title | Filtering by ULP Maximum |
| Afilliation | Software Engineering, Software Engineering |
| Status | Published |
| 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 |
| Date Published | 11/2011 |
| Publisher | IEEE |
| 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 Key | Simula.simula.880 |
