PV3 ⊧ SymDIVINEchecks an LTL property or an assertion about the code

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

Application domain/field

• Model checking
• Concurrent programs
• Software model checking

Type of tool

Model checker

Expected input

• Program
• Optional: Assertions in program
• Optional: LTL property

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.