Une approximation du calcul en nombres réels sur les ordinateurs est l'arithmétique à virgule flottante, qui utilise une représentation finie des nombres. Ceci implique qu'une erreur d'arrondi (petite en général) peut être commise à chaque opération. Cette approximation est suffisamment précise pour la plupart des applications, mais il y a des cas dans lesquels les résultats ne sont plus représentatifs, à cause de pertes de précision à certaines étapes du calcul, ceci même lorsque le schéma numérique sous-jacent est stable.

Notre but est d'étudier la propagation des erreurs d'arrondi dans les calculs utilisant des nombres flottants, de façon à détecter automatiquement une éventuelle perte de précision catastrophique, et sa source dans le programme. Nous développons un analyseur statique, capable de traiter des cas industriels, et que nous pensons particulièrement adapté à l'étude des logiciels contrôle-commande critiques.

• Sémantiques concrètes et abstraites pour les operations sur les nombres flottants


• Analyse statique de programmes par interprétation abstraite

Contexte général Principe de l'analyse Présentation de l'analyseur FLUCTUAT Bibliographie du projet

• Eric Goubault,  email: eric.goubault@cea.fr


• Matthieu Martel, email: matthieu.martel@cea.fr


• Sylvie Putot, email: sylvie.putot@cea.fr

• 2000-2002 : projet RTD IST-1999-20527 DAEDALUS du programme européen FP5


• 2003-2004 : projet "Preuves Approchées", soutenu par la Direction des Programmes de l'Aviation Civile (DPAC)


• 2004 : Action Spécifique Validation numérique pour le calcul embarqué (GDR ARP, CNRS-STIC)


• 2004-2005: ACI-SI V3F : Validation et Vérification en présence de calculs à Virgule Flottante

 

Retour vers le laboratoire LSL