A Simulator for LLVM Bitcode

Logo poskytovatele

Varování

Publikace nespadá pod Ekonomicko-správní fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

ROČKAI Petr BARNAT Jiří

Rok publikování 2019
Druh Článek ve sborníku
Konference 24th International Conference on Formal Methods for Industrial Critical Systems, FMICS 2019
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www https://link.springer.com/chapter/10.1007%2F978-3-030-27008-7_8
Doi http://dx.doi.org/10.1007/978-3-030-27008-7_8
Klíčová slova simulator; LLVM; verification; counterexample
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.