Publication details

Model Checking of C and C++ with DIVINE 4

Authors

BARANOVÁ Zuzana BARNAT Jiří KEJSTOVÁ Katarína KUČERA Tadeáš LAUKO Henrich MRÁZEK Jan ROČKAI Petr ŠTILL Vladimír

Year of publication 2017
Type Article in Proceedings
Conference Automated Technology for Verification and Analysis
MU Faculty or unit

Faculty of Informatics

Citation
Web https://link.springer.com/chapter/10.1007/978-3-319-68167-2_14
Doi http://dx.doi.org/10.1007/978-3-319-68167-2_14
Field Informatics
Keywords Model Checking; Verification; C; C++; DIVINE
Description 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++.
Related projects: