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 a Jiří BARNAT

Základní údaje

Originální název

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

Autoři

MRÁZEK, Jan (203 Česká republika, domácí), Petr BAUCH (203 Česká republika, domácí), Henrich LAUKO (703 Slovensko, domácí) a Jiří BARNAT (203 Česká republika, garant, domácí)

Vydání

Neuveden, Model Checking Software, od s. 208-213, 6 s. 2016

Nakladatel

Springer International Publishing

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Švýcarsko

Utajení

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

Forma vydání

tištěná verze "print"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/16:00088095

Organizační jednotka

Fakulta informatiky

ISBN

978-3-319-32581-1

ISSN

DOI

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

Klíčová slova anglicky

Model checking; C++; Symbolic approach

Štítky

firank_B

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 27. 4. 2017 06:45, RNDr. Pavel Šmerk, Ph.D.

Anotace

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.

Návaznosti

GA15-08772S, projekt VaV

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

Investor: Grantová agentura ČR, Correctness Analysis of C and C++ Programs with Threads

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

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

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace V., DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

Citovat

MRÁZEK, Jan, Petr BAUCH, Henrich LAUKO a 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, s. 208-213. ISBN 978-3-319-32581-1. Dostupné z: 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 a 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, s.~208-213. ISBN~978-3-319-32581-1. Dostupné z: https://dx.doi.org/10.1007/978-3-319-32582-8\_{}14.

Podrobný výpis o publikaci