References

  1. Jean-Raymond Abrial (2005): The B-book - assigning programs to meanings. Cambridge University Press.
  2. Clark Barrett, Pascal Fontaine & Cesare Tinelli (2015): The SMT-LIB Standard: Version 2.5. Technical Report. Department of Computer Science, The University of Iowa. Available at www.SMT-LIB.org.
  3. François Bobot, Jean-Christophe Filliâtre, Claude Marché & Andrei Paskevich (2011): Why3: Shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages, pp. 53–64.
  4. Sylvain Conchon & Mohamed Iguernelala (2014): Tuning the Alt-Ergo SMT Solver for B Proof Obligations. In: Yamine Ait Ameur & Klaus-Dieter Schewe: Abstract State Machines, Alloy, B, TLA, VDM, and Z: 4th International Conference, ABZ 2014, Toulouse, France, June 2-6, 2014. Proceedings. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 294–297, doi:10.1007/978-3-662-43652-3_27.
  5. Jean-François Couchot & Thierry Hubert (2007): A Graph-based Strategy for the Selection of Hypotheses. In: FTP'07, Int. Workshop on First-Order Theorem Proving, Liverpool, UK.
  6. David Déharbe, Pascal Fontaine, Yoann Guyot & Laurent Voisin (2012): SMT Solvers for Rodin. In: Proceedings of the Third International Conference on Abstract State Machines, Alloy, B, VDM, and Z, ABZ'12. Springer-Verlag, Berlin, Heidelberg, pp. 194–207, doi:10.1007/978-3-642-30885-7_14.
  7. David Delahaye, Catherine Dubois, Claude Marché & David Mentré (2014): The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations. In: Abstract State Machines, Alloy, B, VDM, and Z (ABZ), pp. –, doi:10.1007/978-3-662-43652-3_26.
  8. Michael Leuschel & Michael Butler (2003): ProB: A Model Checker for B. In: Keijiro Araki, Stefania Gnesi & Dino Mandrioli: FME 2003: Formal Methods: International Symposium of Formal Methods Europe, Pisa, Italy, September 8-14, 2003. Proceedings. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 855–874, doi:10.1007/978-3-540-45236-2_46.
  9. David Mentré, Claude Marché, Jean-Christophe Filliâtre & Masashi Asuka (2012): Discharging Proof Obligations from Atelier B using Multiple Automated Provers. In: Steve Reeves & Elvinia Riccobene: ABZ - 3rd International Conference on Abstract State Machines, Alloy, B and Z, Lecture Notes in Computer Science 7316. Springer, Pisa, Italy, pp. 238–251, doi:10.1007/978-3-642-30885-7_17. Available at https://hal.inria.fr/hal-00681781.
  10. BWare team (2012): The BWare Project. Available at http://bware.lri.fr/.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org