SymDIVINE is a tool for control explicit/data symbolic bit-precise LTL verification of parallel C/C++ programs using LLVM bitcode as intermediate representation.
How to run it
You can build SymDIVINE yourself (see section Building), or you can obtain pre-built binary for x64 Linux from here.
Runtime dependencies of SymDIVINE are:
z3. To compile
C/C++ programs to LLVM you need
clang-3.5. If you want to use LTL model
ltl2tgba is required.
If your system doesn't have package for Z3 SMT solver or you want to use the newest version (strongly recommended), you can download it or get sources and compile it from their official repository.
For simple assert reachability verification of LLVM bitcode run
bin/symdivine reachability <model.ll> or see
bin/symdivne help for more info. SymDIVINE
supports pthreads, pthread mutexes, atomic sections via SV-COMP notation and
You can also use helper script
scripts/run_symdivine.py, which takes a C a C++
file, compiles it and runs SymDIVINE.
To build SymDIVINE, yout need
Then just checkout this repo and run
./configure && cd build && make. Final
If you run to problems with
git submodule update --init --recursive.
About the authors
Based on work by Vojtěch Havel and Peter Bauch in ParaDiSe (Parallel & Distributed System Laboratory). Currently developed by Jan Mrázek, Henrich Lauko and Martin Jonáš.