J 2018

DiVM: Model checking with LLVM and graph memory

ROČKAI, Petr, Vladimír ŠTILL, Ivana ČERNÁ a Jiří BARNAT

Základní údaje

Originální název

DiVM: Model checking with LLVM and graph memory

Autoři

ROČKAI, Petr (703 Slovensko, domácí), Vladimír ŠTILL (203 Česká republika, domácí), Ivana ČERNÁ (203 Česká republika, domácí) a Jiří BARNAT (203 Česká republika, domácí)

Vydání

Journal of Systems and Software, Elsevier, 2018, 0164-1212

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Nizozemské království

Utajení

není předmětem státního či obchodního tajemství

Odkazy

Impakt faktor

Impact factor: 2.559

Kód RIV

RIV/00216224:14330/18:00106878

Organizační jednotka

Fakulta informatiky

DOI

UT WoS

000438180000001

Klíčová slova anglicky

Model checking; C plus; Virtual machine; Verification

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 5. 11. 2021 15:28, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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.

Návaznosti

GA15-08772S, projekt VaV
Název: Analýza korektnosti vícevláknových programů v C a C++
Investor: Grantová agentura ČR, Correctness Analysis of C and C++ Programs with Threads