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.
- full text (pdf, revision 3, 2017-12-10)
Benchmark Data
You can download all measurement data as a compressed PostgreSQL database dump: divbench.psql.xz. The relevant instance identifiers used in the paper are following:
- DIVINE 4 (labelled as D4 in the paper): 16891042
- DIVINE 3 with fixed thread interleaving (labelled as D3+p): 16634308
- DIVINE 3 (original reduction, labelled D3): 13148753
- ESBMC 4.1.0 (binary from tool’s homepage): 17253816
Benchmarked Tools
Source codes of all benchmarked versions of DIVINE and binaries of ESBMC are also available: