DiVM: Model checking with LLVM and graph memory

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	ROČKAI Petr ŠTILL Vladimír ČERNÁ Ivana BARNAT Jiří
Year of publication	2018
Type	Article in Periodical
Magazine / Source	Journal of Systems and Software
MU Faculty or unit	Faculty of Informatics
Citation
Web	https://www.sciencedirect.com/science/article/pii/S0164121218300700
Doi	http://dx.doi.org/10.1016/j.jss.2018.04.026
Keywords	Model checking; C plus; Virtual machine; Verification
Description	In this paper, we introduce the concept of a virtual machine with graph-organised memory as a versatile backend for both explicit-state and abstraction-driven verification of software. Our virtual machine uses the LLVM IR as its instruction set, enriched with a small set of hypercalls. We show that the provided hypercalls are sufficient to implement a small operating system, which can then be linked with applications to provide a POSIX-compatible verification environment. Finally, we demonstrate the viability of the approach through a comparison with a more traditionally-designed LLVM model checker.
Related projects:	Correctness Analysis of C and C++ Programs with Threads