MRÁZEK, Jan, Petr BAUCH, Henrich LAUKO and Jiří BARNAT. SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration. In Dragan Bošnački and Anton Wijs. Model Checking Software. Neuveden: Springer International Publishing, 2016. p. 208-213. ISBN 978-3-319-32581-1. doi:10.1007/978-3-319-32582-8_14.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration
Authors MRÁZEK, Jan (203 Czech Republic, belonging to the institution), Petr BAUCH (203 Czech Republic, belonging to the institution), Henrich LAUKO (703 Slovakia, belonging to the institution) and Jiří BARNAT (203 Czech Republic, guarantor, belonging to the institution).
Edition Neuveden, Model Checking Software, p. 208-213, 6 pp. 2016.
Publisher Springer International Publishing
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Switzerland
Confidentiality degree is not subject to a state or trade secret
Publication form printed version "print"
Impact factor Impact factor: 0.402 in 2005
RIV identification code RIV/00216224:14330/16:00088095
Organization unit Faculty of Informatics
ISBN 978-3-319-32581-1
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-319-32582-8_14
Keywords in English Model checking; C++; Symbolic approach
Tags firank_B
Tags International impact, Reviewed
Changed by Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 27. 4. 2017 06:45.
Abstract
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.
Links
GA15-08772S, research and development projectName: Analýza korektnosti vícevláknových programů v C a C++
Investor: Czech Science Foundation
MUNI/A/0945/2015, interní kód MUName: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V.
Investor: Masaryk University, Category A
PrintDisplayed: 25. 5. 2022 15:21