@inproceedings{Whole-Array,
  title = "On Model checking data-independent systems with arrays with whole-array operations",
  author = "A. W. Roscoe and R. S. Lazic and Tom Newcomb",
  year = "2005",
  booktitle = "{Communicating Sequential Processes}",
  number = "3525",
  publisher = "Springer {LNCS}",
  url = "http://web.comlab.ox.ac.uk/oucl/work/bill.roscoe/publications/102.pdf",
}