2018
DiVM: Model checking with LLVM and graph memory
ROČKAI, Petr; Vladimír ŠTILL; Ivana ČERNÁ and Jiří BARNATBasic information
Original name
DiVM: Model checking with LLVM and graph memory
Authors
ROČKAI, Petr (703 Slovakia, belonging to the institution); Vladimír ŠTILL (203 Czech Republic, belonging to the institution); Ivana ČERNÁ ORCID (203 Czech Republic, belonging to the institution) and Jiří BARNAT (203 Czech Republic, belonging to the institution)
Edition
Journal of Systems and Software, Elsevier, 2018, 0164-1212
Other information
Language
English
Type of outcome
Article in a journal
Field of Study
10201 Computer sciences, information science, bioinformatics
Country of publisher
Netherlands
Confidentiality degree
is not subject to a state or trade secret
References:
Impact factor
Impact factor: 2.559
RIV identification code
RIV/00216224:14330/18:00106878
Organization unit
Faculty of Informatics
UT WoS
000438180000001
EID Scopus
2-s2.0-85046825489
Keywords in English
Model checking; C plus; Virtual machine; Verification
Tags
International impact, Reviewed
Changed: 5/11/2021 15:28, RNDr. Pavel Šmerk, Ph.D.
Abstract
In the original language
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.
Links
| GA15-08772S, research and development project |
|