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.

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

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Germany

Confidentiality degree

není předmětem státního či obchodního tajemství

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

DOI

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

Keywords in English

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

Abstract

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.

Links

GAP202/11/0312, research and development project

Name: 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 MU

Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU)

Investor: Masaryk University, Category A

Citovat

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.

@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 and 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, p.~863-868. ISBN~978-3-642-39798-1. Available from: https://dx.doi.org/10.1007/978-3-642-39799-8\_{}60.

Detailed Information on Publication Record