## Why DiVinE ?

The computing power of computers has increased by a factor of a million over the past couple of decades. As a matter of fact, the development effort, both in industry and in academia, has gone into developing bigger, more powerful and more complex applications. In the next few decades we may still expect a similar rate of growth, due to various factors such as continuing miniaturization, parallel and distributed computing.

With the increase in complexity of computer systems, it becomes even more important to develop formal methods for ensuring their quality and reliability. Various techniques for automated and semi-automated analysis and verification have been successfully applied to real-life computer systems. However, these techniques are computationally demanding and memory-intensive in general and their applicability to extremely large and complex systems routinely seen in practice these days is limited. The major hampering factor is the state space explosion problem due to which large industrial models cannot be efficiently handled unless we use more sophisticated and scalable methods and a balance of the usual trade-off between run-time, memory requirements, and precision of a method.

A lot of attention has been paid to the development of approaches to battle the
state space explosion problem. Many techniques, such as abstraction, state
compression, state space reduction, symbolic state representation, etc., are
used to reduce the size of the problem to be handled allowing thus a single
old-fashioned single-processor computer to process larger systems. All these
methods can be therefore characterized as *reduction* techniques.

Verification and analysis methods that are tailored to exploit the
capabilities of the new hardware architectures are slowly appearing as well.
These **platform-dependent** techniques focus on increasing the amount of
available computational power. These are, for example, techniques to fight
memory limits with efficient utilisation of external I/O devices, techniques
that introduce cluster-based algorithms to employ aggregate power of
network-interconnected computers, or techniques to speed-up the verification on
multi-core processors.

The idea of exploiting hard disks or parallel computers in verification already appeared in the very early years of the formal verification era. However, inaccessibility of cheap parallel computers with sufficiently fast external memory together with negative theoretical complexity results excluded these approaches from the main stream in formal verification. The situation changed dramatically during the past several years. The computer progress over the past two decades has measured several orders of magnitude with respect to various physical parameters such as computing power, memory size at all hierarchy levels from caches to disk, power consumption, physical size and cost. In particular, the focus of novel computer architectures in parallel and distributed computing has shifted away from unique massively parallel systems competing for world records towards smaller and more cost effective systems built from personal computer parts. In addition, recent shift in the emphasis of research on parallel algorithms to pragmatic issues has provided practically efficient algorithms for solving computationally hard problems. As a matter of fact, interest in platform-depended verification has been revived and DiVinE was born.

## About DiVinE

DiVinE is an open source and extensible system for platform-dependent
formal verification of computer systems. DiVinE is in fact a **set of tools**
each of them tailored to a particular platform, like distributed-memory (DiVinE Cluster), shared-memory (DiVinE Multi-Core), external hard disks
(DiVinE I-O) etc. DiVinE in its current development phase offers mainly tools
for platform-depended model checking of finite state systems against
specification formulated in linear temporal logics
(LTL). Special DiVinE **branches** focus on model-checking of
probabilistic systems (Markov decision
processes) - ProbDiVinE and on
analyzis of complex biological systems BioDiVinE (under development).

LTL model checking algorithms in DiVinE follow the *automata-based
approach*. Algorithms find accepting cycles in the product of the system model
and a Buchi automaton for the negation of the formula.

In most sequential LTL model checkers Nested Depth-First Search and Tarjan's
decomposition into strongly connected components are used for accepting cycle
detection. Unfortunately, both algorithms strongly rely on depth-first search
postorder which computation is known to be inherently sequential. Therefore,
these algorithms are unsuitable for being used in parallel setting.
DiVinE implements **new algorithms** for parallel accepting cycle detection problem.
These are briefly described on the respective tool pages.

## DiVinE Tools and Branches

DiVinE tools differ in the platforms they are supposed to be run on, while DiVinE branches are domain specific tools.

DiVinE BRANCHES | ||||
---|---|---|---|---|

DiVinE TOOLS | Concurrent Systems | Probabilistic Systems | Biological Systems | |

Clusters (distributed-memory) | DiVinE CLUSTERis a parallel
distributed-memory enumerative model-checking tool for verification of
concurrent systems. The tool can employ aggregate power of
network-interconnected workstations 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. |
ProbDiVinEis an enumerative model-checking tool for verification of probabilistic systems represented as Markov decision processes. The tool supports qualitative LTL model-checking of MDPs and is supposed to be run on clusters of workstations. |
BioDiVinE (under development)is a tool for exploring dicrete models of biological systems, predicting outcomes of experiments, and verifying specific properties at the model, based on techniques for scalable qualitative simulation and analyzis of integrated regulatory networks dymamics. | |

Multi-cores (shared-memory) | DiVinE
MULTI-COREis a parallel shared-memory enumerative model-checking tool for verification
of concurrent systems. The tool can employ full power of modern 64-bit multi-core
architectures. Similarly to DiVinE Cluster, it can be used to prove correctness
of verification models as well as to detect early design errors. |
ProbDiVinE
MC is an enumerative shared-memory model-checking tool for verification
of probabilistic systems represented as Markov decision processes. The tool
supports both qualitative as well as quantitative approaches to LTL
model-checking of MDPs. |
||

GPUs | DiVinE
CUDAis an open source standalone verification tool that supplements DiVinE verification tool chain with GPU accelerated LTL model checking of concurrent systems. DiVinE CUDA builds upon the MAP algorithm reformulated in terms of repeated matrix-vector product. The tool first generates state space of the model under inspection, stores it in the form of a matrix, and then it employs CUDA architecture to solve the accepting cycle detection problem on the graph represented with the matrix. |
|||

Hard Disks | DiVinE I-O (under development)is a distributed-memory enumerative model-checking tool for verification of concurrent systems on external memory devices. The tool implements I/O efficient LTL model-checking algorithms, where the goal is to reduce the number of expensive I/O. This is because the access to information stored on an external device is orders of magnitude slower than the access to information stored in main memory. It can be used both to prove correctness of verification models as well as to detect early design errors. |