DivSIM , an interactive simulator for LLVM bitcode
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F22%3A00126286" target="_blank" >RIV/00216224:14330/22:00126286 - isvavai.cz</a>
Výsledek na webu
<a href="https://link.springer.com/article/10.1007/s10009-022-00659-x" target="_blank" >https://link.springer.com/article/10.1007/s10009-022-00659-x</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/s10009-022-00659-x" target="_blank" >10.1007/s10009-022-00659-x</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
DivSIM , an interactive simulator for LLVM bitcode
Popis výsledku v původním jazyce
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.
Název v anglickém jazyce
DivSIM , an interactive simulator for LLVM bitcode
Popis výsledku anglicky
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.
Klasifikace
Druh
J<sub>imp</sub> - Článek v periodiku v databázi Web of Science
CEP obor
—
OECD FORD obor
10200 - Computer and information sciences
Návaznosti výsledku
Projekt
—
Návaznosti
S - Specificky vyzkum na vysokych skolach
Ostatní
Rok uplatnění
2022
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název periodika
INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER
ISSN
1433-2779
e-ISSN
1433-2787
Svazek periodika
24
Číslo periodika v rámci svazku
3
Stát vydavatele periodika
DE - Spolková republika Německo
Počet stran výsledku
18
Strana od-do
493-510
Kód UT WoS článku
000777237800001
EID výsledku v databázi Scopus
2-s2.0-85127569807