DiVM: Model Checking with LLVM and Graph Memory
This work addresses software verification for developers and researchers, presenting an incremental improvement by integrating graph memory into an existing LLVM-based framework.
The paper tackles the problem of software verification by introducing a virtual machine with graph-organized memory as a backend for explicit-state and abstraction-driven verification, using LLVM IR enriched with hypercalls, and demonstrates its viability by comparing it with a traditional LLVM model checker.
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.