BMoth is a prototypical model checker for models written in classical B. Initially, BMoth was a student project intended to teach basics of model checking and how to implement explicit-state and symbolic model checking algorithms. In consequence, its focus lies on reusing existing libraries to reduce implementation effort. Nowadays, BMoth serves as a testbed for novel algorithms and implementation techniques.
Experience Report on An Inquiry-Based Course on Model Checking. Proceedings 16. Workshop Software Engineering im Unterricht der Hochschulen (SEUH 2019), CEUR Workshop Proceedings (to appear).(2019).
Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation. Proceedings 18th International Workshop on Automated Verification of Critical Systems (AVoCS 2018), Electronic Communications of the EASST.(2018).