BARNAT, Jiří, Luboš BRIM, Vojtěch HAVEL, Jan HAVLÍČEK, Jan KRIHO, Milan LENČO, Petr ROČKAI, Vladimír ŠTILL and 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, p. 863-868. ISBN 978-3-642-39798-1. Available from: https://dx.doi.org/10.1007/978-3-642-39799-8_60.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name DiVinE 3.0 -- An Explicit-State Model Checker for Multithreaded C & C++ Programs
Name in Czech DiVinE 3.0 -- Explicitně-stavový nástroj pro ověřování modelu pro vícevláknové C a C++ programy
Authors BARNAT, Jiří (203 Czech Republic, guarantor, belonging to the institution), Luboš BRIM (203 Czech Republic, belonging to the institution), Vojtěch HAVEL (203 Czech Republic, belonging to the institution), Jan HAVLÍČEK (203 Czech Republic, belonging to the institution), Jan KRIHO (203 Czech Republic, belonging to the institution), Milan LENČO (703 Slovakia, belonging to the institution), Petr ROČKAI (703 Slovakia, belonging to the institution), Vladimír ŠTILL (203 Czech Republic, belonging to the institution) and Jiří WEISER (203 Czech Republic, belonging to the institution).
Edition Heidelberg, Computer Aided Verification 2013, p. 863-868, 6 pp. 2013.
Publisher Springer
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Germany
Confidentiality degree is not subject to a state or trade secret
Publication form printed version "print"
Impact factor Impact factor: 0.402 in 2005
RIV identification code RIV/00216224:14330/13:00066526
Organization unit Faculty of Informatics
ISBN 978-3-642-39798-1
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-642-39799-8_60
Keywords in English model checking; LLVM; C++; C; LTL; timed automata
Tags core_A, firank_1
Changed by Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 27/4/2014 23:39.
Abstract
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.
Links
GAP202/11/0312, research and development projectName: Vývoj a verifikace softwarových komponent v zapouzdřených systémech (Acronym: Components in Embedded Systems)
Investor: Czech Science Foundation
MUNI/A/0739/2012, interní kód MUName: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU)
Investor: Masaryk University, Category A
PrintDisplayed: 14/5/2024 03:23