A Simulator for LLVM Bitcode
| Autor: | Jiří Barnat, Petr Ročkai |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
Thread scheduling
Model checking 050101 languages & linguistics Computer science 05 social sciences 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing 0501 psychology and cognitive sciences 02 engineering and technology Simulation Heap (data structure) Counterexample Visualization |
| Zdroj: | Formal Methods for Industrial Critical Systems ISBN: 9783030270070 FMICS |
| DOI: | 10.1007/978-3-030-27008-7_8 |
| 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|