{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T15:45:37Z","timestamp":1725896737689},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642246890"},{"type":"electronic","value":"9783642246906"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-24690-6_18","type":"book-chapter","created":{"date-parts":[[2011,10,25]],"date-time":"2011-10-25T01:35:37Z","timestamp":1319506537000},"page":"253-268","source":"Crossref","is-referenced-by-count":5,"title":["Verifying B Proof Rules Using Deep Embedding and Automated Theorem Proving"],"prefix":"10.1007","author":[{"given":"M\u00e9lanie","family":"Jacquel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Karim","family":"Berkani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Delahaye","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Catherine","family":"Dubois","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"18_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book, Assigning Programs to Meanings","author":"J.-R. Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-Book, Assigning Programs to Meanings. Cambridge University Press, Cambridge, UK (1996) ISBN 0521496195"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/3-540-45648-1_13","volume-title":"ZB 2002: Formal Specification and Development in Z and B","author":"J.-R. Abrial","year":"2002","unstructured":"Abrial, J.-R., Mussat, L.: On Using Conditional Definitions in Formal Theories. In: Bert, D., et al. (eds.) B 2002 and ZB 2002. LNCS, vol.\u00a02272, pp. 242\u2013269. Springer, Heidelberg (2002)"},{"issue":"7","key":"18_CR3","doi-asserted-by":"publisher","first-page":"855","DOI":"10.3166\/tsi.23.855-878","volume":"23","author":"K. Berkani","year":"2004","unstructured":"Berkani, K., Dubois, C., Faivre, A., Falampin, J.: Validation des r\u00e8gles de base de l\u2019Atelier B. Technique et Science Informatiques (TSI)\u00a023(7), 855\u2013878 (2004)","journal-title":"Technique et Science Informatiques (TSI)"},{"key":"18_CR4","unstructured":"Bodeveix, J.-P., Filali, M., Mu\u00f1oz, C.: A Formalization of the B-Method in Coq and PVS. B Users Group Meeting, Toulouse, France (September 1999)"},{"key":"18_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-540-75560-9_13","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R. Bonichon","year":"2007","unstructured":"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.\u00a04790, pp. 151\u2013165. Springer, Heidelberg (2007)"},{"key":"18_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/BFb0053356","volume-title":"B\u201998: Recent Advances in the Development and Use of the B Method","author":"P. Chartier","year":"1998","unstructured":"Chartier, P.: Formalisation of B in Isabelle\/HOL. In: Bert, D. (ed.) B 1998. LNCS, vol.\u00a01393, pp. 66\u201382. Springer, Heidelberg (1998)"},{"key":"18_CR7","unstructured":"Cirstea, H., Kirchner, C.: Using Rewriting and Strategies for Describing the B Predicate Prover. In: Strategies in Automated Deduction, Lindau, Germany, pp. 25\u201336 (July 1998)"},{"key":"18_CR8","unstructured":"ClearSy. Atelier B 4.0 (February 2009), http:\/\/www.atelierb.eu\/"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"Couchot, J.-F., Dadeau, F., D\u00e9harbe, D., Giorgetti, A., Ranise, S.: Proving and Debugging Set-Based Specifications. In: Workshop on Formal Methods, Campina Grande, Brazil. ENTCS, vol.\u00a095, pp. 189\u2013208. Elsevier (October 2003)","DOI":"10.1016\/j.entcs.2004.04.012"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-642-11811-1_17","volume-title":"Abstract State Machines, Alloy, B and Z","author":"D. D\u00e9harbe","year":"2010","unstructured":"D\u00e9harbe, D.: Automatic Verification for a Class of Proof Obligations with SMT-Solvers. In: Frappier, M., Gl\u00e4sser, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol.\u00a05977, pp. 217\u2013230. Springer, Heidelberg (2010)"},{"key":"18_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-44404-1_7","volume-title":"Logic for Programming and Automated Reasoning","author":"D. Delahaye","year":"2000","unstructured":"Delahaye, D.: A Tactic Language for the System Coq. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS (LNAI), vol.\u00a01955, pp. 85\u201395. Springer, Heidelberg (2000)"},{"key":"18_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/978-3-540-75560-9_22","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"\u00c9. Jaeger","year":"2007","unstructured":"Jaeger, \u00c9., Dubois, C.: Why would you trust B? In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol.\u00a04790, pp. 288\u2013302. Springer, Heidelberg (2007)"},{"key":"18_CR13","unstructured":"Le Lay, \u00c9.: Automatiser la validation des r\u00e8gles. Master\u2019s thesis, INSA (Rennes), Siemens SAS I MO (September 2008)"},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/3-540-45648-1_8","volume-title":"ZB 2002: Formal Specification and Development in Z and B","author":"L. Mikhailov","year":"2002","unstructured":"Mikhailov, L., Butler, M.: An Approach to Combining B and Alloy. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol.\u00a02272, pp. 140\u2013161. Springer, Heidelberg (2002)"},{"key":"18_CR15","unstructured":"The Coq Development Team. Coq, version\u00a08.3. INRIA (October 2010), http:\/\/coq.inria.fr\/"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-24690-6_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,18]],"date-time":"2019-06-18T14:34:11Z","timestamp":1560868451000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24690-6_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642246890","9783642246906"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24690-6_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}