DiVM: Model checking with LLVM and graph memory

Investor logo

Warning

This publication doesn't include Faculty of Sports Studies. 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:

You are running an old browser version. We recommend updating your browser to its latest version.

More info