An Enhanced Equivalence Checking Method to Handle Bugs in Programs with Recurrences

Software designers often apply automatic or manual transformations on the array-handling source programs to improve performance of the target programs. Verdoolaege et al. (Verdoolaege et al., 2012) have proposed a method to automatically prove equivalence of the output arrays of the source and the generated transformed programs. Unlike the other approaches, the method of (Verdoolaege et al., 2012) provides the most sophisticated techniques to validate programs with non-uniform recurrences besides programs with uniform recurrences. However, if the recurrence expressions of the source and the transformed programs refer to more than one base cases of which some are non-equivalent and also if the domain of the output arrays partition based on dependences on different base cases, then some imprecision in the equivalence checking results is observed. The equivalence checker reports that the entire index spaces of the output arrays of the source program to be non-equivalent with that of the transformed program instead of the portion of the output arrays which depend on the non-equivalent base cases of the programs. In the current work, we have enhanced the method of equivalence checking of (Verdoolaege et al., 2012) so that it can precisely indicate the equivalent and non-equivalent portions of the output arrays.