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 fi nish 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 specifi cation language to be checked is needed and where further optimization can take place. To conclude, we compare to other model checkers for classical B.

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