DiVinE Cluster
Description
DiVinE Cluster is a parallel, distributedmemory enumerative LTL modelchecking tool for verification of concurrent systems. The tool can employ aggregate power of networkinterconnected workstations or clusters to verify systems whose verification is beyond capabilities of sequential tools. As a standard modelchecker, DiVinE Cluster can be used to prove correctness of verification models as well as to detect early design errors.
DiVinE Cluster accepts models written in DiVinE native modeling language  DVE, and verifies them against specification formalized in Linear Temporal Logic. Moreover, DiVinE Cluster provides means for the detection of unreachable code, assertion violation, or deadlock.
DiVinE Cluster has also limited support for ProMeLa, that is the modeling language of the verification tool SPIN. This capability makes DiVinE Tool an ideal alternative to SPIN's users whose models cannot be directly verified with SPIN because of insufficient memory resources of a single computer. The restrictions for using DiVinE Cluster with ProMeLa models are incapability of generating counterexamples, performing Partial Order Reduction, verifying unreachable code and assertion violation.
Algorithms
DiVinE comes up with new algorithms for parallel accepting cycle detection problem which work on the graph that is partitioned into disjoint parts. Currently, DiVinE implements the following LTL parallel algorithms (for detailed references see Publications):

Algorithm based on dependency structure.
[Barnat and L. Brim and J. Stribrna: Distributed LTL ModelChecking in SPIN. Proc. SPIN Workshop on Model Checking of Software, Springer, 2001, volume 2057 of LNCS, 200  216.]
The algorithm performs partitioned depthfirst search of the state space and is augmented with an additional data structure that keeps the global DFS postorder.

Algorithm based on negative cycles
The LTL model checking problem is reduced to the negative cycle problem. The idea is to introduce an additional edge labeling function that assigns value 1 to edges outgoing from accepting states and value 0 to all other edges. In this way, accepting cycles coincide with negative cycles. A single source shortest path algorithm is than engaged to identify negative cycles.

Property Driven Nested DFS
The algorithm effectively uses the decomposition of the formula automaton into strongly connected components to achieve more efficient parallelization of nested depthfirst search procedure.

SCCbased algorithm (OWCTY)
The algorithm manipulates strongly connected components. A SCC decomposition is replaced by an iterative process in which nonperspective components (i.e., those which do not contain any accepting cycle) are removed from the state space.

Algorithm based on backlevel edges
A completely different algorithmic solution based on breadthfirst search (BFS) is presented in [ barnat03parallel, bc04fmics]. It is based on a backlevel edge concept. Backlevel edge is any edge which does not increase the breadthfirst search distance from the initial state. BFS is used to identify all backlevel edges. As every cycle contains at least onebacklevel edge, these can be used as triggers for detecting cycles.

Algorithm based on maximal accepting predecessors (MAP)
The algorithm introduces an ordering on accepting states and relies on fact that there is a maximal accepting state on each accepting cycle. The algorithm computes and propagates the value of maximal accepting predecessor. Once an accepting state is propagated to itself, an accepting cycle is revealed. Otherwise the set of accepting states is modified and a new iteration is started.
Download
The latest release of DiVinE Cluster and install instructions can be found here.