*********************************************************************
*                       Ecole Normale Supe'rieure                   *
*                                                                   *
*                              Se'minaire                           *
*                SEMANTIQUE ET INTERPRETATION ABSTRAITE             *
*                              P. Cousot                            *
*                                                                   *
*                        Vendredi, 14h--16h                         *
*                 Salle W, 4e`me e'tage, toits du DMI               *
*                 DMI  ENS  45 rue d'Ulm  75005 Paris               *
*********************************************************************

*** Vendredi 2 decembre 1994 ****************************************

Petit panomara des analyses s\'emantiques de propri\'et\'es de
r\'egularit\'e des valeurs num\'eriques des programmes.

Philippe GRANGER (ENSTA)

Re'sume' :

Faire l'analyse s\'emantique d'un programme, c'est-\`a-dire
caract\'eriser \`a la compilation les valeurs prises \`a l'ex\'ecution
par ses variables, est un probl\`eme ind\'ecidable dans le cas
g\'en\'eral, mais n\'eanmoins essentiel \`a r\'esoudre en pratique
(donc de mani\`ere approch\'ee) dans une optique d'optimisation et de
validation dudit programme.

En ce qui concerne les valeurs num\'eriques, il existe deux grandes
familles d'analyses permettant de les caract\'eriser, l'une faisant
intervenir des relations d'in\'egalit\'e (analyses d\'evelopp\'ees par
P. et R. Cousot et N. Halbwachs), l'autre des propri\'et\'es de
congruence identifiant la r\'egularit\'e de ces valeurs (analyses qui
font l'objet de cet expos\'e).

On concluera bri\`evement par des applications pratiques, concernant
tant les variables num\'eriques elles-m\^emes : vectorisation et
parall\'elisation automatique, tests de d\'ebordement des indices de
tableaux (cf. le s\'eminaire d'A. Deutsch du 16 d\'ecembre 1994) que
des propri\'et\'es non-num\'eriques ramen\'ees \`a un probl\`eme
num\'erique (analyses d'alias, de communications entre canaux).

*** Vendredi 9 decembre 1994 ****************************************

Rela^che (LOMAPS).

*** Vendredi 16 decembre 1994 ***************************************

Optimising Array Bound Checking in Time-Critical System Code

Alain DEUTSCH (INRIA)

Re'sume' : We present a general method  for statically optimising 
array bound checks.  The method is based on forward and  backward
abstract interpretation over relational lattices and performs two
optimisations:  first,  the  removal  of provably redundant array
bound  checks;  second the  code  motion of the remaining checks.
Application of the method to  the  optimisation  of time-critical
networking code will be discussed.

This is joint work with Peter Lee (Carnegie Mellon University).

*********************************************************************