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

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F16%3A00088095" target="_blank" >RIV/00216224:14330/16:00088095 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1007/978-3-319-32582-8_14" target="_blank" >http://dx.doi.org/10.1007/978-3-319-32582-8_14</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-319-32582-8_14" target="_blank" >10.1007/978-3-319-32582-8_14</a>

Result language
angličtina
Original language name
SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration
Original language 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.
Czech name
—
Czech description
—

Project
<a href="/en/project/GA15-08772S" target="_blank" >GA15-08772S: Correctness Analysis of C and C++ Programs with Threads</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year
2016
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Similar results(10)