DiVinE 3.0 -- An Explicit-State Model Checker for Multithreaded C & C++ Programs
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F13%3A00066526" target="_blank" >RIV/00216224:14330/13:00066526 - isvavai.cz</a>
Výsledek na webu
<a href="http://dx.doi.org/10.1007/978-3-642-39799-8_60" target="_blank" >http://dx.doi.org/10.1007/978-3-642-39799-8_60</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-642-39799-8_60" target="_blank" >10.1007/978-3-642-39799-8_60</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
DiVinE 3.0 -- An Explicit-State Model Checker for Multithreaded C & C++ Programs
Popis výsledku v původním jazyce
We present a new release of the parallel and distributed LTL model checker DIVINE. The major improvements in this new release is an extension of the class of systems that may be verified with the model checker, while preserving the unique DIVINE feature,namely parallel and distributed-memory processing. Version 3.0 comes with support for direct model checking of (closed) multithreaded C/C++ programs, full untimed-LTL model checking of timed automata, and a general-purpose framework for interfacing witharbitrary system modelling tools.
Název v anglickém jazyce
DiVinE 3.0 -- An Explicit-State Model Checker for Multithreaded C & C++ Programs
Popis výsledku anglicky
We present a new release of the parallel and distributed LTL model checker DIVINE. The major improvements in this new release is an extension of the class of systems that may be verified with the model checker, while preserving the unique DIVINE feature,namely parallel and distributed-memory processing. Version 3.0 comes with support for direct model checking of (closed) multithreaded C/C++ programs, full untimed-LTL model checking of timed automata, and a general-purpose framework for interfacing witharbitrary system modelling tools.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
IN - Informatika
OECD FORD obor
—
Návaznosti výsledku
Projekt
<a href="/cs/project/GAP202%2F11%2F0312" target="_blank" >GAP202/11/0312: Vývoj a verifikace softwarových komponent v zapouzdřených systémech</a><br>
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach
Ostatní
Rok uplatnění
2013
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ů
Údaje specifické pro druh výsledku
Název statě ve sborníku
Computer Aided Verification 2013
ISBN
9783642397981
ISSN
0302-9743
e-ISSN
—
Počet stran výsledku
6
Strana od-do
863-868
Název nakladatele
Springer
Místo vydání
Heidelberg
Místo konání akce
Heidelberg
Datum konání akce
1. 1. 2013
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
—