D 2019

A Simulator for LLVM Bitcode

ROČKAI, Petr and Jiří BARNAT

Basic information

Original name

A Simulator for LLVM Bitcode

Authors

ROČKAI, Petr (703 Slovakia, belonging to the institution) and Jiří BARNAT (203 Czech Republic, belonging to the institution)

Edition

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

Publisher

Springer Verlag

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Switzerland

Confidentiality degree

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

Publication form

printed version "print"

References:

URL

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/19:00107776

Organization unit

Faculty of Informatics

ISBN

978-3-030-27007-0

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-27008-7_8

UT WoS

000884748400008

Keywords in English

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

Abstract

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.

Links

GA18-02177S, research and development project
Name: Abstrakce a jiné techniky v semi-symbolické verifikaci programů
Investor: Czech Science Foundation
Displayed: 6/11/2024 16:46