At the core of the B-Method is a very expressive language rooted in predicate logic, set theory, relational calculus, higher-order functions and arithmetic. At the heart of our ProB toolset is an evaluator and constraint solver for this language. We strive for both efficiency and correctness, such that the tool can be used in a safety-critical context.

The company ClearSy has posted an interesting success story about using our tool ProB for a railways reverse-engineering project, where they have made use of ProB’s constraint solver in a new way. The article says “Data validation principles have been applied recently to a railways reverse-engineering project with great success. B and ProB have demonstrated again how efficient they are when used in combination. … This problem was solved elegantly by using data validation principles: a B model representing the two graphs and their properties were elaborated, and ProB used for finding a solution.”

Below is the matching graph generated by the ProB constraint solver between the application binary and the high-level source code: