Skip to main content.

DiVinE Cluster

Description

DiVinE Cluster is a parallel, distributed-memory enumerative LTL model-checking tool for verification of concurrent systems. The tool can employ aggregate power of network-interconnected workstations or clusters to verify systems whose verification is beyond capabilities of sequential tools. As a standard model-checker, 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):

Download

The latest release of DiVinE Cluster and install instructions can be found here.