*********************************************************************
*                       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 1 fe'vrier 2001 **** 14h00 *****************************

rela^che

*** Vendredi 8 fe'vrier 2001 **** 14h00 *****************************

Bertrand JEANNET (Projet VERTECS, IRISA-INRIA, Rennes)

Partitionnement dynamique et calcul approché de fonctions de
transfert en interpretation abstraite

Re'sume' :
Ce travail a été initialement motivé par la vérification de propriétés
de sûreté de programmes synchrones manipulant à la fois des variables
Booléennes et numériques.

Une technique classique d'analyse de tels systèmes consiste à associer
à chaque valuation Booléenne un invariant pour les variables
numériques, cet invariant étant obtenu par interprétation abstraite du
domaine numérique (intervalles [Cousot76], zones ou octogones
[Miné00], polyèdres convexes [Cousot&Halbwachs78], ...).

Cette manière de combiner variables booléennes et numériques ne passe
cependant pas à l'échelle, car le nombre de valuations booléennes
croît exponentiellement avec le nombre de variable booléennes.

Dans ce contexte, nous avons généralisé la notion de partitionnement
en interprétation abstraite, et montré comment on peut l'utiliser pour
ajuster le compromis entre précision élevée et coût modéré.  Cette
méthode représente aussi une solution générale pour combiner
efficacement différent types de données en interprétation abstraite
(booléens, réels, files d'attente, ...).

Deux problèmes restent cependant à résoudre:
- il faut pouvoir calculer efficacement les fonctions de transfert
  (post- et pré-conditions), sachant que leur meilleure approximation
  correcte est généralement bien trop coûteuse.
- il faut pouvoir raffiner (automatiquement) le partitionnement 
  lorsque celui-ci engendre trop d'approximations pour autoriser la
  preuve de la propriété.
  
Nous présenterons ces différents aspects, et illustrerons
l'efficacité pratiques de nos solutions sur des études de cas.

Travail commun avec Nicolas Halbwachs et Pascal Raymond (Vérimag,
Grenoble, France)

---

Dynamic partitioning and approximate computation of transfert
functions in abstract interpretation

Abstract :
This work was initially motivated by the verification of safety
properties of synchronous programs that exhibit both Boolean and
numerical aspects.

A classical technique for the analysis of such systems consists in
associating to each Boolean valuation an invariant for the numerical
variables, this invariant being obtained by abstract interpretation of
the numerical domain (intervals [Cousot76], zones or octagons
[Miné00], convex polyhedra [Cousot&Halbwachs78],...).

However, this way of combining Boolean and numerical variables doesn't
scale up, because the number of Boolean valuations is exponential in
the number of Boolean variables.

In this context, we have generalized the notion of partitioning in
abstract interpretation and showed how one can use it to adjust the
tradeoff between high precision and low complexity. This method can
also be viewed as a general solution to efficiently combine different
datatypes in abstract interpretation (Booleans, reals, FIFO queues,
...).

Two problems however have still to be solved: 
- one need to compute efficiently the transfert functions (post- and
  pre- conditions), knowing that their best correct approximations is
  generally too expensive.
- one need to (automatically) refine the partitioning when it
  generates too much approximations to enable the proof of the property.
  
We will present these different aspects, and show on case studies
their practical efficiency.

Joint work with Nicolas Halbwachs and Pascal Raymond (Vérimag,
Grenoble, France)

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