Case study shows that SPIN and DIVINE model checkers can uncover design flaws and code defects in a C++ framework missed by hundreds of hours of testing and can be integrated into the development workflow.
DiVM: Model Checking with LLVM and Graph Memory
1 Pith paper cite this work. Polarity classification is still indexing.
1
Pith paper citing it
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.
fields
cs.SE 1years
2019 1verdicts
UNVERDICTED 1representative citing papers
citing papers explorer
-
Model Checking a C++ Software Framework, a Case Study
Case study shows that SPIN and DIVINE model checkers can uncover design flaws and code defects in a C++ framework missed by hundreds of hours of testing and can be integrated into the development workflow.