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 (via assignment) values of type X within its variables. This property can be expl...

Full description

Bibliographic Details
Main Author: Newcomb, Tom C.
Other Authors: Roscoe, A. W.
Published: University of Oxford 2003
Subjects:
Online Access:http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.400294