********************************************************************* * Ecole Normale Supe'rieure * * * * Se'minaire * * SEMANTIQUE ET INTERPRETATION ABSTRAITE * * P. Cousot * * * * Vendredi, 14h00--15h30 * * Salle R, etage -1 * * DI ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* *** Vendredi 3 mai 2002 **** 14h00 ********************************** Andy GORDON (Microsoft Research, http://research.microsoft.com/~adg) Types and effects for asymmetric cryptographic protocols Re'sume': We present the first type and effect system for proving authenticity properties of security protocols based on asymmetric cryptography. The most significant new features of our type system are: (1) a separation of public types (for data possibly sent to the opponent) from tainted types (for data possibly received from the opponent) via a subtype relation; (2) trust effects, to guarantee that tainted data does not, in fact, originate from the opponent; and (3) challenge/response types to support a variety of idioms used to guarantee message freshness. We illustrate the applicability of our system via protocol examples. Joint work with Alan Jeffrey, DePaul University. *** Vendredi 3 mai 2002 **** 15h00 ********************************** John Gallagher (University of Bristol) Tree Grammars with Constraints for Program Analysis Re'sume': Our starting point is set-based program analysis. In logic or functional programs, this analysis produces a recursive description of the set of terms corresponding to each variable in the program. This has many potential applications, including compiler optimisations, type-checking, debugging, verification and planning. We present a new practical algorithm for computing precise set-based descriptions, obtained by an abstract interpretation over non-deterministic tree grammars. Then we outline the abstract domain of tree grammars with constraints, and discuss the precision and practicality of this extension. *** Vendredi 10 mai 2001 **** 14h00 ********************************* Relache *** Vendredi 17 mai 2001 **** 14h00 ********************************* Lenore ZUCK (NYU, New York) Automatic Verification of Parameterized Systems Re'sume': The talk will briefly introduce the area of automatic formal verification, the challenges posed when attempting to automatically verify infinite-state systems, the notion of "parameterized systems", and the importance and implications of their automatic verification. The talk then will present three newly developed methodologies to deal with the task: (1) The method of "Invisible Invariants" that automatically verifies safety properties of parameterized systems, which has been tested on a wide variety of systems. (2) The method of "Counter Abstraction" that applies a well-studied abstraction technique in novel ways to automatically verify liveness properties of parameterized systems. (3) A simple variant of the method of "Network Invariants" that is applicable to automatic proofs of liveness properties of a wide range of parameterized systems. Joint work with Amir Pnueli. *** Vendredi 17 mai 2001 **** 15h00 ********************************* Gordon PLOTKIN (Laboratory for Foundations of Computer Science, Edinburgh, visiting ENS) An Algebraic View of Computational Effects Re'sume': Moggi introduced a monadic view of computational effects, whereby he was able to add non-functional features to functional programming languages. These include continuations, state, exceptions, interactive I/O and various kinds of nondeterminism. However he did not have a theory of the operations that actually give rise to (construct) the effects, such as nondeterministic choice, or outputting. We survey an algebraic approach to operations, and relate them to generic effects (e.g., tossing a random coin). We consider axiomatizations of the operations; such axiomatizations in fact determine the monads. We consider how to combine different kinds of effects. We consider associated operational semantics.We conclude with various difficulties and open problems, such as that of deconstructors, e.g. for handling exceptions. *** Vendredi 24 mai 2001 **** 14h00 ******************************** Rela^che. *** Vendredi 31 mai 2001 **** 14h00 ******************************** Prakash PANANGADEN (McGill University) From Logic to Stochastic Processes Re'sume': I will give a survey of developments in the cc languages from plain cc to - the as yet undiscovered - stochastic cc. The concurrent constraint programming paradigm evolved out of concurrent logic programming and had strong ties to logic. They abstracted from the variety of control mechanisms that were current then in concurrent logic programming languages and in functional languages with so called ``logic variables''. The cc family was purely asynchronous. In order to express reactive programs as in the family of synchronous languages one had to introduce time. This led to the language tcc which captures temporal notions. However, for synchronous programs one needs an orthogonal idea as well, that of a default. The presence of defaults introduces nonmonotonicity into the language. As we refine the notion of time and introduce a mixture of continuous time as well as discrete time we get a hybrid language called hcc. Proabilistic cc was introduced at the end of the 1990s. I will describe this evolution from logic programming languages to languages for modelling stochastic processes through programming examples. Much of the development is due to Vineet Gupta, Radha Jagadeesan and Vijay Saraswat. ********************************************************************* Pour recevoir l'annonce par courrier electronique: cousot@di.ens.fr WWW: http://www.di.ens.fr/~cousot/annonceseminaire.shtml *********************************************************************