********************************************************************* * Ecole Normale Supe'rieure * * * * Se'minaire * * SEMANTIQUE ET INTERPRETATION ABSTRAITE * * P. Cousot * * * * Vendredi, 14h00--15h30 * * Salle R, etage -1 * * DI ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* *** Vendredi 11 janvier 2002 **** 14h00 ***************************** Relache (NYU). *** Vendredi 18 janvier 2002 **** 14h00 ***************************** Relache (POPL). *** Vendredi 25 janvier 2002 **** 14h00 ***************************** Matthieu MARTEL (CEA) Propagation des Erreurs d'Arrondi dans les Calculs en Pre'cision Finie. Re'sume': Les calculs numériques réalisés par ordinateur sont souvent accueillis avec une certaine méfiance car les erreurs d'arrondi peuvent fausser les résultats. De plus, il est difficile pour un programmeur de déterminer la précision d'un résultat ainsi que les opérations qui introduisent les principales erreurs. Dans cet exposé, nous présentons une sémantique non-standard des opérations en virgule flottante pour modéliser la propagation des erreurs d'arrondi pendant un calcul. Chaque opération élémentaire introduit un nouveau terme d'erreur du premier ordre et la combinaison de ces termes au cours des opérations suivantes crée des termes d'erreur d'ordre supérieur. Cela permet de déterminer quelles opérations ont introduit les principales erreurs faussant le résultat. Notre première sémantique modélise la propagation des erreurs de tout ordre et nous nous intéressons par la suite à des approximations sûres de celle-ci. D'une part nous montrons comment étudier seulement les termes d'erreur d'un ordre maximal tout en s'assurant que les termes d'ordre supérieur restent négligeables. D'autre part nous montrons qu'il est possible de paramétrer la granularité des opérations et de traiter de manière atomique les erreurs introduites lors de calculs intermédiaires. Nous montrons que ces sémantiques approchées sont des abstractions correctes de la sémantique la plus générale. Enfin, nous nous intéressons à une interprétation abstraite fondée sur les sémantiques décrites ci-dessus et nous présentons les premiers résultats produits par un analyseur en cours d'implémentation. ********************************************************************* Pour recevoir l'annonce par courrier electronique: cousot@di.ens.fr WWW: http://www.di.ens.fr/~cousot/annonceseminaire.shtml *********************************************************************