Exploiting binary floating-point representations for constraint propagation

Reliability, testing and fault tolerance of networks and computer systems (68M15) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical problems of computer architecture (68M07) Numerical algorithms for computer arithmetic, etc. (65Y04)

Abstract: 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 is a hot research topic. 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, as 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.

Recommendations

Cites work

Cited in

(9)

Describes a project that uses

Uses Software

This page was built for publication: Exploiting binary floating-point representations for constraint propagation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2806863)