Informační systém MU
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. doi:10.1007/978-3-319-68167-2_14.
Other formats:   BibTeX LaTeX RIS
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
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Switzerland
Confidentiality degree is not subject to a state or trade secret
Publication form printed version "print"
WWW 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 0302-9743
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
Tags core_A, firank_A
Tags International impact, Reviewed
Changed by Changed by: prof. RNDr. Jiří Barnat, Ph.D., učo 3496. Changed: 1/10/2018 16:24.
Abstract
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 projectName: Analýza korektnosti vícevláknových programů v C a C++
Investor: Czech Science Foundation
MUNI/A/0897/2016, interní kód MUName: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VI.
Investor: Masaryk University, Category A
MUNI/A/0992/2016, interní kód MUName: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU)
Investor: Masaryk University, Category A
Displayed: 25/5/2022 08:54