A Generic Framework for Interprocedural Analysis of Numerical Properties

Abstract. In his seminal paper [5], 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.

• Type: Conference
• Year: 2005
• Where: SAS
• Authors: Markus Müller-Olm, Helmut Seidl
• Keywords: Analysis, Formal Methods, Infers, Linear Congruence Relations, SAS 2005