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

Conférence Internationale avec comité de lecture : Abstract State Machines, Alloy, B, VDM, and Z (ABZ), June 2014, pp.-,

Auteurs: D. Delahaye , C. Dubois , C. MarchÃ© , D. MentrÃ©

Mots clés: B Method, Proof Obligations, First Order Provers, SMT Solvers, Logical Frameworks, Industrial Use, Large Scale Study

Résumé: We introduce BWare, 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 integrity. The adopted methodology consists in building a generic verification platform relying on different automated theorem provers, such as first order provers and SMT (Satisfiability Modulo Theories) solvers. Beyond the multi-tool aspect of our methodology, the originality of this project also resides in the requirement for the verification 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.

Equipe: sys

Collaboration: INRIA Saclay - Ile de France

BibTeX

@inproceedings {
	DDM14,
	title	=	"{The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations}",
	author	=	" D. Delahaye and C. Dubois and C. MarchÃ© and D. MentrÃ© ",
	booktitle	=	"{Abstract State Machines, Alloy, B, VDM, and Z (ABZ)}",
	year	=	2014,
	month	=	"June",
	pages	=	"-",
}