DiVM: Model checking with LLVM and graph memory
| Authors | |
|---|---|
| Year of publication | 2018 |
| Type | Article in Periodical |
| Magazine / Source | Journal of Systems and Software |
| MU Faculty or unit | |
| 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: |