DiVM: Model checking with LLVM and graph memory
| Autoři | |
|---|---|
| Rok publikování | 2018 |
| Druh | Článek v odborném periodiku |
| Časopis / Zdroj | Journal of Systems and Software |
| Fakulta / Pracoviště MU | |
| 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: |