*********************************************************************
* 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
*********************************************************************