References

  1. Jean-Raymond Abrial (2005): The B-book - assigning programs to meanings. Cambridge University Press.
  2. Jean-Raymond Abrial, Michael Butler, Stefan Hallerstede, Thai Son Hoang, Farhad Mehta & Laurent Voisin (2010): Rodin: an open toolset for modelling and reasoning in Event-B. STTT 12(6), pp. 447–466. Available at http://dx.doi.org/10.1007/s10009-010-0145-y.
  3. Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds & Cesare Tinelli (2011): CVC4. In: CAV, pp. 171–177. Available at http://dx.doi.org/10.1007/978-3-642-22110-1_14.
  4. Jens Bendisposto, Michael Leuschel, O. Ligot & Mireille Samia (2008): La validation de modèles Event-B avec le plug-in ProB pour RODIN. Technique et Science Informatiques 27(8), pp. 1065–1084. Available at http://dx.doi.org/10.3166/tsi.27.1065-1084.
  5. ClearSy System Engineering, Aix-en-Provence: Atelier B - User Manual. Available at http://www.atelierb.eu/manuels/manuel-utilisateur-atelier-b-4.0-en.pdf.
  6. David Déharbe, Pascal Fontaine, Yoann Guyot & Laurent Voisin (2012): SMT Solvers for Rodin. In: ABZ, pp. 194–207. Available at http://dx.doi.org/10.1007/978-3-642-30885-7_14.
  7. Michael Leuschel (2011): User Manual. Available at http://www.stups.uni-duesseldorf.de/ProB/index.php5/User_Manual.
  8. Michael Leuschel & Michael J. Butler (2003): ProB: A Model Checker for B.. In: FME, pp. 855–874. Available at http://dx.doi.org/10.1007/978-3-540-45236-2_46.
  9. Olivier Ligot, Jens Bendisposto & Michael Leuschel (2007): Debugging Event-B Models using the ProB Disprover Plug-in. Proceedings AFADL'07.
  10. Valério G. Medeiros Jr. & David Déharbe (2012): Experience in Modeling a Microcontroller Instruction Set Using B. In: Brazilian Symposium on Formal Methods. SBMF, Natal - RN.
  11. Leonardo Mendonça de Moura & Nikolaj Bjørner (2008): Z3: An Efficient SMT Solver. In: TACAS, pp. 337–340. Available at http://dx.doi.org/10.1007/978-3-540-78800-3_24.
  12. Daniel Plagge & Michael Leuschel (2012): Validating B, Z and TLA + Using ProB and Kodkod. In: FM, pp. 372–386. Available at http://dx.doi.org/10.1007/978-3-642-32759-9_31.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org