ProB

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

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

1 2 3 4 next

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

1 2 3 4 next