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

Automated Release Process

(2014-11-30) A new automated release process has been rolled out for DIVINE, based on results from our Continuous Integration system. The latest available release is always available from the download page as a source tarball. Automatically built binaries for major operating systems will be made available in the future as well. The release notes document lists important user-visible changes between releases.

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"
}