Filtering by ULP Maximum - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2011

Filtering by ULP Maximum

Résumé

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.
Fichier principal
Vignette du fichier
CG_ICTAI.pdf (108.63 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00699565 , version 1 (21-05-2012)

Identifiants

  • HAL Id : hal-00699565 , version 1

Citer

Matthieu Carlier, Arnaud Gotlieb. Filtering by ULP Maximum. Proc. of the IEEE Int. Conf. on Tools for Artificial Intelligence (ICTAI'11), Nov 2011, Floride, United States. ⟨hal-00699565⟩
134 Consultations
76 Téléchargements

Partager

Gmail Facebook X LinkedIn More