Další formáty:
BibTeX
LaTeX
RIS
@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 a 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. s.~201-207. ISBN~978-3-319-68166-5. doi:10.1007/978-3-319-68167-2\_{}14. 2017.
|
