Model Checking of C and C++ with DIVINE 4

D 2017

Model Checking of C and C++ with DIVINE 4

BARANOVÁ, Zuzana, Jiří BARNAT, Katarína KEJSTOVÁ, Tadeáš KUČERA, Henrich LAUKO et. al.

Basic information

Original name

Model Checking of C and C++ with DIVINE 4

Authors

BARANOVÁ, Zuzana (703 Slovakia, belonging to the institution), Jiří BARNAT (203 Czech Republic, guarantor, belonging to the institution), Katarína KEJSTOVÁ (703 Slovakia, belonging to the institution), Tadeáš KUČERA (203 Czech Republic, belonging to the institution), Henrich LAUKO (703 Slovakia, belonging to the institution), Jan MRÁZEK (203 Czech Republic, belonging to the institution), Petr ROČKAI (703 Slovakia, belonging to the institution) and Vladimír ŠTILL (203 Czech Republic, belonging to the institution)

Edition

Cham, Automated Technology for Verification and Analysis, p. 201-207, 7 pp. 2017

Publisher

Springer International Publishing

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Switzerland

Confidentiality degree

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

Publication form

printed version "print"

References:

URL

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/17:00095126

Organization unit

Faculty of Informatics

ISBN

978-3-319-68166-5

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-68167-2_14

UT WoS

000723567800014

Keywords in English

Model Checking; Verification; C; C++; DIVINE

Abstract

V originále

The fourth version of the DIVINE model checker provides a modular platform for verification of real-world programs. It is built around an efficient interpreter of LLVM code which, together with a small, verification-oriented operating system and a set of runtime libraries, enables verification of code written in C and C++.

Links

GA15-08772S, research and development project

Name: Analýza korektnosti vícevláknových programů v C a C++

Investor: Czech Science Foundation

MUNI/A/0897/2016, interní kód MU

Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VI.

Investor: Masaryk University, Category A

MUNI/A/0992/2016, interní kód MU

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

Investor: Masaryk University, Category A

Citovat

BARANOVÁ, Zuzana, Jiří BARNAT, Katarína KEJSTOVÁ, Tadeáš KUČERA, Henrich LAUKO, Jan MRÁZEK, Petr ROČKAI and Vladimír ŠTILL. Model Checking of C and C++ with DIVINE 4. In Deepak D'Souza, K. Narayan Kumar. Automated Technology for Verification and Analysis. Cham: Springer International Publishing, 2017, p. 201-207. ISBN 978-3-319-68166-5. Available from: https://dx.doi.org/10.1007/978-3-319-68167-2_14.

@inproceedings{1394153,
   author = {Baranová, Zuzana and Barnat, Jiří and Kejstová, Katarína and Kučera, Tadeáš and Lauko, Henrich and Mrázek, Jan and Ročkai, Petr and Štill, Vladimír},
   address = {Cham},
   booktitle = {Automated Technology for Verification and Analysis},
   doi = {http://dx.doi.org/10.1007/978-3-319-68167-2_14},
   editor = {Deepak D'Souza, K. Narayan Kumar},
   keywords = {Model Checking; Verification; C; C++; DIVINE},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Cham},
   isbn = {978-3-319-68166-5},
   pages = {201-207},
   publisher = {Springer International Publishing},
   title = {Model Checking of C and C++ with DIVINE 4},
   url = {https://link.springer.com/chapter/10.1007/978-3-319-68167-2_14},
   year = {2017}
}

TY  - JOUR
ID  - 1394153
AU  - Baranová, Zuzana - Barnat, Jiří - Kejstová, Katarína - Kučera, Tadeáš - Lauko, Henrich - Mrázek, Jan - Ročkai, Petr - Štill, Vladimír
PY  - 2017
TI  - Model Checking of C and C++ with DIVINE 4
PB  - Springer International Publishing
CY  - Cham
SN  - 9783319681665
KW  - Model Checking
KW  - Verification
KW  - C
KW  - C++
KW  - DIVINE
UR  - https://link.springer.com/chapter/10.1007/978-3-319-68167-2_14
L2  - https://link.springer.com/chapter/10.1007/978-3-319-68167-2_14
N2  - The fourth version of the DIVINE model checker provides a modular platform for verification of real-world programs. It is built around an efficient interpreter of LLVM code which, together with a small, verification-oriented operating system and a set of runtime libraries, enables verification of code written in C and C++.
ER  -

BARANOVÁ, Zuzana, Jiří BARNAT, Katarína KEJSTOVÁ, Tadeáš KUČERA, Henrich LAUKO, Jan MRÁZEK, Petr ROČKAI and Vladimír ŠTILL. Model Checking of C and C++ with DIVINE 4. In Deepak D'Souza, K. Narayan Kumar. \textit{Automated Technology for Verification and Analysis}. Cham: Springer International Publishing, 2017, p.~201-207. ISBN~978-3-319-68166-5. Available from: https://dx.doi.org/10.1007/978-3-319-68167-2\_{}14.

Detailed Information on Publication Record