PV3 ⊧ DIVINEchecks user-specified assertions in a C/C++ programDIVINE is an explicit-state LLVM-based model checker focusing on the analysis of real-world C and C++ programs
- Model checker
- Explicit-state model checker
- Multithreaded programs
Type of toolModel checker
Expected inputC program with assertions
Format:Single C/C++ file or a compiled program that is linked to DIVINE's runtime libraries.
Expected outputWhether 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).
InternalsUses 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