BWare, a new research project related to the B method has started in September 2012. It is funded for a period of 4 years by the programme “Ingénierie Numérique & Sécurité” of the French national agency ANR.
This project is aimed at providing a mechanized framework to support the automated verification of proof obligations coming from the development of industrial applications using the B method. The methodology used in this project will consist in building a generic platform of verification relying on different theorem provers, such as first-order provers and SMT solvers. Beyond the multi-tool aspect of this methodology, the originality of the BWare project also resides in the requirement for the verification tools to produce proof objects, which are to be checked independently.
The BWare consortium associates several academics entities (Cedric, LRI, and Inria) and industrial partners (Mitsubishi Electric R&D Centre Europe, CLEARSY, and OCamlPro).
For further information, you can refer to the website of the project: http://bware.lri.fr/