{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T06:56:04Z","timestamp":1757573764836,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":8,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662436516"},{"type":"electronic","value":"9783662436523"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-43652-3_26","type":"book-chapter","created":{"date-parts":[[2014,5,29]],"date-time":"2014-05-29T02:22:12Z","timestamp":1401330132000},"page":"290-293","source":"Crossref","is-referenced-by-count":13,"title":["The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations"],"prefix":"10.1007","author":[{"given":"David","family":"Delahaye","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Catherine","family":"Dubois","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claude","family":"March\u00e9","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Mentr\u00e9","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"26_CR1","unstructured":"Bobot, F., Conchon, S., Contejean, V., Iguernelala, M., Lescuyer, S., Mebsout, A.: Alt-Ergo , version\u00a00.95.2. CNRS, Inria, and Universit\u00e9 Paris-Sud (2013), http:\/\/alt-ergo.lri.fr"},{"key":"26_CR2","unstructured":"Bobot, F., Filli\u00e2tre, J.-C., March\u00e9, 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\u201364 (2011)"},{"key":"26_CR3","unstructured":"Boespflug, M., Carbonneaux, Q., Hermant, O.: The \u03bb\u03a0-Calculus Modulo as a Universal Proof Language. In: Pichardie, D., Weber, T. (eds.) Proof Exchange for Theorem Proving, PxTP, vol.\u00a0878, pp. 28\u201343. CEUR Workshop Proceedings (2012)"},{"key":"26_CR4","series-title":"LNAI","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":"26_CR5","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-642-22438-6_14","volume-title":"Automated Deduction \u2013 CADE-23","author":"G. Burel","year":"2011","unstructured":"Burel, G.: Experimenting with Deduction Modulo. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol.\u00a06803, pp. 162\u2013176. Springer, Heidelberg (2011)"},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"Burel, G.: A Shallow Embedding of Resolution and Superposition Proofs into the \u03bb\u03a0-Calculus Modulo. In: Blanchette, J.C., Urban, J. (eds.) Proof Exchange for Theorem Proving (PxTP). EPiC, vol.\u00a014, pp. 43\u201357. EasyChair (2013)","DOI":"10.29007\/ftc2"},{"key":"26_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-642-45221-5_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D. Delahaye","year":"2013","unstructured":"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.\u00a08312, pp. 274\u2013290. Springer, Heidelberg (2013)"},{"key":"26_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/978-3-642-30885-7_17","volume-title":"Abstract State Machines, Alloy, B, VDM, and Z","author":"D. Mentr\u00e9","year":"2012","unstructured":"Mentr\u00e9, D., March\u00e9, C., Filli\u00e2tre, J.-C., Asuka, M.: Discharging Proof Obligations from Atelier\u00a0B Using Multiple Automated Provers. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol.\u00a07316, pp. 238\u2013251. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines, Alloy, B, TLA, VDM, and Z"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-43652-3_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,3]],"date-time":"2025-05-03T04:46:56Z","timestamp":1746247616000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-43652-3_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783662436516","9783662436523"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-43652-3_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}