{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:58:13Z","timestamp":1762459093215},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2013,6,27]],"date-time":"2013-06-27T00:00:00Z","timestamp":1372291200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2015,2]]},"DOI":"10.1007\/s10270-013-0322-z","type":"journal-article","created":{"date-parts":[[2013,6,26]],"date-time":"2013-06-26T10:17:11Z","timestamp":1372241831000},"page":"101-119","source":"Crossref","is-referenced-by-count":4,"title":["Verifying B proof rules using deep embedding and automated theorem proving"],"prefix":"10.1007","volume":"14","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","published-online":{"date-parts":[[2013,6,27]]},"reference":[{"key":"322_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: The $$\\sf {B}$$ B -Book, Assigning Programs to Meanings. Cambridge University Press, Cambridge (UK) (1996). ISBN: 0521496195","DOI":"10.1017\/CBO9780511624162"},{"key":"322_CR2","unstructured":"Abrial, J.-R., Butler, M., Hallerstede, S., Hoang, T., Mehta, F., Voisin, L.: $$\\sf {Rodin}$$ Rodin : an open toolset for modelling and reasoning in $$\\sf {Event}$$ Event - $$\\sf {B}$$ B . Softw. Tools Technol. Transf. 12(6), 447\u2013466 (2010)"},{"key":"322_CR3","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R., Mussat, L.: On using conditional definitions in formal theories. In: Formal Specification and Development in $$\\sf {Z}$$ Z and $$\\sf {B}$$ B (ZB), vol. 2272 of LNCS, pp. 317\u2013322. Springer, Grenoble (France) Jan (2002)","DOI":"10.1007\/3-540-45648-1_13"},{"issue":"1\u20132","key":"322_CR4","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1006\/jsco.2001.0455","volume":"32","author":"H Barendregt","year":"2001","unstructured":"Barendregt, H., Cohen, A.M.: Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants. J. Symbolic Comput. 32(1\u20132), 3\u201322 (2001)","journal-title":"J. Symbolic Comput."},{"key":"322_CR5","doi-asserted-by":"crossref","unstructured":"Berkani, K., Dubois, C., Faivre, A., Falampin, J.: Validation des r\u00e8gles de base de l\u2019 $$\\sf {Atelier~B}$$ Atelier B . Technique et Science Informatiques 23(7), 855\u2013878 (2004)","DOI":"10.3166\/tsi.23.855-878"},{"key":"322_CR6","unstructured":"Bobot, F., Conchon, S., Contejean, V., Iguernelala, M., Lescuyer, S., Mebsout, A.: $$\\sf {Alt}$$ Alt - $$\\sf {Ergo}$$ Ergo , version 0.94. $$\\sf {CNRS, INRIA}$$ CNRS , INRIA , and Universit\u00e9 Paris-Sud 11. http:\/\/alt-ergo.lri.fr\/ . Dec (2011)"},{"key":"322_CR7","unstructured":"Bobot, F., Filli\u00e2tre, J.-C., March\u00e9, C., Paskevich, A.: $$\\sf {Why3}$$ Why 3 : Shepherd your herd of provers. In: International Workshop on Intermediate Verification Languages (BOOGIE), Wroc\u0142aw (Poland) Aug (2011)"},{"key":"322_CR8","unstructured":"Bodeveix, J.-P., Filali, M., Mu\u00f1oz, C.: A Formalization of the $$\\sf {B}$$ B -method in $$\\sf {Coq}$$ Coq and $$\\sf {PVS}$$ PVS . In: $$\\sf {B}$$ B Users Group Meeting, Toulouse (France) Sept (1999)"},{"key":"322_CR9","doi-asserted-by":"crossref","unstructured":"Bonichon, R., Delahaye, D., Doligez, D.: $$\\sf {Zenon}$$ Zenon : An extensible automated theorem prover producing checkable proofs. In: Logic for Programming Artificial Intelligence and Reasoning (LPAR), vol. 4790 of LNCS\/LNAI, pp. 151\u2013165. Springer, Yerevan (Armenia) Oct (2007)","DOI":"10.1007\/978-3-540-75560-9_13"},{"key":"322_CR10","doi-asserted-by":"crossref","unstructured":"Chartier, P.: Formalisation of $$\\sf {B}$$ B in $$\\sf {Isabelle\/ HOL}$$ Isabelle \/ HOL . In: $$\\sf {B}$$ B Conference, vol. 1393 of LNCS, pp. 66\u201382. Springer, Montpellier (France) Apr (1998)","DOI":"10.1007\/BFb0053356"},{"key":"322_CR11","doi-asserted-by":"crossref","unstructured":"Cirstea, H., Kirchner, C.: Using rewriting and strategies for describing the $$\\sf {B}$$ B predicate prover. In: Strategies in Automated Deduction, pp. 25\u201336. Lindau (Germany) July (1998)","DOI":"10.1007\/BFb0054239"},{"key":"322_CR12","unstructured":"$$\\sf {ClearSy: Atelier \\ B}$$ ClearSy : Atelier B 4.0. http:\/\/www.atelierb.eu\/ Feb (2009)"},{"key":"322_CR13","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, vol. 95 of ENTCS, pp. 189\u2013208. Elsevier, Campina Grande (Brazil) Oct (2003)","DOI":"10.1016\/j.entcs.2004.04.012"},{"key":"322_CR14","doi-asserted-by":"crossref","unstructured":"Delahaye, D.: A tactic language for the system $$\\sf { Coq}$$ Coq . In: Logic for Programming and Automated Reasoning (LPAR), vol. 1955 of LNCS\/LNAI, pp. 85\u201395. Springer, Reunion Island (France) Nov (2000)","DOI":"10.1007\/3-540-44404-1_7"},{"key":"322_CR15","doi-asserted-by":"crossref","unstructured":"D\u00e9harbe, D.: Automatic verification for a class of proof obligations with SMT-solvers. In: Abstract State Machines, $$\\sf {Alloy}$$ Alloy , $$\\sf {B}$$ B and $$\\sf {Z}$$ Z (ABZ), vol. 5977 of LNCS, pp. 217\u2013230. Springer, Orford (Canada, QC) Feb (2010)","DOI":"10.1007\/978-3-642-11811-1_17"},{"key":"322_CR16","doi-asserted-by":"crossref","unstructured":"Jaeger, \u00c9., Dubois, C.: Why would you trust $$\\sf {B?}$$ B ? In: Logic for Programming Artificial Intelligence and Reasoning (LPAR), vol. 4790 of LNCS\/LNAI, pp 288\u2013302. Springer, Yerevan (Armenia) Oct (2007)","DOI":"10.1007\/978-3-540-75560-9_22"},{"key":"322_CR17","doi-asserted-by":"crossref","unstructured":"Korovin, K.: $$\\sf {iProver}$$ iProver - An instantiation-based theorem prover for first-order logic (System Description). In: International Joint Conference on Automated Reasoning (IJCAR), vol. 5195 of LNCS\/LNAI, pp 292\u2013298. Springer, Sydney (Australia) Aug (2008)","DOI":"10.1007\/978-3-540-71070-7_24"},{"key":"322_CR18","unstructured":"Le Lay, \u00c9.: Automatiser la validation des r\u00e8gles. Master\u2019s thesis, $$\\sf {INSA}$$ INSA (Rennes), $$\\sf {Siemens \\ IC}$$ Siemens IC - $$\\sf {MOL}$$ MOL , Sept (2008)"},{"key":"322_CR19","doi-asserted-by":"crossref","unstructured":"Maamria, I., Butler, M., Edmunds, A., Rezazadeh, A.: On an extensible rule-based prover for $$\\sf {Event}$$ Event - $$\\sf {B}$$ B . In: Abstract State Machines, $$\\sf {Alloy}$$ Alloy , $$\\sf {B}$$ B and $$\\sf {Z}$$ Z (ABZ), vol. 5977 of LNCS, p 407. Springer, Orford (Canada, QC) Feb (2010)","DOI":"10.1007\/978-3-642-11811-1_40"},{"key":"322_CR20","doi-asserted-by":"crossref","unstructured":"McCune, W., Wos, L.: $$\\sf {Otter}$$ Otter \u2013 the CADE-13 competition incarnations. J. Autom. Reason. 18(2), 211\u2013220 (1997)","DOI":"10.1023\/A:1005843632307"},{"key":"322_CR21","doi-asserted-by":"crossref","unstructured":"Mentr\u00e9, D., March\u00e9, C., Filli\u00e2tre, J.-C., Asuka, M.: Discharging proof obligations from $$\\sf {Atelier \\ B}$$ Atelier B using multiple automated provers. In: Abstract State Machines, $$\\sf {Alloy}$$ Alloy , $$\\sf {B}$$ B and $$\\sf {Z}$$ Z (ABZ), vol. 7316 of LNCS, pp 238\u2013251. Springer, Pisa (Italy) June (2012)","DOI":"10.1007\/978-3-642-30885-7_17"},{"key":"322_CR22","doi-asserted-by":"crossref","unstructured":"Mikhailov, L., Butler, M.: An approach to combining $$\\sf {B}$$ B and $$\\sf {Alloy}$$ Alloy . In: Formal Specification and Development in $$\\sf {Z}$$ Z and $$\\sf {B}$$ B (ZB), vol. 2272 of LNCS, pp 140\u2013161. Springer, Grenoble (France) Jan (2002)","DOI":"10.1007\/3-540-45648-1_8"},{"key":"322_CR23","doi-asserted-by":"crossref","unstructured":"Riazanov, A., Voronkov, A.: $$\\sf {Vampire}$$ Vampire . In: Conference on Automated Deduction (CADE), vol. 1632 of LNCS, pp 292\u2013296. Springer, Trento (Italy) July (1999)","DOI":"10.1007\/3-540-48660-7_26"},{"key":"322_CR24","unstructured":"Schulz, S.: $$\\sf {E}$$ E \u2013 A brainiac theorem prover. AI Commun. 15(2\/3), 111\u2013126 (2002)"},{"key":"322_CR25","unstructured":"The $$\\sf {Coq}$$ Coq Development Team: $$\\sf {Coq}$$ Coq , version 8.3. $$\\sf {INRIA}$$ INRIA . http:\/\/coq.inria.fr\/ . Oct (2010)"}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-013-0322-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-013-0322-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-013-0322-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,2,26]],"date-time":"2022-02-26T12:32:04Z","timestamp":1645878724000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-013-0322-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,6,27]]},"references-count":25,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,2]]}},"alternative-id":["322"],"URL":"https:\/\/doi.org\/10.1007\/s10270-013-0322-z","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,6,27]]}}}