********************************************************************* * Ecole Normale Supe'rieure * * * * Se'minaire * * SEMANTIQUE ET INTERPRETATION ABSTRAITE * * P. Cousot * * * * Vendredi, 14h00--15h30 * * Salle W, 4e`me e'tage, toits du DMA * * DI ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* *** Vendredi 28 janvier 2000 **** 14h00 *************************** Franck VEDRINE (ENS) Analyses totales de programmes par Interpretation Abstraite, Application au langage C++ Soutenance de these, Amphi Becquerel, Ecole Polytechnique, (RER B Lozere). Cette th`ese porte sur la construction d'analyses traitant l'ensemble des propri'et'es d'un programme afin d'avoir une preuve de correction totale de logiciels. Une telle analyse est appel'ee analyse totale par opposition aux analyses partielles telles les analyses de n'ecessit'e, de temps de liaisons, de typage, de propagation des constantes, qui ne s'int'eressent qu'`a un seul aspect du programme, aussi complexe soit-il. Les applications principales sont le test abstrait et l'optimisation de la compilation. Une telle analyse pourrait intervenir d`es l''edition du code soit de mani`ere semi-automatique avec interaction avec le programmeur pour des preuves de correction, soit de mani`ere automatique avec perte de pr'ecision pour l'optimisation du code. Plusieurs applications seront pr'esent'ees. Une premi`ere application sur s'emantique d'enotationnelle correspond `a l'analyse d'un mini langage de type ML avec une s'emantique paresseuse. Les propri'et'es les plus complexes `a capturer sont les propri'et'es de terminaison totale (pour tous les arguments) qui ne sont vraies qu'`a la limite en g'en'eral pour des fonctions r'ecursives. Le proc'ed'e de capture s'effectue `a l'aide d'it'erations ordinales croissantes (calcul'ees dynamiquement) au lieu d'it'erations d'ecroissantes sur les arguments pour un ordre statique. Les applications sur s'emantiques op'erationnelles concernent essentiellement l'analyse de programmes imp'eratifs. Comme illustraction, je pr'esenterai l'analyse compl`ete d'un petit programme C++ par sp'ecialisation. ********************************************************************* Pour recevoir l'annonce par courrier electronique: cousot@di.ens.fr WWW: http://www.di.ens.fr/~cousot/annonceseminaire.shtml *********************************************************************