ProB for Event-B

In addition to classical B (aka B for software development), ProB also supports Event-B and the Rodin platform. ProB can be installed as a plugin for Rodin. See the tutorial pages for more information:

• Starting ProB for Rodin and first animation steps
• Important Parameters of ProB for Rodin
• Exporting Rodin Models for ProB Classic
• Using the Symbolic Contants Plugin
• Using the ProB (Dis-)Prover
• Visualization of LTL Counter-examples in Rodin

The Rodin handbook also contains material about ProB:

• Finding Invariant Violations with ProB
• Finding Solutions to Axioms