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

D 2016

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

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

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

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Switzerland

Confidentiality degree

není předmětem státního či obchodního tajemství

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

DOI

http://dx.doi.org/10.1007/978-3-319-32582-8_14

Keywords in English

Model checking; C++; Symbolic approach

Abstract

V originále

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 project

Name: Analýza korektnosti vícevláknových programů v C a C++

Investor: Czech Science Foundation

MUNI/A/0945/2015, interní kód MU

Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V.

Investor: Masaryk University, Category A

Citovat

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. Available from: https://dx.doi.org/10.1007/978-3-319-32582-8_14.

@inproceedings{1352238,
   author = {Mrázek, Jan and Bauch, Petr and Lauko, Henrich and Barnat, Jiří},
   address = {Neuveden},
   booktitle = {Model Checking Software},
   doi = {http://dx.doi.org/10.1007/978-3-319-32582-8_14},
   editor = {Dragan Bošnački and Anton Wijs},
   keywords = {Model checking; C++; Symbolic approach},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Neuveden},
   isbn = {978-3-319-32581-1},
   pages = {208-213},
   publisher = {Springer International Publishing},
   title = {SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration},
   year = {2016}
}

TY  - JOUR
ID  - 1352238
AU  - Mrázek, Jan - Bauch, Petr - Lauko, Henrich - Barnat, Jiří
PY  - 2016
TI  - SymDIVINE: Tool for Control-Explicit Data-Symbolic State Space Exploration
PB  - Springer International Publishing
CY  - Neuveden
SN  - 9783319325811
KW  - Model checking
KW  - C++
KW  - Symbolic approach
N2  - 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.
ER  -

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. \textit{Model Checking Software}. Neuveden: Springer International Publishing, 2016, p.~208-213. ISBN~978-3-319-32581-1. Available from: https://dx.doi.org/10.1007/978-3-319-32582-8\_{}14.

Detailed Information on Publication Record