PV3 SymDIVINEchecks an LTL property or an assertion about the code

SymDIVINE, a model-checker for concurrent C/C++ programs

Application domain/field

Type of tool

Model checker

Expected input


.ll file (for assert reachability verification of LLVM bitcode) or C/C++ program.

Expected output

TIMEOUT, true or false indicating whether it could prove the assertion/LTL property.


Uses Z3


The repo is archived and no longer maintained. It is now integrated into DIVINE.
C Concurrency C++ LTL Model checking


Repository: https://github.com/paradise-fi/SymDIVINE

Related papers

Last publication date

31 March 2017

ProVerB specific

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