|
 
|
[JBD13] Verifying B proof rules using deep embedding and automated theorem proving
Revue Internationale avec comité de lecture : Journal Software & Systems Modeling (SoSym), pp. online, 2013, (doi:10.1007/s10270-013-0322-z)
motcle:
Résumé:
We propose a formal and mechanized framework which consists in verifying proof rules of the B method, which cannot be automatically proved by the elementary prover of Atelier B and using an external automated theorem prover called Zenon. This framework contains in particular a set of tools, named BCARe and developed by Siemens IC-MOL, which relies on a deep embedding of the B theory within the logic of the Coq proof assistant. This toolkit allows us to automatically generate the required properties to be checked for a given proof rule. Currently, this tool chain is able to automatically verify a part of the derived rules of the B-Book, as well as some added rules coming from Atelier B and the rule database maintained by Siemens IC-MOL.
Equipe:
sys
BibTeX
| @article { | |||
| JBD13, | |||
| title | = | "{Verifying B proof rules using deep embedding and automated theorem proving}", | |
| author | = | "M. Jacquel and K. Berkani and D. Delahaye and C. Dubois", | |
| journal | = | "Software & Systems Modeling (SoSym)", | |
| year | = | 2013, | |
| pages | = | "online", | |
| doi | = | "10.1007/s10270-013-0322-z", | |
| } | |||
