********************************************************************* * Ecole Normale Supe'rieure * * * * Se'minaire * * SEMANTIQUE ET INTERPRETATION ABSTRAITE * * P. Cousot * * * * Vendredi, 14h00--15h30 * * Salle W, 4e`me e'tage, toits du DMI * * DMI ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* *** Vendredi 5 mars 1999 **** 14h00 ********************************* Model Checking for Integer-Valued Systems with Constraints over Reals Andreas Podelski (Max-Planck-Institut, Saarbruecken) Re'sume' : We present a translation of concurrent systems to CLP programs such that a temporal property is exactly a CLP program semantics. This yields a constraint-based model-checking method, which we have implemented in a CLP system and used to verify well-known examples of infinite-state programs over integers. We employ several optimizations by abstraction: the relaxation to linear constraints over reals, and widening and narrowing techniques. In order to exclude "don't know" answers which may usually arise when abstraction is employed, we investigate ways to obtain accurate (or ``complete'') abstractions. This is joint work with Giorgio Delzanno. *** Vendredi 12 mars 1999 **** 14h00 ******************************** Relache. *** Vendredi 19 mars 1999 **** 14h00 & 15h30 ************************ Dependence Analysis for Recursive Data Yanhong Annie LIU (Indiana University, Bloomington) Re'sume' : Suppose we have a program that performs expensive computations and returns the results in a recursive data structure. Suppose for some purpose, we need only parts of those results, perhaps as input to another program. How can we automatically, efficiently, and precisely determine all the dead data and dead computations in the original program? How can we even describe the recursive substructure that we need? We describe a general and powerful method for dependence analysis in the presence of recursive data constructions. The particular analysis is for identifying partially dead recursive data, but the general framework for representing and manipulating recursive substructures applies to all dependence analyses. The method uses regular tree grammars extended with notions of live and dead. All grammar operations used in the analysis have efficient algorithms. The overall analysis yields significantly more precise results than other known methods. A prototype implementation demonstrates the efficiency and preciseness. -------------------------------------------------------------------- Automated verification of authentication protocols Scott D. STOLLER (Indiana University) Resume' : Many cryptographic protocols (for authentication, electronic commerce, etc.) are required to work correctly in systems allowing an unbounded number of concurrent runs of the protocol and containing an adversary that can perform an unbounded number of operations (encryption, decryption, etc.) while fabricating messages. Such systems are not finite-state, so state-space exploration tools such as model checkers ---the dominant technology for general-purpose automated verification--- are not directly applicable. Reduction theorems are needed, which show that if a protocol satisfies certain properties when appropriate small bounds are placed on the numbers of runs and operations, then the protocol is correct (in the unbounded setting). This talk focuses on reductions for authentication and key establishment protocols; the approach should apply to other classes of cryptographic protocols as well. *** Vendredi 26 mars 1999 **** 14h00 ******************************** Utilisation de l'abstraction des specifications temporelles dans l'implementation des systemes en temps reels. Anatole URSU (LIX) Prenom NOM (Institution) Re'sume' : Nous proposons une methode d'implementation des systemes en utilisant l'abstraction des specifications temporelles du type formules de transition. La methode est base sur l'analyse de la satisfiabilite des specifications temporelles abstraites qui sont obtenues a partir des specifications concretes par l'abstraction des etats du systeme specifie. L'abstraction est basee sur la transformation des ensembles d'evenements associes aux etats concrets du systeme dans un ensemble d'evenements abstraits. Cette procedure permet d'eliminer l'information incomplete sur les etats du systeme et d'introduire un domaine d'evenements abstraits. Cela permet de transformer les specifications temporelles qui contiennent des predicats d'etats et des variables propositionnelles d'evenements dans des specifications propositionelles des sequences d'evenements abstraites. Pour ce type des specifications temporelles abstraites nous proposons une methode simple d'analyse de la satisfiabilite par la resolution d'un systeme des equations de point fixe. Le raffinement de l'automate abstrait, obtenu de l'analyse de la satisfiabilite, est effectue par la concretisation des evenements abstraits. Les specifications temporelles du protocole de transport TP0 sont utilisees dans un exemple de conception pour montrer l'avantage pratique de l'utilisation des specifications abstraites dans la conception d'un systeme concret. ********************************************************************* Pour recevoir l'annonce par courrier electronique: cousot@dmi.ens.fr WWW: http://www.dmi.ens.fr/~cousot/annonceseminaire.html *********************************************************************