Projet ANR-15-CE25-0002 – Coverif : Vers une combinaison de l’interprétation abstraite et de la programmation par contraintes pour la vérification de propriétés critiques pour  des  programmes embarqués avec des calculs en virgule flottante
Programme : Sciences et technologies logicielles (DS0705) 2015
Année de financement : 2015
Coordinateur du projet : Monsieur Eric Goubault (Laboratoire d'Informatique de l'Ecole Polytechnique)
Montant : 751167.0 euros
Date de début : 2015
Durée : 48 mois
Résumé : Pouvoir vérifier la correction et la robustesse des programmes et systèmes devient un enjeu majeur dans une société où les applications embarquées sont de plus en plus nombreuses et où leur caractère critique ne cesse d’augmenter. C’est notamment un enjeu crucial pour le calcul basé sur l’arithmétique des nombres à virgule flottante, qui a des comportements assez inhabituels et  qui est de plus en plus utilisée dans les logiciels embarqués. Notons par exemple le phénomène de “catastrophic cancellation” qui invalide la plupart des chiffres significatifs d’un résultat ou encore, des suites numériques dont le point de convergence est très différent sur les réels et sur les flottants. Un problème vient aussi de la difficulté  à relier le calcul sur les flottants avec un calcul “idéalisé” qui serait effectué avec des nombres réels, la référence de fait lors de la conception du programme. Pour certaines valeurs d’entrée, le flot de contrôle lié aux réels peut ainsi passer dans une branche de la conditionnelle tandis qu’il passe par l’autre pour les flottants. S’assurer qu’un code, malgré cette divergence de flot de contrôle calcule tout ce qu’il est censé calculer, avec une erreur minimale, est l’objet de l’analyse de robustesse, ou de continuité.  Le développement d'un ensemble de techniques et d’outils pour vérifier l’exactitude, la correction et la robustesse  est donc un challenge important dans le domaine des logiciels embarqués critiques.  L’objectif de ce projet est de contribuer à relever ce défi  en explorant de nouvelles méthodes basées sur une collaboration fine entre interprétation abstraite (IA)  et programmation par contraintes (PPC). Plus précisément, il s’agit 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 critiques liées à ces calculs. Un des originalités de ce projet est de combiner les deux approches, pour permettre à la preuve de robustesse de bénéficier d’une précision accrue, par l’utilisation de techniques PPC, et le cas échéant, pour exhiber des cas non robustes. Il s’agit aussi de marier les forces des deux techniques : la PPC propose des mécaniques algorithmiques puissantes, mais chères en temps de calcul, pour atteindre des domaines d’une précision arbitraire fixée. L'IA n’offre pas de contrôle fin sur la précision atteinte, mais a développé de nombreux domaines abstraits qui capturent très rapidement des invariants de programme de formes diverses. En intégrant certains mécanismes de la PPC (arbre de recherche, heuristiques) dans des domaines abstraits, on pourra, en présence de fausses alarmes, raffiner le domaine abstrait en se basant sur une notion de précision. 
La première difficulté à résoudre est d’asseoir les bases théoriques d’un analyseur basé sur deux paradigmes substantiellement différents. Lorsque les interactions entre PPC et IA seront bien formalisées, le deuxième verrou que nous visons à lever est de gérer des contraintes de formes générales et des domaines abstraits potentiellement non-linéaires. Enfin, un verrou important du projet concerne l’analyse de robustesse de systèmes plus généraux que les programmes, par exemple les systèmes hybrides, qui modélisent les programmes de contrôle commande
Les résultats des recherches menées dans ce projet seront validés sur des exemples réalistes issus du monde industriel, afin d’en déterminer l’intérêt et la pertinence. L’utilisation d’exemples réels est un des points clefs de la validation des approches explorées : de par la complexité dans le pire des cas des problèmes traités, les techniques proposées ne traitent de manière acceptable que des sous classes de problèmes. Ainsi, les solutions adoptées restent souvent liées aux problèmes ciblés.