DivSIM , an interactive simulator for LLVM bitcode
Authors | |
---|---|
Year of publication | 2022 |
Type | Article in Periodical |
Magazine / Source | INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER |
MU Faculty or unit | |
Citation | ROČKAI, Petr and Jiří BARNAT. DivSIM , an interactive simulator for LLVM bitcode. INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER. GERMANY: SPRINGER HEIDELBERG, 2022, vol. 24, No 3, p. 493-510. ISSN 1433-2779. Available from: https://dx.doi.org/10.1007/s10009-022-00659-x. |
web | https://link.springer.com/article/10.1007/s10009-022-00659-x |
Doi | http://dx.doi.org/10.1007/s10009-022-00659-x |
Keywords | Abstracting; C++ (programming language); Computer software; Simulators |
Description | 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. |
Related projects: |