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



Partner University



Associated Research Projects