| ||||
| ||||
![]() Title:Statistical Model Checking of LLVM Code Conference:FM 2018 Tags:explicit state model checking, Importance Splitting, LLVM, Rare Event Simulation and Statistical Model Checking Abstract: We present the new tool Lodin for statistical model checking of LLVM-bitcode. Lodin implememts a simulation engine for LLVM- bitcode and implements classic statistical model checking algorithms on top it. The simulation engine implements only the core of LLVM but supports extending this core through a plugin-architecture. Besides the statistical model checking algorithms Lodin also provides an interactive simulation front-end. The simulator front-end was integral for our second contribution - an integration of Lodin into Plasma-Lab. The integration with Plasma-Lab is integral to allow reasoning about rare properties of programs. Statistical Model Checking of LLVM Code ![]() Statistical Model Checking of LLVM Code | ||||
Copyright © 2002 – 2025 EasyChair |