*********************************************************************
*                       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 1 novembre 1996 **** 14h00 *****************************

Rela^che

*** Vendredi 8 novembre 1996 **** 14h00 *****************************

Rela^che

*** Vendredi 15 novembre 1996 **** 14h00 ****************************

Rela^che

*** Vendredi 22 novembre 1996 **** 14h00 ****************************

Towards Verification and Debugging of Concurrent Constraint Programs
through Abstract Interpretation with Set Constraints

Andreas PODELSKI (Max-Planck-Institut fuer Informatik, Saarbruecken)

Re'sume' :  The existing, essentially automata-theoretic methods for 
verifying concurrent systems apply to systems such as circuits and network
protocols.  There, the number of concurrent processes is statically
fixed and the data dependencies in the control flow are simple (the
systems can be modeled as finite-state systems). In this talk, we will
address the problem of verifying more general concurrent systems. We
consider systems obtained by programs written in the CCP paradigm. We
deal with (CTL*-style) temporal-logic properties of system states
obtained from a restricted class of atomic properties.  Given a
program and the property to be verified (defining the set of "correct"
states), we first derive a set constraint.  This step is formalized as
an abstract interpretation process, which thus defines the degree of
approximation in our verification method.  Then, for the case of the
constraint domain over infinite trees, we solve the set constraint by
deriving an equivalent automaton over infinite trees.  This automaton
can then be used to test initial states for membership in the
approximation of the set of correct states.  If the automaton is
deterministic, the test is linear in the description of the initial
states.


*** Vendredi 29 novembre 1996 **** 14h00 ****************************

Topology in distributed computing: deadlocks and directed homotopy

Lisbeth FAJSTRUP and Martin RAUSSEN (Aalborg University)

Re'sume' :
   The problem of coordinating concurrent processes is central within
{\em distributed computing}. Coordination is difficult because
modern multiprocessor systems are inherently totally asynchronous
without global clocks; the execution speed of each processor may
fluctuate widely.

Classically, graph theory and logic were the main mathematical
disciplines used in theoretical computer science to analyse those
networks and to achieve theoretical bounds for coordination
problems. Recently, geometrically based models have found
considerable interest. Certain decidability problems have been solved
with methods from classical {\em combinatorial/simplicial topology}.

Cubical complexes, introduced by Serre in his work on fibrations
around 1950, were used to model ``Higher Dimensional Automata''.
What is new, is that time induces a direction into the model, giving
rise to ``light cones''. It seems interesting to look at ``{\em
directed geometry/topology/homotopy theory}'' to analyse some of
the properties of these automata.

As a particular example, we investigate {\em deadlocks} in
concurrent systems: this annoying situation arises when several
processors block each other. Deadlocks are shown to correspond to
local maxima in a directed graph modelling the space of states of
such a system. More generally, we propose a {\em critical point
analysis} \`{a} la Morse theory to analyse the directed topological
properties of these state spaces.

This survey talk will certainly include more questions than answers.

*********************************************************************
Pour recevoir l'annonce par courrier electronique: cousot@dmi.ens.fr
WWW: http://www.ens.fr/~cousot/annonceseminaire.html
*********************************************************************