Yay, I got my paper “Statistical Model Checking of LLVM Code” accepted for publication. The paper presents the tool, Lodin. A tool that performs both explicit-state model checking and Statistical model checking (SMC) of LLVM code. This combination of techniques is useful, since it allows applying SMC when the state space is too large for exhaustive techniques.

Statistical Model Checking is simulation-based and therefore it has a major drawback: finding rare events is very difficult for it. To help combat this, we integrated Lodin with Plasma-Lab. This integration provides access to Plasma-Labs many statistical methods among which is Importance Splitting. Importance splitting is exactly used for estimating probabilities of rare events.

The paper is joint work with Axel Legay, Dirk Nowotka and Louis-Marie Traonoues. A longer version of the paper is available here