DiVM: Model checking with LLVM and graph memory

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Autoři

ROČKAI Petr ŠTILL Vladimír ČERNÁ Ivana BARNAT Jiří

Rok publikování 2018
Druh Článek v odborném periodiku
Časopis / Zdroj Journal of Systems and Software
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Doi http://dx.doi.org/10.1016/j.jss.2018.04.026
Klíčová slova Model checking; C plus; Virtual machine; Verification
Popis 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.
Související projekty: