SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration

Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

MRÁZEK Jan BAUCH Petr LAUKO Henrich BARNAT Jiří

Year of publication 2016
Type Article in Proceedings
Conference Model Checking Software
MU Faculty or unit

Faculty of Informatics

Citation
Doi http://dx.doi.org/10.1007/978-3-319-32582-8_14
Field Informatics
Keywords Model checking; C++; Symbolic approach
Description We present SymDIVINE: a tool for bit-precise model checking of parallel C and C++ programs. It builds upon LLVM compiler infrastructure, hence, it uses LLVM IR as an input formalism. Internally, SymDIVINE extends the standard explicit-state state space exploration with SMT machinery to handle non-deterministic data values. As such, SymDIVINE is on a halfway between a symbolic executor and an explicit-state model checker. The key differentiating aspect present in SymDIVINE is the ability to decide about equality of two symbolically represented states preventing thus repeated exploration of the state space graph. This is crucially important in particular for verification of parallel programs where the state space graph is full of diamond-shaped subgraphs.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.