DiVinE 3.0 -- An Explicit-State Model Checker for Multithreaded
C & C++ Programs

D 2013

DiVinE 3.0 -- An Explicit-State Model Checker for Multithreaded C & C++ Programs

BARNAT, Jiří, Luboš BRIM, Vojtěch HAVEL, Jan HAVLÍČEK, Jan KRIHO et. al.

Základní údaje

Originální název

DiVinE 3.0 -- An Explicit-State Model Checker for Multithreaded C & C++ Programs

Název česky

DiVinE 3.0 -- Explicitně-stavový nástroj pro ověřování modelu pro vícevláknové C a C++ programy

Autoři

BARNAT, Jiří (203 Česká republika, garant, domácí), Luboš BRIM (203 Česká republika, domácí), Vojtěch HAVEL (203 Česká republika, domácí), Jan HAVLÍČEK (203 Česká republika, domácí), Jan KRIHO (203 Česká republika, domácí), Milan LENČO (703 Slovensko, domácí), Petr ROČKAI (703 Slovensko, domácí), Vladimír ŠTILL (203 Česká republika, domácí) a Jiří WEISER (203 Česká republika, domácí)

Vydání

Heidelberg, Computer Aided Verification 2013, od s. 863-868, 6 s. 2013

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

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/13:00066526

Organizační jednotka

Fakulta informatiky

ISBN

978-3-642-39798-1

ISSN

DOI

http://dx.doi.org/10.1007/978-3-642-39799-8_60

Klíčová slova anglicky

model checking; LLVM; C++; C; LTL; timed automata

Štítky

core_A, firank_1

Změněno: 27. 4. 2014 23:39, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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 with arbitrary system modelling tools.

Návaznosti

GAP202/11/0312, projekt VaV

Název: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Akronym: Components in Embedded Systems)

Investor: Grantová agentura ČR, Software Components in Embedded Systems: Development and Verification

MUNI/A/0739/2012, interní kód MU

Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Akronym: SKOMU)

Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity, DO R. 2020_Kategorie A - Specifický výzkum - Studentské výzkumné projekty

Citovat

BARNAT, Jiří, Luboš BRIM, Vojtěch HAVEL, Jan HAVLÍČEK, Jan KRIHO, Milan LENČO, Petr ROČKAI, Vladimír ŠTILL a Jiří WEISER. DiVinE 3.0 -- An Explicit-State Model Checker for Multithreaded C & C++ Programs. In Sharygina, Natasha; Veith, Helmut. Computer Aided Verification 2013. Heidelberg: Springer, 2013, s. 863-868. ISBN 978-3-642-39798-1. Dostupné z: https://dx.doi.org/10.1007/978-3-642-39799-8_60.

@inproceedings{1130026,
   author = {Barnat, Jiří and Brim, Luboš and Havel, Vojtěch and Havlíček, Jan and Kriho, Jan and Lenčo, Milan and Ročkai, Petr and Štill, Vladimír and Weiser, Jiří},
   address = {Heidelberg},
   booktitle = {Computer Aided Verification 2013},
   doi = {http://dx.doi.org/10.1007/978-3-642-39799-8_60},
   editor = {Sharygina, Natasha; Veith, Helmut},
   keywords = {model checking; LLVM; C++; C; LTL; timed automata},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Heidelberg},
   isbn = {978-3-642-39798-1},
   pages = {863-868},
   publisher = {Springer},
   title = {DiVinE 3.0 -- An Explicit-State Model Checker for Multithreaded C & C++ Programs},
   year = {2013}
}

TY  - JOUR
ID  - 1130026
AU  - Barnat, Jiří - Brim, Luboš - Havel, Vojtěch - Havlíček, Jan - Kriho, Jan - Lenčo, Milan - Ročkai, Petr - Štill, Vladimír - Weiser, Jiří
PY  - 2013
TI  - DiVinE 3.0 -- An Explicit-State Model Checker for Multithreaded C & C++ Programs
PB  - Springer
CY  - Heidelberg
SN  - 9783642397981
KW  - model checking
KW  - LLVM
KW  - C++
KW  - C
KW  - LTL
KW  - timed automata
N2  - 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 with arbitrary system modelling tools.
ER  -

BARNAT, Jiří, Luboš BRIM, Vojtěch HAVEL, Jan HAVLÍČEK, Jan KRIHO, Milan LENČO, Petr ROČKAI, Vladimír ŠTILL a Jiří WEISER. DiVinE 3.0 -- An Explicit-State Model Checker for Multithreaded C \&{} C++ Programs. In Sharygina, Natasha; Veith, Helmut. \textit{Computer Aided Verification 2013}. Heidelberg: Springer, 2013, s.~863-868. ISBN~978-3-642-39798-1. Dostupné z: https://dx.doi.org/10.1007/978-3-642-39799-8\_{}60.

Podrobný výpis o publikaci