Experience with widening based equivalence checking in realistic multimedia systems

Designers often apply manual or semi-automatic loop and data transformations on array and loop intensive programs to improve performance. For the class of static affine programs, automatic methods exist for proving the correctness of these transformations. Realistic multimedia systems, however, often contain constructs that fall outside of this class. We present an extension of a widening based approach to handle the most relevant of these constructs, viz. accesses to array slices and data dependent accesses, and report on some experiments with non-trivial applications.