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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [12 references]  Display  Hide  Download
https://hal.inria.fr/inria-00520370
Contributor : Christophe Lecoutre <>
Submitted on : Thursday, September 23, 2010 - 9:11:53 AM
Last modification on : Monday, November 5, 2018 - 3:48:02 PM
Long-term archiving on : Thursday, October 25, 2012 - 11:22:15 AM

File

michel.pdf
Explicit agreement for this submission

Identifiers

  • 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. ⟨inria-00520370⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

342

Files downloads

202

Contact


archive-ouverte@inria.fr