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
Keywords in English Model Checking; Verification; C; C++; DIVINE
Tags 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, Standard Projects
MUNI/A/0897/2016, internal MU codeName: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VI.
Investor: Masaryk University, Grant Agency of Masaryk University, Category A
MUNI/A/0992/2016, internal MU codeName: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity (Acronym: SKOMU)
Investor: Masaryk University, Grant Agency of Masaryk University, Category A
PrintDisplayed: 29/1/2022 14:08