Exploiting binary floating-point representations for constraint propagation
| Autor: | Roberto Bagnara, Matthieu Carlier, Roberta Gori, Arnaud Gotlieb |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2016 |
| Předmět: |
Theoretical computer science
Floating point Test data generation Computer science Rounding General Engineering Binary scaling 020207 software engineering 02 engineering and technology Minifloat Computer engineering 0202 electrical engineering electronic engineering information engineering Local consistency 020201 artificial intelligence & image processing Software verification Test data |
| Popis: | Floating-point computations are quickly finding their way in the design of safety- and mission-critical systems, despite the fact that designing floating-point algorithms is significantly more difficult than designing integer algorithms. For this reason, verification and validation of floating-point computations are hot research topics. An important verification technique, especially in some industrial sectors, is testing. However, generating test data for floating-point intensive programs proved to be a challenging problem. Existing approaches usually resort to random or search-based test data generation, but without symbolic reasoning it is almost impossible to generate test inputs that execute complex paths controlled by floating-point computations. Moreover, because constraint solvers over the reals or the rationals do not natively support the handling of rounding errors, the need arises for efficient constraint solvers over floating-point domains. In this paper, we present and fully justify improved algorithms for the propagation of arithmetic IEEE 754 binary floating-point constraints. The key point of these algorithms is a generalization of an idea by B. Marre and C. Michel that exploits a property of the representation of floating-point numbers. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|