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

Format:

.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.

Internals

Uses Z3

Comments

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

Links

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.