Abstractions for Data Structures: Abstraction of data structures such as Java classes can be achieved by component-wise abstraction of each field in a class. This approach is taken by Bandera (Dwyer et al. 2000). Array abstractions can be defined in a similar way: the user needs to define an integer abstraction for the array index and a data structure abstraction for the component type. Manually created abstractions with this structure have been used for the verification of wireless protocols.