********************************************************************* * 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 *********************************************************************