Model Checking of C and C++ with DIVINE 4

March 3, 2020

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++.

Authors: Zuzana BaranováJiří BarnatKatarína KejstováTadeáš KučeraHenrich LaukoJan MrázekPetr Ročkai, and Vladimír Štill

Project: DIVINE4

Published in: International Symposium on Automated Technology for Verification and Analysis (ATVA) (to appear), 2017, volume 10482 of Lecture Notes in Computer Science.

Go to pdf

Article Link


Partner University



Associated Research Projects