Model Checking of C and C++ with DIVINE 4

Authors: Zuzana Baranová, Jiří Barnat, Katarína Kejstová, Tadeáš Kučera, Henrich Lauko, Jan Mrázek, Petr Ročkai, Vladimír Štill

The fourth version of the DIVINE model checker provides a modular platform for verification of real-world programs. It is built on an efficient interpreter of LLVM code which, together with a small, verification-oriented operating system and a set of runtime libraries, enables verification of code written in C and C++.



DIVINE can be downloaded from the links below. These links reflect the state of DIVINE at the time of the finalization of this paper.


Apart from the short guide included in the paper, there is a longer and more elaborate guide in the manual.

Example Programs

Here you can find some commented example programs which demonstrate features of DIVINE. Below, you will find pointers to additional, more complex examples.

Simple Memory Access Error


$ divine verify memory.c

This code demonstrates DIVINE’s ability to uncover an invalid access to a stack variable (array x). It also shows that traces produced by DIVINE contain strings that the program wrote to the standard output and the error output.

Constant Memory Write Error


$ divine verify constants.c

In this code, we can see that DIVINE can detect attempts to write into constant memory.

Simple C++ Threading


$ divine verify -std=c++11 -o nofail:malloc thread.cpp

This program demonstrates that C++11 threads are supported in DIVINE. There is a data race between the two increment operations on x. Please note that -o nofail:malloc is used to suppress fault injection in memory allocation (std::thread allocates memory for passing arguments to the created thread; it would be also possible to solve this problem in the program by catching an exception of type std::bad_alloc).

Uninitialised Value Detection


$ divine verify undef.c

In this program, DIVINE detects use of an uninitialised value in a conditional statement. Here, the error is caused by a data race that results in a read of an uninitialised value (x) at line 7.

pthreads Deadlock Detection


$ divine verify deadlock.c

This is an example of a program which contains a deadlock caused by improper use of pthread mutexes.

Further Examples

Some further examples can be found in DIVINE’s testsuite (in the test directory in DIVINE sources). For example test/cpp/2.fifo-bug.cpp is a unit test of a parallel reader-writer queue which was used in DIVINE 3 and in which DIVINE discovered an error (fixed version is in test/cpp/2.fifo.cpp).

Another nice example is a unit test of the parallel hash table used in DIVINE: In this case, the program also contains headers and can use preprocessor macros for configuration. Therefore, it is better to use DIVINE’s compiler (divine cc) to compile the program to LLVM IR first. It can be compiled and verified using the following commands (in the directory with the test):

(Memory allocation failure simulation is disabled as the hashset is not supposed to be resilient to memory exhaustion).

  1. Windows Subsystem for Linux (WSL, also known as Bash on Windows) allows you to run Linux binaries on Windows 10, please refer to for installation instructions. Once you have WSL installed, it should be sufficient to run bash, download DIVINE binary using wget && chmod +x divine and then run ./divine.