Recent Publications

More Publications

. Measuring Coverage of Prolog Programs Using Mutation Testing. To appear in Proceedings WFLP, Springer LNCS, 2018.

. Repair and Generation of Formal Models Using Synthesis. Accepted for iFM 2018, 2018.

Preprint Project

. Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation. Accepted for AVoCS 2018, 2018.




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.


ProB is an animator, constraint solver and model checker for the B-Method. It allows fully automatic animation of B specifications, and can be used to systematically check a specification for a wide range of errors. The constraint-solving capabilities of ProB can also be used for model finding, deadlock checking and test-case generation.



Beitreiber gemäß § 5 TMG:

Sebastian Krings
Schiefbahner Str. 64
41352 Korschenbroich


Verantwortlich nach § 55 Abs. 2 RStV:

Sebastian Krings