Model Checking of C and C++ with DIVINE 4

Warning

This publication doesn't include Faculty of Education. 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:	Correctness Analysis of C and C++ Programs with Threads Rozsáhlé výpočetní systémy: modely, aplikace a verifikace VI. Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity