DIVINE is a modern explicit-state model checker. Building on high­-per­for­mance algorithms and data structures, it offers unparalleled versatility, sca­ling from a typical developer’s laptop, up to a high-end compute cluster. What more, it can verify a wide range of languages, including C and C++. Learn more in the manual, or try it out.

Feature Highlights

DIVINE 3.0 has been released

(2013-07-13) The final version of DIVINE 3.0 has been released today. Get the source code or pre-built binaries! The changelog is here: what’s new. The major highlights of the 3.0 release are:

DIVINE 3.1 beta 1 has been released

(2014-01-06) We are pleased to announce the first beta release in preparation of version 3.1 of DIVINE. Please download the source code (or visit our hydra to obtain recent binary snapshots) and help us by testing this pre-release.

The major improvements making a debut in version 3.1 are more sophisticated shared-memory verification, lossless tree-based state space compression, improved performance and substantially improved memory efficiency. The series also includes improved support for compilation of C++ into LLVM bitcode (now including the standard library out of the box) and improvements to the DVE specification language. The LLVM backend has gained a number of improvements, including more sophisticated error detection and reporting.

Additionally, a number of improvements and bug fixes has been added since the last alpha release in autumn. Please consult the changelog.

Contacting Us

If you have comments or questions about DIVINE, please email divine at fi.muni.cz. To file a bug report or an enhancement request, please use our trac.

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{BBH+13,
  author    = "Jiří Barnat and Luboš Brim and Vojtěch Havel
               and Jan Havlíček and Jan Kriho and Milan Lenčo
               and Petr Ročkai and Vladimír Štill and Jiří Weiser",
  title     = "{DiVinE 3.0 -- An Explicit-State Model Checker
                for Multithreaded C \& C++ Programs}",
  booktitle = "{Computer Aided Verification (CAV 2013)}",
  pages     = "863--868",
  volume    = "8044",
  series    = "LNCS",
  year      = "2013",
  publisher = "Springer"
}