D 2019

A Simulator for LLVM Bitcode

ROČKAI, Petr a Jiří BARNAT

Základní údaje

Originální název

A Simulator for LLVM Bitcode

Autoři

ROČKAI, Petr (703 Slovensko, domácí) a Jiří BARNAT (203 Česká republika, domácí)

Vydání

Scham, 24th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2019, od s. 127-142, 16 s. 2019

Nakladatel

Springer Verlag

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Švýcarsko

Utajení

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

Forma vydání

tištěná verze "print"

Odkazy

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/19:00107776

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-27007-0

ISSN

DOI

UT WoS

000884748400008

Klíčová slova anglicky

simulator; LLVM; verification; counterexample
Změněno: 13. 5. 2024 16:25, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

In this paper, we introduce an interactive simulator for programs in the form of LLVM bitcode. The main features of the simulator include precise control over thread scheduling, automatic checkpoints and reverse stepping, support for source-level information about functions and variables in C and C++ programs and structured heap visualisation. Additionally, the simulator is compatible with DiVM (DIVINE VM) hypercalls, which makes it possible to load, simulate and analyse counterexamples from an existing model checker.

Návaznosti

GA18-02177S, projekt VaV
Název: Abstrakce a jiné techniky v semi-symbolické verifikaci programů
Investor: Grantová agentura ČR, Abstrakce a jiné techniky v semi-symbolické verifikaci programů