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.
We are currently offline. Please leave a message and we will answer you soon. 