The PV tool is based on a new partial order reduction algorithm called Two-phase that generates a significantly reduced state space on a large class of practical protocols over alternative algorithms in its class. The Two-phase algorithm preserves all CTL*-X assertions (next-time free CTL*). The implementation of the PV tool that embodies Two-phase follows the nested DFS on-the-fly model-checking procedure due to Courcoubetis, Vardi, Wolper, and Yannakakis; the PV tool preserves LTL-X (next-time free LTL). Two-phase follows an alternative implementation of the proviso step. In particular, Two-phase avoids the in-stack check that other tools use in order to realize the proviso step. We have found the in-stack check based implementation of the Proviso to be the source of state explosion in many examples. For details on the Two-phase algorithm, kindly see the forthcoming FMSD paper by Nalumasu and Gopalakrishnan, or see our papers cited.

Two-phase incorporates selective state caching. Selective caching refers to the class of techniques where instead of saving every state visited in the reduced state space, only a subset of states are saved. There is a very natural way to incorporate selective caching into Two-phase because it guarantees that a given state always generates the same subgraph beneath it whether it is expanded as part of outer dfs or inner dfs of the Courcoubetis et.al. algorithm - an important correctness requirement. The "save back edges" flag of the PV tool supports selective state caching by saving states only when backward transitions (back edges) are taken during Phase-1.

PV also detects and attempts to reset dead-variables automatically, avoiding another manual chore required in other tools.

PV has helped us complete full state-space search several orders of magnitude faster than all alternative tools available in its class on several real protocols, including on protocols that came with the distribution of these tools. PV has helped us detect bugs in Distributed Shared Memory cache coherency protocols used in the Utah Avalanche Shared Memory Multiprocessor project that were missed during incomplete search using alternate tools. PV also finishes (and often faster) in all our experiments on Test Model-Checking to date.

References:

Univ of Utah, Dept of CS Tech Report, UUCS-96-006, Ratan Nalumasu and Ganesh Gopalakrishnan, "Partial Order Reduction Without the Proviso." This TR first introduces Two-phase and PV.

UUCS-98-017, Ratan Nalumasu and Ganesh Gopalakrishnan, "A Partial Order Reduction Algorithm without the Proviso." A later TR with more details.

Ratan Nalumasu and Ganesh Gopalakrishnan, "A New Partial Order Reduction Algorithm for Concurrent System Verification," Proceedings of the 1997 Computer Hardware Description Languages, Toledo, Spain, April 1997, pp. 305-314.

Ratan Nalumasu and Ganesh Gopalakrishnan, ``PV: A Model-checker for Verifying LTL-X Properties,'' Lfm97: Fourth NASA LaRC Formal Methods Workshop, 10-12 September 1997, Hampton, Virginia.

Ratan Nalumasu and Ganesh Gopalakrishnan, "PV: an Explicit Enumeration Model-checker," Formal Methods in Computer Aided Design, Second International Conference, FMCAD'98, Palo Alto, CA, USA, Nov 1998, Proceedings. Ganesh Gopalakrishnan and Phillip Windley (editors). Springer-Verlag LNCS 1522. pp. 523-528.

Ratan Nalumasu and Ganesh Gopalakrishnan, "An Efficient Partial Order Reduction Algorithm with an Alternative Proviso Implementation," Formal Methods in System Design} (Kluwer), To appear.