Abstract
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.
This work is supported by the BWare project (ANR-12-INSE-0010), funded for 4 years by the INS programme of the French National Research Agency (ANR) and started on September 2012. For more details, see: http://bware.lri.fr/ .
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Bobot, F., Conchon, S., Contejean, V., Iguernelala, M., Lescuyer, S., Mebsout, A.: Alt-Ergo , version 0.95.2. CNRS, Inria, and Université Paris-Sud (2013), http://alt-ergo.lri.fr
Bobot, F., Filliâtre, J.-C., Marché, C., Paskevich, A.: Why3: Shepherd Your Herd of Provers. In: Leino, K.R.M., Moskal, M. (eds.) International Workshop on Intermediate Verification Languages, Boogie, pp. 53–64 (2011)
Boespflug, M., Carbonneaux, Q., Hermant, O.: The λΠ-Calculus Modulo as a Universal Proof Language. In: Pichardie, D., Weber, T. (eds.) Proof Exchange for Theorem Proving, PxTP, vol. 878, pp. 28–43. CEUR Workshop Proceedings (2012)
Bonichon, R., Delahaye, D., Doligez, D.: Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol. 4790, pp. 151–165. Springer, Heidelberg (2007)
Burel, G.: Experimenting with Deduction Modulo. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 162–176. Springer, Heidelberg (2011)
Burel, G.: A Shallow Embedding of Resolution and Superposition Proofs into the λΠ-Calculus Modulo. In: Blanchette, J.C., Urban, J. (eds.) Proof Exchange for Theorem Proving (PxTP). EPiC, vol. 14, pp. 43–57. EasyChair (2013)
Delahaye, D., Doligez, D., Gilbert, F., Halmagrand, P., Hermant, O.: Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19. LNCS, vol. 8312, pp. 274–290. Springer, Heidelberg (2013)
Mentré, D., Marché, C., Filliâtre, J.-C., Asuka, M.: Discharging Proof Obligations from Atelier B Using Multiple Automated Provers. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 238–251. Springer, Heidelberg (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Delahaye, D., Dubois, C., Marché, C., Mentré, D. (2014). The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations. In: Ait Ameur, Y., Schewe, KD. (eds) Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2014. Lecture Notes in Computer Science, vol 8477. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-43652-3_26
Download citation
DOI: https://doi.org/10.1007/978-3-662-43652-3_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-43651-6
Online ISBN: 978-3-662-43652-3
eBook Packages: Computer ScienceComputer Science (R0)