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

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

• Originální 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: 0302-9743
• 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

Anotace

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