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.