The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations

Abstract : We introduce BWare, an industrial research project that aims to provide a mechanized framework to support the automated veri cation of proof obligations coming from the development of industrial applications using the B method and requiring high integrity. The methodology adopted consists in building a generic veri cation platform relying on di erent theorem provers, such as rst order provers and SMT (Satisfi ability Modulo Theories) solvers. Beyond the multi-tool aspect of our methodology, the originality of this project also resides in the requirement for the veri cation tools to produce proof objects, which are to be checked independently. In this paper, we present some preliminary results of BWare, as well as some current major lines of work.
Type de document :
Communication dans un congrès
Abstract State Machines, Alloy, B, VDM, and Z, Jun 2014, Toulouse, France. Springer, 8477, pp.290-293, 2014, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/hal-00998092
Contributeur : Claude Marché <>
Soumis le : vendredi 30 mai 2014 - 14:20:34
Dernière modification le : mardi 10 juillet 2018 - 17:02:03
Document(s) archivé(s) le : samedi 30 août 2014 - 10:43:02

Fichier

bware_ABZ_14_.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00998092, version 1

Collections

Citation

David Delahaye, Catherine Dubois, Claude Marché, David Mentré. The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations. Abstract State Machines, Alloy, B, VDM, and Z, Jun 2014, Toulouse, France. Springer, 8477, pp.290-293, 2014, Lecture Notes in Computer Science. 〈hal-00998092〉

Partager

Métriques

Consultations de la notice

678

Téléchargements de fichiers

110