Markus Müller-Olm and Helmut Seidl. Precise interprocedural analysis through linear algebra. In Neil D. Jones and Xavier Leroy, editors, Principles of Programming Languages, pages 330-341, Venice,Italy, January 2004. ACM.
We apply linear algebra techniques to precise interprocedural dataflow analysis. Specifically, we describe analyses that determine for each program point identities that are valid among the program variables whenever control reaches that program point. Our analyses fully interpret assignment statements with affine expressions on the right hand side while considering other assignments as non-deterministic and ignoring conditions at branches. Under this abstraction, the analysis computes the set of all affine relations and, more generally, all polynomial relations of bounded degree precisely. The running time of our algorithms is linear in the program size and polynomial in the number of occurring variables. We also show how to deal with affine preconditions and local variables and indicate how to handle parameters and return values of procedures.