Bware

It is an industrial research project that aims to
provide a mechanized framework to support the automated verification
of proof obligations coming from the development of industrial
applications using the B method and requiring high guarantees of
confidence. The methodology used in this project consists in
building a generic platform of verification relying on different
theorem provers, such as first-order provers and SMT solvers. The
variety of these theorem provers aims at allowing a wide panel of
proof obligations to be automatically verified by the platform. The
major part of the verification tools used in BWare have already been
involved in some experiments, which have consisted in verifying
proof obligations or proof rules coming from industrial
applications.
This therefore should be a driving
factor to reduce the risks of the project, which can then focus on
the design of several extensions of the verification tools to deal
with a larger amount of proof obligations.

Research activities
  Automated Proof, SMT and Applications
  Deductive Verification of Programs

Participants
CONTEJEAN Evelyne
FILLIÂTRE Jean-Christophe
MARCHÉ Claude
PASKEVYCH Andriy


More information : http://bware.lri.fr/index.php/BWare_project