*********************************************************************
*                       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 1er mars 2002 **** 14h00 *******************************

rela^che

*** Vendredi 8 mars 2001 **** 14h00 -- 15h00 ************************

Jacob A. ABRAHAM (Computer Engineering Research Center, The University
                  of Texas at Austin)

Taming Complexity Through Abstraction and Hierarchy: Applications to
Test Generation and Timing Verification

Re'sume': Complexity is the primary stumbling block to the effective
analysis of electronic designs.  This talk will describe a novel
hierarchical technique which focuses on one module of the design at a
time and abstracts the rest of the design into reduced logic.  The
underlying theory will be described with applications to manufacturing
test generation and full-chip timing verification.  Results of applying
these techniques to complex designs demonstrate improvements, in time
and quality of solution, several orders of magnitude better than
conventional approaches.


*** Vendredi 8 mars 2001 **** 15h00 -- 16h00 ************************

Mooly SAGIV (Tel Aviv University)

Static Program Analysis via 3-Valued Logic

Re'sume': Static program analysis is concerned with the problem of 
exploring a program's behavior for all possible inputs, but without
actually running the program on specific inputs.  One of the major
challenges is how to handle programs that use dynamically allocated
storage -- a feature found in all modern programming languages, including
C, C++, and Java.  In programs written in such languages, a program's data
structures can grow and shrink dynamically, with no fixed upper bound
on their size or number.  The analysis problem is complicated even
more by the fact that such languages also permit fields of dynamically
allocated objects to be destructively updated.  In the case of
thread-based languages, such as Java, the number of threads can also
grow and shrink dynamically -- again with no fixed upper bound on size
or number.

A key technical challenge is to find a way to create finite-sized
descriptors of memory configurations.  Such descriptors must abstract
away certain details of the memory configurations that can possibly
arise during execution, but must retain enough key information so that
the analysis can identify interesting properties that hold.  This talk
presents a recently developed framework for static program analysis
that addresses these issues by using 3-valued logic in a novel way.

I will present the abstract domain of 3-valued
structures and study its properties.

This is a joint work with T. Reps and R. Wilhelm.

A generalized version of the framework was designed and implemented by
T. Lev-Ami (http://www.cs.tau.ac.il/~rumster/TVLA).

*** Vendredi 16 mars 2001 **** 14h00 ********************************

rela^che

*** Vendredi 22 mars 2001 **** 14h00 ********************************

MFPS XVIII http://www.math.tulane.edu/~mfps/mfps18.html

*** Vendredi 29 mars 2001 **** 14h00 ********************************

rela^che

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