********************************************************************* * LIENS Ecole Normale Superieure * * * * Groupe de travail * * 'Semantique et Interpretation Abstraite' * * P. Cousot * * * * Vendredi, 10h--12h * * Salle Henri Cartan B, etage -2 * * DMI ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* *** Vendredi 7 mai 1993 ***** Seminaire ******* Henri Cartan B *** Nouvelles Applications des Syste`mes d'Effets. Pierre Jouvelot (CRI-ENSMP) Resume: La notion de syste`me d'effet permet d'envisager d'effectuer certaines analyses statiques de programmes fonctionnels type's d'ordre supe'rieur, en pre'sence a` la fois d'effets de bord ou de compilation se'pare'e. De nombreux re'sultats ont de'ja` e'te' obtenus en ce qui concerne l'analyse des effets de bord, de contro^le ou de communication. Nous de'taillons ici les dernie`res applications de cette approche, en particulier pour les analyses de complexite' et de flot de contro^le, ainsi que l'e'valuation partielle. *** Vendredi 14 mai 1993 ********* Seminaire ***** Henri Cartan B *** A copy/restore semantics of (some) higher-order languages and its applications Francois Bourdoncle (DEC-PRL) Resume: This talk is concerned with the abstract interpretation of higher-order languages with imperative features. We first show that the abstract interpretation of these languages based on their standard operational semantics (e.g., closures, stacks, etc) is very costly and inaccurate. We then introduce a new copy/restore semantics of these languages and show that it is equivalent to the standard one for a large and interesting class of programs containing, in particular, all second-order programs with jumps to non-local labels (e.g., Wirth- Pascal) and all higher-order programs with exceptions but without local procedures (e.g., C). *** Vendredi 21 mai 1993 *** Relache ******************************** *** Vendredi 28 mai 1993 ********* Seminaire ***** Henri Cartan B *** Model checking symbolique des syste`mes temps re'e'l Xavier Nicollin (VERIMAG, Grenoble) Resume: non parvenu. *********************************************************************