# DiVM: Model Checking with LLVM and Graph Memory

## TL;DR

This paper presents DiVM, a virtual machine with graph-organized memory using LLVM IR, enabling flexible software verification through hypercalls and a POSIX-compatible environment, demonstrated via comparison with traditional LLVM model checkers.

## Contribution

Introduces DiVM, a novel LLVM-based virtual machine with graph memory and hypercalls, facilitating versatile software verification and OS integration.

## Key findings

- DiVM supports explicit and abstract verification methods.
- Demonstrated compatibility with POSIX applications.
- Comparison shows DiVM's effectiveness over traditional LLVM model checkers.

## 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.