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