Why3 as another proof toolchain for Atelier B

In 2011,  Why3 proof tool-chain has been plugged into Atelier B, in order to transform Proof Obligations generated by Atelier B into Why3 verification conditions. 

Those verification conditions can then be checked with several automatic provers (Alt-Ergo, CVC3 and Z3). Overall, the automatic provers of Why3 proof tool-chain prove more proof obligations that native Atelier B automatic prover (F0 and F1). An article on this topic has been accepted at ABZ 2012 conference.

Source: http://bentobako.org/david/blog/index.php?post/2012/03/11/New-paper-accepted-on-use-of-Why3-as-another-toolchain-for-Atelier-B

Ce contenu a été publié dans Research, Tools. Vous pouvez le mettre en favoris avec ce permalien.

1 réponse à Why3 as another proof toolchain for Atelier B

  1. interested dit :

    Any plan to integrate these tools with Atelier B ?

Laisser un commentaire