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. s. 208-213. ISBN 978-3-319-32581-1. doi:10.1007/978-3-319-32582-8_14. 2016.
Další formáty:   BibTeX LaTeX RIS
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
Originální 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 0302-9743
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ěnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 27. 4. 2017 06:45.
Anotace
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 VaVNá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 MUNá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
VytisknoutZobrazeno: 28. 3. 2024 16:39