Next: Modèles et implémentation d'interprètes
Up: Activités de recherche
Previous: Activités de recherche
  Contents
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 INKA2 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
a pour unique solution sur les réels 0,
elle admet n'importe quel flottant appartenant à l'intervalle
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 flottants
sur bits entre et ). 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 -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 -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)).
Next: Modèles et implémentation d'interprètes
Up: Activités de recherche
Previous: Activités de recherche
  Contents
Claude Michel
2002-03-27