@InProceedings{MartinHuddart00,
  title =        "{P}arallel {A}lgorithms for {D}eadlock and {L}ivelock {A}nalysis of {C}oncurrent {S}ystems",
  author=        "Martin,  Jeremy M. R. and Huddart,  Yvonne",
  editor=        "Welch, Peter H. and Bakkers,  Andr\`{e} W. P.",
  pages =        "1--14",
  booktitle=     "{C}ommunicating {P}rocess {A}rchitectures 2000",
  isbn=          "1 58603 077 9",
  year=          "2000",
  month=         "sep",
  abstract=      "Conventional model-checking techniques for analysing
     concurrent systems for deadlock or livelock are hampered by
     the problem of exponential state explosion: the overall
     number of global states that needs to be checked may grow
     exponentially with the number of component processes in the
     system. The state-of-the-art commercial tool FDR provides
     deadlock and livelock analysis but it is limited at present
     to analysing systems of up to one hundred million global
     states. The Deadlock Checker tool is capable of analysing
     very much larger systems by taking certain short-cuts. But
     this is achieved at the cost of incompleteness -- there are
     certain deadlock-free and livelock-free networks that may
     not be proven so using that tool. Here we investigate a
     different approach. We present parallelised model-checking
     algorithms for deadlock and livelock analysis and describe
     their implementation. The techniques are found to scale well
     running either on a conventional supercomputer or on a PC
     cluster."
}