In 2011, in collaboration with Jean-Christophe Filliâtre and Claude Marché of ProVal team at INRIA/LRI and Masashi Asuka of my company, we have plugged Why3 proof tool-chain into Atelier B. More exactly, we wrote a tool called bpo2why and associated Why3 theories to transform Proof Obligations generated by Atelier B into Why3 verification conditions. Those verification conditions can then be checked with several automatic provers (we have used Alt-Ergo, CVC3 and Z3). Overall, we are quite satisfied with the result, the automatic provers of Why3 proof tool-chain proving more proof obligations that native Atelier B automatic prover (F0 and F1). We made an article about this work and this article has been accepted at ABZ 2012 conference! :-)

For further details, just read "Discharging Proof Obligations from Atelier B using Multiple Automated Provers" (PDF).