Détection des cas de débordement flottant avec une recherche locale

National audienceDans ce papier, nous proposons une nouvelle approche de génération automatique des cas de test, de programmes de calcul numérique, qui donnent lieu à des débordements flottants. Afin de résoudre les contraintes sur les flottants modélisant cette problématique, nous proposons un algorithme de recherche locale mis en oeuvre avec la bibliothèque multi-précision MPFR. Notre démarche de résolution procède en deux étapes : exploitation d'une recherche locale classique (e.g., méthode de gradient) pour avoir une solution sur le domaine réel, puis un algorithme spécifique de recherche locale pour déterminer la solution exacte qui mène immanquablement à un débordement flottant. La démarche MLFP qu'on propose permet de trouver évidemment une seule solution, car une recherche complète serait trop couteuse en raison de la nature fortement exponentielle de l'espace des flottants. Nous exploitons la bibliothèque multi-précision MPFR tout au long de notre résolution en deux étapes pour sécuriser le solveur contre tout débordement lors de la recherche numérique de la solution flottante. Car, parmi les contraintes du problème, il existe des contraintes dédiées à l'expression de l'état de débordement qui, d'une part utilise des constantes qui sont à la limite du débordement, et d'autre part l'évaluation de ces contraintes va nécessairement provoquer un débordement dans la représentation flottante de la machine. Le recours à une précision plus grande permettrait d'atteindre des solutions sans que le solveur en souffre. Nous avons mené plusieurs expérimentations de cette démarche sur des programmes significatifs. Cette expérimentation a montré l'intérêt de la première recherche locale dont la précision de la solution est importante pour que la deuxième recherche locale puisse explorer un espace réduit sur les flottants