ProB: an automated analysis toolset for the B method. We present ProB, a validation toolset for the B method. ProB’s automated animation facilities allow users to gain confidence in their specifications. ProB also contains a model checker and a refinement checker, both of which can be used to detect various errors in B specifications. We describe the underlying methodology of ProB, and present the important aspects of the implementation. We also present empirical evaluations as well as several case studies, highlighting that ProB enables users to uncover errors that are not easily discovered by existing tools.

References in zbMATH (referenced in 47 articles )

Showing results 1 to 20 of 47.
Sorted by year (citations)

1 2 3 next

  1. Dobrikov, Ivaylo; Leuschel, Michael: Optimising the ProB model checker for B using partial order reduction (2016)
  2. Hoang, Thai Son; Schneider, Steve; Treharne, Helen; Williams, David M.: Foundations for using linear temporal logic in Event-B refinement (2016)
  3. Vekris, Dimitris; Lang, Frédéric; Dima, Catalin; Mateescu, Radu: Verification of $\mathrmEB^3$ specifications using CADP (2016)
  4. Mammar, Amel; Frappier, Marc: Proof-based verification approaches for dynamic properties: application to the information system domain (2015)
  5. Mota, A.; Farias, A.; Woodcock, J.; Larsen, P.G.: Model checking CML: tool development and industrial applications (2015)
  6. Vu, Dieu-Huong; Chiba, Yuki; Yatake, Kenro; Aoki, Toshiaki: Checking the conformance of a Promela design to its formal specification in Event-B (2015)
  7. Li, Yi; Dong, Jin Song; Sun, Jing; Liu, Yang; Sun, Jun: Model checking approach to automated planning (2014)
  8. Llano, Maria Teresa; Ireland, Andrew; Pease, Alison: Discovery of invariants through automated theory formation (2014)
  9. Hallerstede, Stefan; Leuschel, Michael; Plagge, Daniel: Validation of formal models by refinement animation (2013)
  10. Hoang, Thai Son: Security invariants in discrete transition systems (2013)
  11. Perna, Juan I.; George, Chris: Model checking RAISE applicative specifications (2013)
  12. Barbosa, Haniel; Déharbe, David: An approach using the B method to formal verification of PLC programs in an industrial setting (2012)
  13. Hallerstede, Stefan; Leuschel, Michael: Experiments in program verification using Event-B (2012)
  14. Leino, K.Rustan M.; Yessenov, Kuat: Stepwise refinement of heap-manipulating code in Chalice (2012)
  15. Leuschel, Michael; Llorens, Marisa; Oliver, Javier; Silva, Josep; Tamarit, Salvador: Static slicing of explicitly synchronized languages (2012)
  16. Ndukwu, Ukachukwu: Generating counterexamples for quantitative safety specifications in probabilistic B (2012)
  17. Plagge, Daniel; Leuschel, Michael: Validating B,Z and TLA$^ + $ using ProB and Kodkod (2012)
  18. Vaz, Cátia; Ferreira, Carla: On the analysis of compensation correctness (2012)
  19. Williams, David M.; de Ruiter, Joeri; Fokkink, Wan: Model checking under fairness in prob and its application to fair exchange protocols (2012)
  20. Leuschel, Michael; Bendisposto, Jens: Directed model checking for B: an evaluation and new techniques (2011)

1 2 3 next