| ROČKAI, Petr, Vladimír ŠTILL, Ivana ČERNÁ and Jiří BARNAT. DiVM: Model checking with LLVM and graph memory. Journal of Systems and Software. Elsevier, 2018, vol. 143, Oct, p. 1-13. ISSN 0164-1212. Available from: https://dx.doi.org/10.1016/j.jss.2018.04.026. |
Other formats:
BibTeX
LaTeX
RIS
@article{1528139,
author = {Ročkai, Petr and Štill, Vladimír and Černá, Ivana and Barnat, Jiří},
article_number = {Oct},
doi = {http://dx.doi.org/10.1016/j.jss.2018.04.026},
keywords = {Model checking; C plus; Virtual machine; Verification},
language = {eng},
issn = {0164-1212},
journal = {Journal of Systems and Software},
title = {DiVM: Model checking with LLVM and graph memory},
url = {https://www.sciencedirect.com/science/article/pii/S0164121218300700},
volume = {143},
year = {2018}
}
TY - JOUR
ID - 1528139
AU - Ročkai, Petr - Štill, Vladimír - Černá, Ivana - Barnat, Jiří
PY - 2018
TI - DiVM: Model checking with LLVM and graph memory
JF - Journal of Systems and Software
VL - 143
IS - Oct
SP - 1-13
EP - 1-13
PB - Elsevier
SN - 01641212
KW - Model checking
KW - C plus
KW - Virtual machine
KW - Verification
UR - https://www.sciencedirect.com/science/article/pii/S0164121218300700
L2 - https://www.sciencedirect.com/science/article/pii/S0164121218300700
N2 - 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.
ER -
ROČKAI, Petr, Vladimír ŠTILL, Ivana ČERNÁ and Jiří BARNAT. DiVM: Model checking with LLVM and graph memory. \textit{Journal of Systems and Software}. Elsevier, 2018, vol.~143, Oct, p.~1-13. ISSN~0164-1212. Available from: https://dx.doi.org/10.1016/j.jss.2018.04.026.
|
