DivSIM , an interactive simulator for LLVM bitcode

• Autoři: ROČKAI Petr; BARNAT Jiří
• Rok publikování: 2022
• Druh: Článek v odborném periodiku
• Časopis / Zdroj: INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER
• Fakulta / Pracoviště MU: Fakulta informatiky
• www: https://link.springer.com/article/10.1007/s10009-022-00659-x
• Doi: http://dx.doi.org/10.1007/s10009-022-00659-x
• Klíčová slova: Abstracting; C++ (programming language); Computer software; Simulators
• Popis: 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ů.

Související projekty

• Rozsáhlé výpočetní systémy: modely, aplikace a verifikace XI.