J 2022

DivSIM , an interactive simulator for LLVM bitcode

ROČKAI, Petr a Jiří BARNAT

Základní údaje

Originální název

DivSIM , an interactive simulator for LLVM bitcode

Autoři

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

Vydání

INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, GERMANY, SPRINGER HEIDELBERG, 2022, 1433-2779

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10200 1.2 Computer and information sciences

Stát vydavatele

Německo

Utajení

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

Odkazy

Impakt faktor

Impact factor: 1.500

Kód RIV

RIV/00216224:14330/22:00126286

Organizační jednotka

Fakulta informatiky

DOI

UT WoS

000777237800001

Klíčová slova anglicky

Abstracting; C++ (programming language); Computer software; Simulators

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 28. 3. 2023 11:41, RNDr. Pavel Šmerk, Ph.D.

Anotace

ORIG CZ

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, DivSIM is compatible with DiVM (DIVINE VM) hypercalls, which makes it possible to load, simulate and analyse counterexamples from an existing model checker, and with abstract bitcode generated by LART (LLVM Abstraction and Refinement Tool), making it suitable for direct analysis of abstract and/or symbolic programs and counterexamples.

Česky

V tomto článku představujeme interaktivní simulátor pro programy ve formě LLVM bitcode. Mezi hlavní vlastnosti simulátoru patří precizní kontrola nad plánováním vláken, automatické kontrolní body a zpětné krokování, podpora informací o funkcích a proměnných na úrovni zdroje v programech C a C++ a strukturovaná vizualizace haldy. Kromě toho je DivSIM kompatibilní s hypervoláním DiVM (DIVINE VM), což umožňuje načítat, simulovat a analyzovat protipříklady ze stávajícího nástroje pro kontrolu modelu a s abstraktním bitkódem generovaným LART (LLVM Abstraction and Refinement Tool), takže je vhodný pro přímou analýzu abstraktních a/nebo symbolických programů a protipříkladů.

Návaznosti

MUNI/A/1145/2021, interní kód MU
Název: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace XI. (Akronym: SV-FI MAV XI.)
Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace XI.