*********************************************************************
*                       Ecole Normale Supe'rieure                   *
*                                                                   *
*                              Se'minaire                           *
*                SEMANTIQUE ET INTERPRETATION ABSTRAITE             *
*                              P. Cousot                            *
*                                                                   *
*                        Vendredi, 14h00--15h30                     *
*                           Salle U/V, etage -2                     *
*                  DI  ENS  45 rue d'Ulm  75005 Paris               *
*********************************************************************

*** Vendredi 1 novembre 2002 **** 14h00 *****************************

Fe'rie'

*** Vendredi 8 novembre 2002 **** 14h00 *****************************

Rela^che

*** Vendredi 15 novembre 2002 **** 14h00 ****************************

Rela^che

*** Vendredi 22 novembre 2002 **** 14h00 ****************************

Damien MASSE' (E'cole polytechnique)

Property Checking Driven Abstract Interpretation-Based Static Analyses

Re'sume' :
Concrete semantics used for abstract interpretation-based analyses are
generally expressed as fixpoints. Checking a property on this kind of
semantics can be done by intersecting the fixpoint with a specification
related to the property. In this talk, we will show how to produce a new,
"reverse" analysis from this specification. The result of
this analysis, expressed as a lower closure operator, is
then used to guide the initial analysis. With this approach,
we can refine the result given by the direct abstract analysis.
We show that this method enables to deduce forward analyses from backward
analyses (and vice-versa), and to combine them iteratively in a way
similar to the forward-backward combination of analyses.

This work will be presented to VMCAI'03 in january 2003.

*** Vendredi 29 novembre 2002 **** 14h00 ****************************

Alan MYCROFT (Computer Laboratory, University of Cambridge, UK)

Combined Code Motion and Register Allocation using the Value State
Dependence Graph

Travail commun avec Neil JOHNSON.

Re'sume' :

We define the Value State Dependence Graph (VSDG). The VSDG is a form of the
Value Dependence Graph (VDG) which includes state dependence edges to model
serialised computation. These are used to model store dependencies and loop
termination dependencies (thereby resolving a correctness problem with the
original VDG) of the original program. We show that state dependence edges
(now modelling implementation-oriented serialisation) can then be added until
the VSDG represents a single Control Flow Graph.

The central idea is that this can be done incrementally so that we have
a class
of algorithms which effectively interleave register allocation and code motion,
thereby avoiding a well-known phase-order problem in compilers. This class
operates by first normalising the VSDG during construction, to remove all
duplicated computation and performing maximal lifting from loops, and then
repeatedly choosing between:
- allocate a value to a register,
- spill a value to memory,
- move a loop-invariant computation within a loop
             to avoid register spillage, and
- statically duplicate a computation
             to avoid register spillage.

We show that the classical two-phase approach (code motion then register
allocation in both Chow and Chaitin forms) are examples of this class,
and propose a new algorithm based on depth-first cuts of the VSDG.

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