********************************************************************* * Ecole Normale Supe'rieure * * * * Se'minaire * * SEMANTIQUE ET INTERPRETATION ABSTRAITE * * P. Cousot * * * * Vendredi, 14h00--15h30 * * Salle U/V, etage -2 * * DI ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* *** Vendredi 6 decembre 2002 **** 14h00 ***************************** Leslie LAMPORT (Microsoft Research) High-Level Specifications: Lessons from Industry Travail commun avec Brannon BATSON (Intel) Re'sume' : The TLA+ specification language and the TLC model checker are described. Experience using them at Compaq/HP and Intel for writing and debugging high-level specifications is described, and lessons are drawn. Many popular fads are found to be irrelevant to high-level specification. *** Vendredi 13 decembre 2002 **** 14h00 **************************** Franc,ois POTTIER (INRIA) Une pre'sentation des range'es a` base de contraintes Re'sume' : Les range'es de Wand et Re'my offrent un langage pour repre'senter de fac,on finie des fonctions de domaine infini mais constantes en dehors d'un sous-domaine fini. Elles sont tre`s utiles pour associer des types pre'cis aux ope'rations sur les enregistrements. De plus, l'unification sur les range'es e'tant de'cidable et efficace, elles permettent l'infe'rence de types pour les extensions de ML dote'es d'enregistrements. On peut e'galement les employer dans des syste`mes de types plus avance's, munis par exemple de contraintes de sous-typage. J'ai re'cemment tente' d'effectuer une analyse de complexite' pour un algorithme de re'solution de contraintes de sous-typage (dites ``non structurelles'') en pre'sence de range'es. L'analyse se re've`le de'licate, car l'algorithme standard cre'e des variables auxiliaires, dont la prolife'ration me`ne a` une borne pessimiste. Pour obtenir une meilleure borne, j'ai imagine' une formulation diffe'rente du proble`me, ou` les range'es sont non plus repre'sente'es par des termes mais code'es par des contraintes. Ce nouvel algorithme se pre^te mieux a` l'analyse de complexite' et a l'inte're^t inattendu de proposer une nouvelle vision des range'es. *** Vendredi 13 decembre 2002 **** 15h30 **************************** David SCHMIDT (Computing and Information Sciences Dept., Kansas State University) Storeless Semantics and Separation Logic Abstract: Jonkers and Deutsch have promoted ``storeless semantics,'' where locations and even the store/heap disappear and are replaced by paths of identifiers and field selectors. Axiomatic (Hoare-) logic is a classic example of a storeless semantics, and in this talk, we present Reynolds-O'Hearn separation logic, an axiomatic logic for reasoning about heap storage, and employ it in a big-step semantics for an applicative, object-based language. We then (informally) abstractly interpret the semantics to recover a simple variant of Blanchet's escape analysis for an ML-subset. Our goal is to systematically derive modular region- and escape-analyses as instances of separation-logic semantics. *** Vendredi 20 decembre 2002 **** 14h00 **************************** Rela^che. ********************************************************************* Pour recevoir l'annonce par courrier electronique: cousot@di.ens.fr WWW: http://www.di.ens.fr/~cousot/annonceseminaire.html *********************************************************************