Résolution de contraintes sur les nombres à virgule flottante par une approximation sur les nombres réels

Mohammed Said Belaid 1 Claude Michel 1 Michel Rueher 1
1 Laboratoire d'Informatique, Signaux, et Systèmes de Sophia-Antipolis (I3S) / Equipe CEP
Laboratoire I3S - MDSC - Modèles Discrets pour les Systèmes Complexes
Résumé : La mise en oeuvre effective de méthodes de vérification de programmes comportant des calculs sur les nombres à virgule flottante reste encore problématique. Cela est en partie dû aux difficultés inhérentes à l'arithmétique des nombres à virgule flottante dont la pauvreté des propriétés rend souvent impossible la transposition de résultats établis sur les réels. C'est pourquoi nous présentons dans cet article une nouvelle méthode de résolution de contraintes sur les nombres à virgule flottante qui consiste à les approximer sur les réels. En construisant des approximations sur les réels, fines et conservatives des solutions des contraintes sur les nombres à virgule flottante, cette méthode permet de s'appuyer sur l'utilisation d'algorithmes de filtrage sur les réels pour résoudre des problèmes sur les nombres à virgule flottante. Il devient ainsi possible de repousser les limitations actuelles des solveurs de contraintes sur les nombres à virgules flottantes, telles que le problème du passage à l'échelle, pour générer des jeux de tests, ou vérifier des programmes plus conséquents que ceux traités jusqu'à maintenant.
Type de document :
Communication dans un congrès
JFPC 2010 - Sixièmes Journées Francophones de Programmation par Contraintes, Jun 2010, Caen, France. pp.51-60, 2010
Liste complète des métadonnées

Littérature citée [12 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/inria-00520370
Contributeur : Christophe Lecoutre <>
Soumis le : jeudi 23 septembre 2010 - 09:11:53
Dernière modification le : lundi 5 novembre 2018 - 15:48:02
Document(s) archivé(s) le : jeudi 25 octobre 2012 - 11:22:15

Fichier

michel.pdf
Accord explicite pour ce dépôt

Identifiants

  • HAL Id : inria-00520370, version 1

Collections

UNICE | I3S | JFPC2010 | UNIV-COTEDAZUR

Citation

Mohammed Said Belaid, Claude Michel, Michel Rueher. Résolution de contraintes sur les nombres à virgule flottante par une approximation sur les nombres réels. JFPC 2010 - Sixièmes Journées Francophones de Programmation par Contraintes, Jun 2010, Caen, France. pp.51-60, 2010. 〈inria-00520370〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

333

Téléchargements de fichiers

193

Contact


archive-ouverte@inria.fr