Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation


During a course on model checking we developed BMoth, a full-stack model checker for classical B, featuring both explicit-state and symbolic model checking. Given that we only had a single university term to finish the project, a particular focus was on reusing existing libraries to reduce implementation workload. In the following, we report on a selection of reusable libraries, which can be combined into a prototypical model checker relatively easily. Additionally, we discuss where custom code depending on the specification language to be checked is needed and where further optimization can take place.. To conclude, we compare to other model checkers for classical B.

In Proceedings 18th International Workshop on Automated Verification of Critical Systems (AVoCS 2018), Electronic Communications of the EASST
Sebastian Krings
Sebastian Krings
Software Engineer

My interests include software analysis, formal methods and offensive security.