Contraintes sur les flottants (11/2000 - ...)

Mes travaux de recherches dans ce domaine portent sur la réalisation d'un solveur pour les systèmes de contraintes définies sur les nombres flottants. Ce travail s'inscrit dans le projet RNTL INKA² qui a pour objectif la réalisation d'un système automatique de génération de jeux de test structurel pour les programmes écrits dans des langages impératifs tels que C ou C++. Dans ce contexte, le traitement d'expressions utilisant des nombres flottants est un problème majeur. Le point délicat réside dans la recherche de données d'entré qui garantit que, lors de l'exécution, le programme C ou C++ passera effectivement par un point préalablement sélectionné. La résolution de ce problème nécessite la prise en compte du modèle de calcul propre aux flottants lors de la définition et de la résolution des contraintes.

• Filtrages conservatifs pour les contraintes sur les flottants

  Problème

  Élaborer des techniques de filtrages qui conservent l'ensemble des solutions de contraintes sur les flottants.

  Difficultés

  La difficulté provient du fait que les techniques utilisées sur les domaines continus (i.e. les réels) font appels à des propriétés qui ne sont pas conservées par l'arithmétique sur les flottants. Par exemple, si la relation $16.1 = 16.1 + x$ a pour unique solution sur les réels 0, elle admet n'importe quel flottant appartenant à l'intervalle $[ -1.77635683940025046e-15, 1.77635683940025046e-15]$ comme solution sur les flottants. Par ailleurs, les techniques de filtrage sur les domaines finis se révèlent être beaucoup trop lourdes pour filtrer des contraintes sur les flottants (il y a plus de $10^{18}$ flottants sur $64$ bits entre $-1.0$ et $1.0$). Il est donc nécessaire de développer des techniques adaptées au traitement des contraintes sur les flottants.
  

  Contributions

  • Définition d'une technique de filtrage basée sur la $box$-consistance et qui conserve l'ensemble des solutions sur les flottants (en collaboration avec Michel Rueher et Yahia Lebbah).
    Publication : Cette technique à fait l'objet d'un article long publié à CP2001 (7th International Conference on Principles and Practice of Constraint Programming).
    $\;$
    
  • Définition de fonctions de projections correctes et complètes pour les contraintes sur les flottants.
    Publication : Ces fonctions de projections ont fait l'objet d'article long au 7th AIMA (7th International Symposium on Artificial Intelligence and Mathematics).
    Perspectives :
    
  • Développement d'une véritable $2B$-consistance qui conserve l'ensemble des solutions de contraintes sur les flottants.
    Application des ces travaux à la vérification de la cohérence entre les spécifications d'un programme et son implémentation (Cette application fait l'objet d'un second RNTL (j'ai participé à l'élaboration de ce second RNTL)).