BWare est un projet de R&D qui a démarré en Septembre 2012, pour une durée de 4 ans. Il est financé par l’ANR dans le cadre du programme « Ingénierie Numérique & Sécurité ».
Ce projet vise à fournir un environnement de preuve mécanisé pour la démonstration d’obligations de preuve issues de la méthode B. La méthodologie utilisée dans ce projet repose sur la construction d’une plateforme de vérification générique s’appuyant sur plusieurs prouveurs de théorèmes, tels que des prouveurs du premier ordre ou des SMT solveurs. Au delà de l’aspect multi-outils de cette méthodologie, l’originalité de BWare réside aussi dans l’exigence pour les outils de vérification de fournir des objets de preuve qui pourront être vérifiés indépendamment.
Le consortium BWare regroupe des partenaires académiques (Cedric, LRI et Inria) et industriels (Mitsubishi Electric R&D Europe, CLEARSY et OcamlPro).
Plus d’information sur le site: http://bware.lri.fr