  In this work we present our work in developing a software verification tool
for llvm-code - Lodin - that incorporates both explicit-state model checking,
statistical model checking and symbolic state model checking algorithms.
