We present the new tool Lodin for statistical model checking of LLVM-bitcode. Lodin implements a simulation engine for LLVM-bitcode and implements classic statistical model checking algorithms on top of 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.
CITATION STYLE
Legay, A., Nowotka, D., Poulsen, D. B., & Tranouez, L. M. (2018). Statistical model checking of LLVM code. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10951 LNCS, pp. 542–549). Springer Verlag. https://doi.org/10.1007/978-3-319-95582-7_32
Mendeley helps you to discover research relevant for your work.