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.

Sebastian Krings

My research interests include formal methods, model checking and logic programming.


The development and improvement of model checkers for the validation of hard- and software is an ongoing research topic in computer …

During a course on model checking we developed BMoth, a full-stack model checker for classical B, featuring both explicit-state and …