Markus Müller-Olm and Helmut Seidl. A Generic Framework for Interprocedural Analysis of Numerical Properties. In Chris Hankin and Igor Siveroni, editors, Static Analysis, volume 3672 of Lecture Notes in Computer Science, pages 235-250, London, UK, September 2005. Springer.

In his seminal paper , Granger presents an analysis which infers linear congruence relations between integer variables. For affine programs without guards, his analysis is complete, i.e., infers all such congruences. No upper complexity bound, though, has been found for Granger’s algorithm. Here, we present a variation of this analysis which runs in polynomial time. Moreover, we provide an interprocedural extension of this algorithm. These algorithms are obtained by means of multiple instances of a general framework for constructing interprocedural analyses of numerical properties. Finally, we indicate how the analyses can be enhanced to deal with equality guards interprocedurally.

Download: PDF Reference: Bibtex The original publication is available at