DiVinE 3.0 -- An Explicit-State Model Checker for Multithreaded C & C++ Programs (2013)výskyt výsledku
| Identifikační kód | RIV/00216224:14330/13:00066526 |
|---|---|
| Název v anglickém jazyce | DiVinE 3.0 -- An Explicit-State Model Checker for Multithreaded C & C++ Programs |
| Druh | D - Článek ve sborníku |
| Jazyk | eng - angličtina |
| Obor - skupina | I - Informatika |
| Obor | IN - Informatika |
| Rok uplatnění | 2013 |
| Kód důvěrnosti údajů | S - Úplné a pravdivé údaje o výsledku nepodléhající ochraně podle zvláštních právních předpisů. |
| Počet výskytů výsledku | 2 |
| Počet tvůrců celkem | 9 |
| Počet domácích tvůrců | 9 |
| Výčet všech uvedených jednotlivých tvůrců | Jiří Barnat (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 5692792) Luboš Brim (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 6500773) Vojtěch Havel (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 3095673) Jan Havlíček (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 1753444) Jan Kriho (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 1956256) Milan Lenčo (státní příslušnost: SK - Slovenská republika, domácí tvůrce: A, vedidk: 4075951) Petr Ročkai (státní příslušnost: SK - Slovenská republika, domácí tvůrce: A, vedidk: 1292358) Vladimír Štill (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 6284272) Jiří Weiser (státní příslušnost: CZ - Česká republika, domácí tvůrce: A, vedidk: 8287031) |
| Popis výsledku v anglické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. |
| Klíčová slova oddělená středníkem | model checking; LLVM; C++; C; LTL; timed automata |
| Stránka www, na které se nachází výsledek | - |
| DOI výsledku | 10.1007/978-3-642-39799-8_60 |
Údaje o výsledku v závislosti na druhu výsledku
| Název sborníku | Computer Aided Verification 2013 |
|---|---|
| ISBN | 9783642397981 |
| ISSN | 0302-9743 |
| 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 | 2013 |
| Typ akce podle státní příslušnosti účastníků | WRD - Celosvětová |
| Kód UT WoS článku podle Web of Science | - |
Ostatní informace o výsledku
| Předkladatel | Masarykova univerzita / Fakulta informatiky |
|---|---|
| Dodavatel | MSM - Ministerstvo školství, mládeže a tělovýchovy (MŠMT) |
| Rok sběru | 2014 |
| Specifikace | RIV/00216224:14330/13:00066526!RIV14-MSM-14330___ |
| Datum poslední aktualizace výsledku | 29.05.2014 |
| Kontrolní číslo | 56538277 |
Informace o dalších výskytech výsledku dodaného stejným předkladatelem
| Dodáno GA ČR v roce 2014 | RIV/00216224:14330/13:00066526 v dodávce dat RIV14-GA0-14330___/01:1 |
|---|
Odkazy na výzkumné aktivity, při jejichž řešení výsledek vznikl
| Projekt podporovaný GA ČR v programu GA | GAP202/11/0312 - Vývoj a verifikace softwarových komponent v zapouzdřených systémech (2011 - 2013) |
|---|---|
| Podpora / návaznosti | Specifický výzkum na vysokých školách, poskytovatel MŠMT |