Statistical Model Checking of LLVM Code
(2018) Statistical Model Checking of LLVM Code — p. pp 542-549 (2018)
Files
Legay2018_Chapter_StatisticalModelCheckingOfLLVM.pdf
Open Access - Adobe PDF
- 761.1 KB
Details
- Authors
- Abstract
- 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.
- Affiliations
Citations
Legay, A., Nowotka, D., Poulsen, D. B., & Tranouez, L.-M. (2018). Statistical Model Checking of LLVM Code. Statistical Model Checking of LLVM Code, pp 542-549. https://doi.org/10.1007/978-3-319-95582-7_32 (Original work published 2018)