********************************************************************* * Ecole Normale Supe'rieure * * * * Se'minaire * * SEMANTIQUE ET INTERPRETATION ABSTRAITE * * P. Cousot * * * * Vendredi, 14h00--15h30 * * Salle Verdier * * DI ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* *** Vendredi 1 decembre 2000 **** 14h00 ***************************** David MONNIAUX (ENS) Monte-Carlo et interprétation abstraite Re'sume' : Les méthodes de Monte-Carlo sont bien connues et très utilisées en analyse de systèmes stochastiques. Une de leurs limites pour l'analyse des systèmes informatiques est que, jusqu'à présent, elles ne permettaient pas d'analyser des systèmes à la fois stochastiques et non-déterministes au sens habituel. D'un autre côté, l'interprétation abstraite est une technique générale puissante pour l'analyse de programmes éventuellement non déterministes, mais elle gère encore mal les probabilités. Nous verrons donc comment combiner Monte-Carlo et interprétation abstraite. De plus, nous verrons comment l'interprétation abstraite peut servir à pallier le point noir commun à toutes les méthodes de Monte-Carlo, à savoir la lenteur de la convergence. *** Jeudi 7 decembre 2000 **** 11h00 ******************************** Soutenance de la these de Bruno Blanchet : Analyse d'échappement. Applications à ML et Java(TM) le jeudi 7 décembre à 11h, à l'Ecole polytechnique, amphi Fresnel. *** Vendredi 8 decembre 2000 **** 14h00 ***************************** Conseil scientifique du DI *** Vendredi 15 decembre 2000 **** 14h00 **************************** Jean-Francois RASKIN (Universite' Libre de Bruxelles ) Verification of Non-Repudiation Protocols. A Game Approach. Re'sume' : In this talk, we report on a recent work for the verification of non-repudiation protocols. We propose a verification method based on the idea that non-repudiation protocols are best modeled as games. To formalize this idea, we use alternating transition systems, a game based model, to model protocols and alternating temporal logic, a game based logic, to express requirements that the protocols must ensure. This method is automated by using the model-checker Mocha, a model-checker that supports the alternating transition systems and the alternating temporal logic. An optimistic non-repudiation protocol is analyzed using Mocha. *** Vendredi 22 & 29 decembre 2000 **** 14h00 *********************** Rela^che. Bonnes fe^tes. ********************************************************************* Pour recevoir l'annonce par courrier electronique: cousot@di.ens.fr WWW: http://www.di.ens.fr/~cousot/annonceseminaire.shtml *********************************************************************