BMoth

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.

Avatar
Sebastian Krings
Postdoc

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

Publications