DiVM: Model checking with LLVM and graph memory

Logo poskytovatele

Varování

Publikace nespadá pod Ekonomicko-správní 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
www https://www.sciencedirect.com/science/article/pii/S0164121218300700
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:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.