DIVINE is a tool for LTL model checking and reachability analysis of discrete distributed systems. The tool is able to efficiently exploit the aggregate computing power of multiple network-interconnected multi-cored workstations in order to deal with extremely large verification tasks. As such it allows to analyse systems whose size is far beyond the size of systems that can be handled with regular sequential tools.
New developments in DIVINE include:
- Execution on cluster of multi-core workstations
- On-the-fly verification
- Execution of models compiled to binary code
- Parallel partial order reduction
- Support for MS windows
- Graphical user interface
- Support for Murphi models
Use in Publications
When you refer to DiVinE in an academic paper, we would appreciate if you could use the following reference (the currently most up-to-date tool paper on DiVinE):
@InProceedings{BBCR10,
author = "J. Barnat and L. Brim and M. \v{C}e\v{s}ka and P. Ro\v{c}kai",
title = "{DiVinE: Parallel Distributed Model Checker (Tool paper)}",
booktitle = "Parallel and Distributed Methods in Verification and High
Performance Computational Systems Biology
(HiBi/PDMC 2010)",
pages = "4--7",
year = "2010",
publisher = "IEEE"}
Version 2.5 Now Available
(2011-12-04) UPDATE: Another minor revision to 2.5 has been released, with version number 2.5.2, fixing compatibility with more recent releases of GCC and CMake.
(2011-04-05) UPDATE: A minor revision to 2.5 has been released, with version number 2.5.1, and fixing a few important bugs in the DVE compiler. All users of the DVE compiler are strongly advised to update to this version.
(2011-03-01) The DIVINE team has released a new version of its parallel LTL model checking tool. This version brings further improvements in verification performance, as well as a few new major features:
-
A new command, “divine draw” has been added to the suite of support tools, enabling graphviz-based visualisation of model state spaces and counterexample traces. The graphviz package needs to be installed to make this functionality available. Please see divine draw –help for usage instructions.
-
A new input language, CoIN is now available for use with DiVinE.
Component-interaction automata language (CI Automata, or CoIn Automata for short) was designed for modelling of component interactions in hierarchical component-based software systems. The language supports modelling of important interaction attributes of such systems, and hence provides a rich base for further application of formal methods. Component-based systems, that are to be modelled, are usually connected to a particular component model. For this reason, Component-interaction automata are very general and support modelling of component interactions in component-based systems built on various component models.
-
Support for the Windows platform has been further improved, with “divine combine” now being available, completing the toolchain for model development and model checking.
Moreover, a number of bugfixes and minor improvements have been made in this release. You can download the new version here.