Roberto, Margherita and Beatrice


Personal Info




Filtering Floating-Point Constraints by Maximum ULP

Roberto Bagnara
BUGSENG and Dipartimento di Matematica e Informatica
Università di Parma
Parco Area delle Scienze 53/A
I-43124 Parma

Matthieu Carlier
INRIA Rennes Bretagne Atlantique

Roberta Gori
Dipartimento di Informatica
Università di Pisa
Corso Italia 40
I-56125 Pisa

Arnaud Gotlieb
Certus Software V&V Center
SIMULA Research Laboratory
P.O.Box 134, 1325 Lysaker


Floating-point computations are quickly finding their way in the design of safety- and mission-critical systems, despite the fact that designing correct floating-point algorithms is significantly more difficult than designing correct 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 handle the 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 filtering of arithmetic IEEE 754 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.

[Page last updated on August 14, 2013, 17:25:56.]

© Roberto Bagnara

Home | Personal | Papers | Teaching | Links