@book(bbook,
 author       = {Jean{-}Raymond Abrial},
 year         = {2005},
 title        = {The B-book - assigning programs to meanings},
 publisher    = {Cambridge University Press},
)
@techreport(BarFT-RR-15,
 author       = {Clark Barrett and Pascal Fontaine and Cesare Tinelli},
 year         = {2015},
 title        = {{The SMT-LIB Standard: Version 2.5}},
 type         = {Technical Report},
 institution  = {Department of Computer Science, The University of Iowa},
 note         = {Available at {\tt www.SMT-LIB.org}},
)
@inproceedings(bobot2011why3,
 author       = {Fran{\c{c}}ois Bobot and Jean-Christophe Filli{\^a}tre and Claude March{\'e} and Andrei Paskevich},
 year         = {2011},
 title        = {Why3: Shepherd your herd of provers},
 booktitle    = {Boogie 2011: First International Workshop on Intermediate Verification Languages},
 pages        = {53--64},
)
@inproceedings(Conchon2014,
 author       = {Sylvain Conchon and Mohamed Iguernelala},
 year         = {2014},
 title        = {Tuning the Alt-Ergo SMT Solver for B Proof Obligations},
 editor       = {Ait Ameur, Yamine and Klaus-Dieter Schewe},
 booktitle    = {Abstract State Machines, Alloy, B, TLA, VDM, and Z: 4th International Conference, ABZ 2014, Toulouse, France, June 2-6, 2014. Proceedings},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {294--297},
 doi          = {10.1007/978-3-662-43652-3_27},
)
@inproceedings(ch07:bl,
 author       = {Jean-Fran\c{c}ois Couchot and Thierry Hubert},
 year         = {2007},
 title        = {A Graph-based Strategy for the Selection of Hypotheses},
 booktitle    = {FTP'07, Int. Workshop on First-Order Theorem Proving},
 address      = {Liverpool, UK},
)
@inproceedings(Deharbe:2012:SSR:2345997.2346015,
 author       = {David D{\'e}harbe and Pascal Fontaine and Yoann Guyot and Laurent Voisin},
 year         = {2012},
 title        = {SMT Solvers for Rodin},
 booktitle    = {Proceedings of the Third International Conference on Abstract State Machines, Alloy, B, VDM, and Z},
 series       = {ABZ'12},
 publisher    = {Springer-Verlag},
 address      = {Berlin, Heidelberg},
 pages        = {194--207},
 doi          = {10.1007/978-3-642-30885-7_14},
)
@inproceedings(DDM14,
 author       = {David Delahaye and Catherine Dubois and March\IeC{\'e}, Claude and Mentr\IeC{\'e}, David},
 year         = {2014},
 title        = {{The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations}},
 booktitle    = {{Abstract State Machines, Alloy, B, VDM, and Z (ABZ)}},
 pages        = {--},
 doi          = {10.1007/978-3-662-43652-3_26},
)
@inproceedings(leuschel2003prob,
 author       = {Michael Leuschel and Michael Butler},
 year         = {2003},
 title        = {ProB: A Model Checker for B},
 editor       = {Keijiro Araki and Stefania Gnesi and Dino Mandrioli},
 booktitle    = {FME 2003: Formal Methods: International Symposium of Formal Methods Europe, Pisa, Italy, September 8-14, 2003. Proceedings},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 pages        = {855--874},
 doi          = {10.1007/978-3-540-45236-2_46},
)
@inproceedings(mentre:hal-00681781,
 author       = {David Mentr{\'e} and Claude March{\'e} and Jean-Christophe Filli{\^a}tre and Masashi Asuka},
 year         = {2012},
 title        = {{Discharging Proof Obligations from Atelier B using Multiple Automated Prover}s},
 editor       = {Steve Reeves and Elvinia Riccobene},
 booktitle    = {{ABZ - 3rd International Conference on Abstract State Machines, Alloy, B and Z}},
 series       = {Lecture Notes in Computer Science},
 volume       = {7316},
 publisher    = {{Springer}},
 address      = {Pisa, Italy},
 pages        = {238--251},
 doi          = {10.1007/978-3-642-30885-7_17},
 url          = {https://hal.inria.fr/hal-00681781},
)
@misc(Bware,
 author       = {BWare team},
 year         = {2012},
 title        = {The {BWare Project}},
 url          = {http://bware.lri.fr/},
)