@inproceedings{DIVINEToolPaper2017,
 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++.},
 address = {Cham},
 author = {Zuzana Baranová and Jiří Barnat and Katarína Kejstová and Tadeáš Kučera and Henrich Lauko and Jan Mrázek and Petr Ročkai and Vladimír Štill},
 booktitle = {{Automated Technology for Verification and Analysis}},
 doi = {10.1007/978-3-319-68167-2_14},
 editor = {D'Souza, Deepak and Narayan Kumar, K.},
 isbn = {978-3-319-68167-2},
 note = {https://divine.fi.muni.cz/2017/divine4/},
 pages = {201--207},
 publisher = {Springer International Publishing},
 title = {{Model Checking of C and C++ with DIVINE 4}},
 year = {2017}
}