Markus Mueller-Olm (Fernuniversitaet Hagen)

Precise Program Analysis with (Linear) Algebra
        
We combine techniques from algebra and linear algebra with abstract
interpretation 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 field,
e.g., the rationals.  Our analyses precisely interpret assignment
statements with affine or polynomial right hand side (affine
vs. polynomial programs) and treat other assignment statements
conservatively.  Our analyses for polynomial programs also interpret
polynomial disequality guards precisely.  Besides of this, branching
is assumed to be non-deterministic.

More specifically, we have constructed

 - an interprocedural analysis for affine programs that determines for
   every program point all valid affine relations;

 - generalizations of this analysis to polynomial relations of bounded
   degree and to affine programs with local variables and procedures
   with parameters and results;

 - a generalization that takes affine preconditions into account; and

 - an intraprocedural analysis for polynomial programs that computes
   all valid polynomial relations of a given format.
        
The running time of analysis 1,2, and 3 is linear in the size of the
program and polynomial in the number of program variables.  For
analysis 4 we have a termination guarantee but do not know an upper
complexity bound.  These analyses have many potential applications,
because many analysis questions can be coded as affine or polynomial
relations.

(This is joint work with Helmut Seidl.)