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

• Model checker
• Explicit-state model checker
• Multithreaded programs
• LLVM

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)