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.
Keywords for this software
References in zbMATH (referenced in 67 articles )
Showing results 1 to 20 of 67.
Sorted by year (- Cristiá, Maximiliano; Rossi, Gianfranco: Automated reasoning with restricted intensional sets (2021)
- Devyanin, P. N.; Leonova, M. A.: The techniques of formalization of OS Astra Linux special edition access control model using event-B formal method for verification using Rodin and prob (2021)
- Stankaitis, Paulius; Iliasov, Alexei; Kobayashi, Tsutomu; Aït-Ameur, Yamine; Ishikawa, Fuyuki; Romanovsky, Alexander: A refinement-based development of a distributed signalling system (2021)
- Cristiá, Maximiliano; Rossi, Gianfranco: Solving quantifier-free first-order constraints over finite sets and binary relations (2020)
- Lahouij, Aida; Hamel, Lazhar; Graiet, Mohamed; el Ayeb, Béchir: An Event-B based approach for cloud composite services verification (2020)
- Leuschel, Michael: Prolog for verification, analysis and transformation tools (2020)
- Liu, Yezhou; Nicolescu, Radu; Sun, Jing: Formal verification of cP systems using PAT3 and ProB (2020)
- Maximiliano Cristiá, Andrea Fois, Gianfranco Rossi: Declarative Programming with Intensional Sets in Java Using JSetL (2020) arXiv
- Borralleras, Cristina; Larraz, Daniel; Rodríguez-Carbonell, Enric; Oliveras, Albert; Rubio, Albert: Incomplete SMT techniques for solving non-linear formulas over the integers (2019)
- Kobayashi, Tsutomu; Ishikawa, Fuyuki; Honiden, Shinichi: Consistency-preserving refactoring of refinement structures in Event-B models (2019)
- Llorens, M.; Oliver, J.; Silva, J.; Tamarit, S.: Tracking CSP computations (2019)
- van der Hallen, Matthias; Paramonov, Sergey; Janssens, Gerda; Denecker, Marc: Knowledge representation analysis of graph mining (2019)
- Cristiá, Maximiliano; Rossi, Gianfranco: A set solver for finite set relation algebra (2018)
- Cristiá, Maximiliano; Rossi, Gianfranco: A decision procedure for restricted intensional sets (2017)
- Graiet, Mohamed; Hamel, Lazhar; Mammar, Amel; Tata, Samir: A verification and deployment approach for elastic component-based applications (2017)
- Dobrikov, Ivaylo; Leuschel, Michael: Optimising the ProB model checker for B using partial order reduction (2016)
- Hoang, Thai Son; Schneider, Steve; Treharne, Helen; Williams, David M.: Foundations for using linear temporal logic in Event-B refinement (2016)
- Vekris, Dimitris; Lang, Frédéric; Dima, Catalin; Mateescu, Radu: Verification of (\mathrmEB^3) specifications using CADP (2016)
- Abrial, Jean-Raymond: Definition of a mathematical language together with its proof system in Event-B (2015)
- Mammar, Amel; Frappier, Marc: Proof-based verification approaches for dynamic properties: application to the information system domain (2015)