Filtering by ULP Maximum

Matthieu Carlier 1 Arnaud Gotlieb 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
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.
Type de document :
Communication dans un congrès
Proc. of the IEEE Int. Conf. on Tools for Artificial Intelligence (ICTAI'11), Nov 2011, Floride, United States. 2011
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00699565
Contributeur : Arnaud Gotlieb <>
Soumis le : lundi 21 mai 2012 - 11:31:38
Dernière modification le : mercredi 16 mai 2018 - 11:23:28
Document(s) archivé(s) le : mercredi 22 août 2012 - 02:25:33

Fichier

CG_ICTAI.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00699565, version 1

Citation

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. 2011. 〈hal-00699565〉

Partager

Métriques

Consultations de la notice

215

Téléchargements de fichiers

114