A Simulator for LLVM Bitcode

• 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
• 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

• Abstrakce a jiné techniky v semi-symbolické verifikaci programů