Equivalence Checking of Array-Intensive Programs

An equivalence checking method for ensuring correctness of loop and arithmetic transformations in array intensive programs is presented here. The array data dependence graphs (ADDGs) are used to represent both the input and the transformed behaviours and the correctness of the transformations is ensured by proving equivalence of two ADDGs. In contrast to the existing path based one, we formalize a slice based equivalence of ADDGs. Moreover, normalization of arithmetic expressions and some simplification rules are incorporated to handle arithmetic transformations. Experimental results on several test cases demonstrate the effectiveness of our method.