Model Checking of C and C++ with DIVINE 4

Varování

Publikace nespadá pod Ústav výpočetní techniky, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Autoři	BARANOVÁ Zuzana BARNAT Jiří KEJSTOVÁ Katarína KUČERA Tadeáš LAUKO Henrich MRÁZEK Jan ROČKAI Petr ŠTILL Vladimír
Rok publikování	2017
Druh	Článek ve sborníku
Konference	Automated Technology for Verification and Analysis
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
www	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
Obor	Informatika
Klíčová slova	Model Checking; Verification; C; C++; DIVINE
Popis	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++.
Související projekty:	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