ProB

ProB

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. 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.

Avatar
Sebastian Krings
Postdoc

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

Publications

(2015). Inferring Physical Units in Formal Models. Software and Systems Modeling, Springer.

PDF Project

(2014). Turning Failure into Proof: The ProB Disprover. Poster presented at SAT / SMT Summer School.

Project Poster