DiVM: Model Checking with LLVM and Graph Memory
Software Engineering
2019-07-10 v3
Abstract
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.
Cite
@article{arxiv.1703.05341,
title = {DiVM: Model Checking with LLVM and Graph Memory},
author = {Petr Ročkai and Vladimír Štill and Ivana černá and Jiří Barnat},
journal= {arXiv preprint arXiv:1703.05341},
year = {2019}
}
Comments
2017-04-19 / revision 3: add a missing author to arxiv metadata 2017-03-31 / revision 2: now with an experimental evaluation