A Distributed Partial Order Reduction Algorithm

  • Robert Palmer
  • Ganesh Gopalakrishnan
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2529)


A distributed version of the PV model checker [5] is being developed at the University of Utah [7]. Other distributed model checkers have also been implemented [1], [2], [6], however these have limited, or do not use partial order reduction.


  1. 1.
    Jiri Barnat, Lubos Brim, and Jitka Stribrna. Distributed ltl model-checking in spin. In Proceedings of the 7th International SPIN Workshop, pages 200–216, 2001. LNCS 2057.Google Scholar
  2. 2.
    Hubert Garavel, Radu Mateescu, and Irina Smarandache. Parallel state space construction for model-checking. In Proceedings of the 7th International SPINWorkshop, pages 217–234, 2001. LNCS 2057.Google Scholar
  3. 3.
    Richard J. Lipton. Reduction:A method of proving properties of parallel programs. Communications of the ACM, 18(12), December 1975.Google Scholar
  4. 4.
    Ratan Nalumasu and Ganesh Gopalakrishnan. An efficent partial order reduction algorithm with an alternative proviso implementation. Formal Methods in System Design, 20(3):231–247, May 2002.zbMATHCrossRefGoogle Scholar
  5. 5.
    Robert Palmer and Ganesh Gopalakrishnan. Partial order reduction assisted parallel modelchecking (full version). Technical report, University of Utah, August 2002.Google Scholar
  6. 6.
    Ulrich Stern and David Dill. Parallelizing the Murö verifier. Formal Methods in System Design, 18(2):117–129, 2001. (Journal version of their CAV 1997 paper).zbMATHCrossRefGoogle Scholar
  7. 7.
    The Utah Verifier group website. verification.

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Robert Palmer
    • 1
  • Ganesh Gopalakrishnan
    • 1
  1. 1.School of ComputingUniversity of UtahUSA

Personalised recommendations