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 59 articles )

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

1 2 3 next

  1. Cristiá, Maximiliano; Rossi, Gianfranco: Solving quantifier-free first-order constraints over finite sets and binary relations (2020)
  2. Kobayashi, Tsutomu; Ishikawa, Fuyuki; Honiden, Shinichi: Consistency-preserving refactoring of refinement structures in Event-B models (2019)
  3. Llorens, M.; Oliver, J.; Silva, J.; Tamarit, S.: Tracking CSP computations (2019)
  4. van der Hallen, Matthias; Paramonov, Sergey; Janssens, Gerda; Denecker, Marc: Knowledge representation analysis of graph mining (2019)
  5. Cristiá, Maximiliano; Rossi, Gianfranco: A set solver for finite set relation algebra (2018)
  6. Cristiá, Maximiliano; Rossi, Gianfranco: A decision procedure for restricted intensional sets (2017)
  7. Graiet, Mohamed; Hamel, Lazhar; Mammar, Amel; Tata, Samir: A verification and deployment approach for elastic component-based applications (2017)
  8. Dobrikov, Ivaylo; Leuschel, Michael: Optimising the ProB model checker for B using partial order reduction (2016)
  9. Hoang, Thai Son; Schneider, Steve; Treharne, Helen; Williams, David M.: Foundations for using linear temporal logic in Event-B refinement (2016)
  10. Vekris, Dimitris; Lang, Frédéric; Dima, Catalin; Mateescu, Radu: Verification of (\mathrmEB^3) specifications using CADP (2016)
  11. Abrial, Jean-Raymond: Definition of a mathematical language together with its proof system in Event-B (2015)
  12. Mammar, Amel; Frappier, Marc: Proof-based verification approaches for dynamic properties: application to the information system domain (2015)
  13. Mota, A.; Farias, A.; Woodcock, J.; Larsen, P. G.: Model checking CML: tool development and industrial applications (2015) ioport
  14. Sulskus, Gintautas; Poppleton, Michael; Rezazadeh, Abdolbaghi: An interval-based approach to modelling time in Event-B (2015) ioport
  15. Vu, Dieu-Huong; Chiba, Yuki; Yatake, Kenro; Aoki, Toshiaki: Checking the conformance of a Promela design to its formal specification in Event-B (2015)
  16. Li, Yi; Dong, Jin Song; Sun, Jing; Liu, Yang; Sun, Jun: Model checking approach to automated planning (2014)
  17. Llano, Maria Teresa; Ireland, Andrew; Pease, Alison: Discovery of invariants through automated theory formation (2014) ioport
  18. Hallerstede, Stefan; Leuschel, Michael; Plagge, Daniel: Validation of formal models by refinement animation (2013)
  19. Hoang, Thai Son: Security invariants in discrete transition systems (2013)
  20. Jones, Cliff B.; Freitas, Leo; Velykis, Andrius: Ours \textitisto reason why (2013)

1 2 3 next