Computing Interprocedurally Valid Relations in Affine Programs

We consider an abstraction of programs which preserves affine assignments exactly while conservatively dealing with other assignments and ignoring conditions at branches. We present an interprocedural analysis of such abstracted programs which for every program point v determines the set of all affine relations between program variables which are valid when reaching v. The runtime of this algorithm is linear in the program size and polynomial in the number of occurring variables. We extend this result to a polynomial-time algorithm which determines for every program point the set of all valid polynomial relations between program variables of bounded degree