Equivalence Checking of Array-Intensive Programs
Chandan Karfa, Kunal Banerjee, Debjit Sarkar, Chittaranjan Mandal · 2011
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.