Anzeige
Erschienen in:
2014 | OriginalPaper | Buchkapitel
The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations
verfasst von : David Delahaye, Catherine Dubois, Claude Marché, David Mentré
Erschienen in: Abstract State Machines, Alloy, B, TLA, VDM, and Z
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.