Model Checking of C and C++ with DIVINE 4

Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
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:

You are running an old browser version. We recommend updating your browser to its latest version.