DIVINE.md

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

Name:

DIVINE

Application domain/field:

Model checker Explicit-state model checker Multithreaded programs LLVM

Type of tool (e.g. model checker, test generator):

Model checker

Expected input thing:

C program with assertions

Expected input 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 (tools used, frameworks, techniques, paradigms, ...):

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)

URIs (github, websites, etc.):

Project page: https://divine.fi.muni.cz/index.html Repository: https://github.com/paradise-fi/divine (mirror)

Last commit date:

21 Mar 2021 (default branch) 21 Mar 2021 (last activity)

Last publication date:

04 April 2019

List of related papers:

Extending DIVINE with Symbolic Verification Using SMT (TACAS '19) Model Checking of C and C++ with DIVINE 4 (ATVA '17) DIVINE: Explicit-State LTL Model Checker (TACAS '16)

Related tools (tools mentioned or compared to in the paper):

Tool that is now integrated in DIVINE: SymDIVINE

Meta

:: C :: C++ :: PV3 :: checks user-specified assertions in a C/C++ program :: Simulation :: Source :: https://doi.org/10.1145/3550355.3552426