*********************************************************************
* 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 30 mai 2003 **** 14h00 *********************************
Markus M"uller-Olm (FernUniversit"at Hagen)
(Linear) Algebra for Program Analysis
Re'sume': I am going to talk on onging research in which we use
techniques from algebra and linear algebra to construct highly precise
analysis routines for imperative programs or program fragments. We
are interested in programs that work on variables taking values in
some fixed ring or field, e.g., the integers or the rationals. Our
analyses precisely interpret assignment statements with affine or
polynomial right hand side and treat other assignment statements as
well as guarded branching statements conservatively as
non-deterministic statements.
More specifically, we have constructed
- an interprocedural analysis that determines for every program point
of an affine program all valid affine relations;
- a generalization of this analysis to polynomial relations of
bounded degree and to affine programs with local variables; and
- an intraprocedural analysis that decides validity of polynomial
relations in polynomial programs.
The running time of analysis 1 and 2 is linear in the size of the
program and polynomial in the number of program variables. For
analysis 3 we have a termination guarantee but do not know an upper
complexity bound. These analyses have many potential applications,
because analysis questions can often be coded as affine or polynomial
relations easily.
(This is joint work with Helmut Seidl.)
*********************************************************************
Pour recevoir l'annonce par courrier electronique: cousot@di.ens.fr
WWW: http://www.di.ens.fr/~cousot/annonceseminaire.shtml
*********************************************************************