DIVINE is a modern, explicit-state model checker. Based on the LLVM toolchain, it can verify programs written in multiple real-world programming languages, including C and C++. The verification core is built on a foundation of high­-per­for­mance algorithms and data structures, scaling all the way from a laptop to a high-end cluster. Learn more in the manual. Our plans for upcoming releases are outlined in the roadmap.

DIVINE 4 Now Available

[2017-01-08] We are pleased to announce that, after a few last-minute holdups, we are ready to label DIVINE 4 as stable. Please bear in mind, however, that DIVINE is still an academic tool and unfortunately only saw limited testing in the beta period. That said, our experience says that it’s already pretty useful in practice and we have some nice improvements planned for future releases.

The latest source tarball for DIVINE 4 is, as always, available for download. Starting on January 15th, there will be semi-automated, fortnightly point releases in the 4.0 series (which will include new features as they stabilise), and a 4.1 milestone in July this year.

DIVINE 4 Coming This Autumn

[2016-09-23] A major update of our software model checker is scheduled for release in autumn 2016. The new release will bring a new, flexible execution environment, based on the traditional virtual machine – operating system – user pro­gram division, along with a more efficient multi-threaded verification core. The user interface has also seen major improvements. Finally, the upcoming version of DIVINE will make working with counterexamples a much smoother and more pleasant experience.

Contacting Us

If you have comments or questions about DIVINE, please send an email to divine at fi.muni.cz.

Use in Publications

When you refer to DIVINE in an academic paper, we would appreciate if you could use the following reference (our currently most up-to-date tool paper):

  author = {Zuzana Baranová and Jiří Barnat and Katarína Kejstová
            and Tadeáš Kučera and Henrich Lauko and Jan Mrázek
            and Petr Ročkai and Vladimír Štill},
  title = {Model Checking of {C} and {C}++ with {DIVINE} 4},
  booktitle = {Automated Technology for Verification and Analysis (ATVA 2017)},
  pages     = {201-207},
  volume = {10482},
  series = {LNCS},
  year = {2017},
  publisher = {Springer}}