@InProceedings{BrookePaige07,
  title =        "{L}azy {E}xploration and {C}hecking of {CSP} {M}odels with {CSP}sim",
  author=        "Brooke,  Philip J and Paige,  Richard F.",
  editor=        "McEwan,  Alistair A. and Schneider,  Steve and Ifill,  Wilson and Welch, Peter H.",
  pages =        "33--50",
  booktitle=     "{C}ommunicating {P}rocess {A}rchitectures 2007",
  isbn=          "978-1-58603-767-3",
  year=          "2007",
  month=         "jul",
  abstract=      "We have recently constructed a model, and carried out an
     analysis, of
a concurrent extension to an object-oriented
     language at a level of abstraction above threads. The model
     was constructed in CSP. We subsequently found that existing
     CSP tools were unsuitable for reasoning about and analysing
     this model, so it became necessary to create a new tool to
     handle CSP models: CSPsim. We describe this tool, its
     capabilities and algorithms, and compare it with the related
     tools, FDR2 and ProBE. We illustrate CSPsim's usage with
     examples from the model. The tool's on-the-fly construction
     of successor states is important for exhaustive and
     non-exhaustive state exploration. Thus we found CSPsim to be
     particularly useful for parallel compositions of components
     with infinite states that reduce to finite-state systems."
}