Model Checking Data-Independent Systems With Arrays

We say a program is data-independent with respect to a data type X if the operations it can perform on values of type X are restricted to just equality testing, although the system may also input, store and move around values of type X within its variables. This property can be exploited to give procedures for the automatic veri cation, called model checking, of such programs independently of the instance for the type X