Annuaire des projets

COVERIF

Vers une combinaison de l’interprétation abstraite pour des programmes embarqués avec des calculs en virgule flottante

Les applications embarquées sont de plus en plus nombreuses et leur caractère critique ne cesse d’augmenter. La capacité à vérifier la correction et la robustesse des décisions devient un enjeu majeur, en particulier pour les programmes basés sur des calculs avec des nombres à virgule flottante. L’interprétation abstraite et la programmation par contraintes, deux des approches utilisées en vérification, ont en commun de déterminer l’ensemble des valeurs atteignables par les variables du problème qu’elles traitent, grâce à un calcul itératif de point fixe. Ce projet vise à explorer de nouvelles méthodes basées sur une collaboration fine entre l’interprétation abstraite et la programmation par contraintes. L’objectif est de repousser les limites inhérentes à ces deux techniques, d’améliorer la précision des estimations, de permettre une vérification plus complète des programmes utilisant des calculs sur les flottants, et de rendre ainsi plus robustes les décisions liées à ces calculs.