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, 2017, s.~201-207. ISBN~978-3-319-68166-5. Dostupné z: https://dx.doi.org/10.1007/978-3-319-68167-2\_{}14.
|