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

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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ázev v anglickém jazyce

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

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/GA15-08772S" target="_blank" >GA15-08772S: Analýza korektnosti vícevláknových programů v C a C++</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2016

Kód důvěrnosti údajů

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

Název statě ve sborníku

Model Checking Software

ISBN

9783319325811

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

6

Strana od-do

208-213

Název nakladatele

Springer International Publishing

Místo vydání

Neuveden

Místo konání akce

Eindhoven, The Netherlands

Datum konání akce

1. 1. 2016

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—