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](manual.html)**. Our plans for upcoming releases are
outlined in the [roadmap] [rmap].

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]
[rmap].

The latest source tarball for DIVINE 4 is, as always, [available for download]
[dl]. 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.

[rmap]: roadmap.html
[dl]: download.html

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):

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