ProB: a model-checker for data validation

26 March 2013

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

Prob is developed by the team of Michael Leuschel, University of Dusseldorf, while commercial support is provided by the spin-off company Formal Mind.

ProB is now being used within Siemens and Alstom for data validation of complicated properties.