PV3 DIVINEchecks user-specified assertions in a C/C++ program

DIVINE is an explicit-state LLVM-based model checker focusing on the analysis of real-world C and C++ programs

Application domain/field

Type of tool

Model checker

Expected input

C program with assertions

Format:

Single C/C++ file or a compiled program that is linked to DIVINE's runtime libraries.

Expected output

Whether it could verify the assertions in the program. If not then it will produce an error trace (output of the program until the point of the error).

Internals

Uses Z3. Aside from verifying the program, DIVINE also has some an option to visualize the state space and to simulate a program run interactively. Note: before verifying with DIVINE, you first need to compile the program (if it's not a single file) into LLVM bitcode and link it against DIVINE's runtime librraries. This can be done with divine cc program.c

Comments

License; ISC license (2-clause BSD)
C C++ Simulation

Links

Related papers

Last publication date

04 April 2019

Related tools

Tool that is now integrated in DIVINE: SymDIVINE

ProVerB specific



ProVerB is a part of SLEBoK. Last updated: February 2023.