********************************************************************* * 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 * ********************************************************************* *** Jeudi 25 novembre 1999 **** 15h00 **** Ecole Polytechnique ***** Soutenance de these : Representation d'ensembles d'arbres pour l'interpretation abstraite Laurent MAUBORGNE le jeudi 25 novembre a 15h00 en amphi Becquerel (a l'Ecole polytechnique). Vous etes tous cordialement invites a la soutenance et au pot qui suivra. Vous pouvez trouver une description du sujet de la these a l'adresse: http://www.di.ens.fr/~mauborgn/these.html *** Vendredi 26 novembre 1999 **** 14h00 *************************** Jerome FERRET (LIX) The design of Pi-S.A. : a generic static analysis tool for the Pi-calculus Re'sume' : The pi-calculus is a formalism wich describes communications in a system of processes. It can be used for representing for instance a phone network or a key exchange protocole. The static analysis of the pi-calculus has not been deeply studied yet, whereas such an analysis would permit to verify many important properties. In the case of a phone network you could check that concrete resources will never be exhausted or overflowed. In the case of a key exchange protocole you could guarantee security constraints by proving that particular channels cannot be linked one to each other. For many reasons such goals cannot be reached with the traditional operational semantics of the pi-calculus, because it deals with an infinity of subprocesses, and uses the arbitrary method of alpha-conversion to assign names to new channels. We will design a non-standard lazy semantic in which, in one hand processes are duplicated only when it is necessary, and in the other hand, new channel names are precisely determined. We will then use Abstract Interpretation to design a generic static analyser for pi-calculus processes. We will instantiate this analyser with abstracts domains fitting well to the communication properties we will deal with. Finally, we will elaborate on the possibility of analysing a subprocess regardless of the rest of the processes in the system, wich would lead to a modular analysis. ********************************************************************* Pour recevoir l'annonce par courrier electronique: cousot@di.ens.fr WWW: http://www.di.ens.fr/~cousot/annonceseminaire.shtml *********************************************************************