@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." }