{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,6]],"date-time":"2026-01-06T05:10:16Z","timestamp":1767676216124},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642308840"},{"type":"electronic","value":"9783642308857"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-30885-7_17","type":"book-chapter","created":{"date-parts":[[2012,6,27]],"date-time":"2012-06-27T08:50:45Z","timestamp":1340787045000},"page":"238-251","source":"Crossref","is-referenced-by-count":27,"title":["Discharging Proof Obligations from Atelier\u00a0B Using Multiple Automated Provers"],"prefix":"10.1007","author":[{"given":"David","family":"Mentr\u00e9","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claude","family":"March\u00e9","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Christophe","family":"Filli\u00e2tre","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Masashi","family":"Asuka","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: The B-Book: Assigning programs to meanings. Cambridge University Press (1996)","key":"17_CR1","DOI":"10.1017\/CBO9780511624162"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/11415787_20","volume-title":"ZB 2005: Formal Specification and Development in Z and B","author":"F. Badeau","year":"2005","unstructured":"Badeau, F., Amelot, A.: Using B as a High Level Programming Language in an Industrial Project: Roissy VAL. In: Treharne, H., King, S., C. Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol.\u00a03455, pp. 334\u2013354. Springer, Heidelberg (2005)"},{"unstructured":"Barras, B.: Sets in Coq, Coq in sets. Journal of Formalized Reasoning (2010)","key":"17_CR3"},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Computer Aided Verification","author":"C.W. Barrett","year":"2007","unstructured":"Barrett, C.W., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 298\u2013302. Springer, Heidelberg (2007)"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/3-540-48119-2_22","volume-title":"FM\u201999 - Formal Methods","author":"P. Behm","year":"1999","unstructured":"Behm, P., Benoit, P., Faivre, A., Meynadier, J.-M.: M\u00e9t\u00e9or: A Successful Application of B in a Large Project. In: Wing, J.M., Woodcock, J. (eds.) FM 1999. LNCS, vol.\u00a01708, pp. 369\u2013387. Springer, Heidelberg (1999)"},{"unstructured":"Bobot, F., Filli\u00e2tre, J.-C., March\u00e9, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: Workshop on Intermediate Verification Languages (2011)","key":"17_CR6"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-642-24364-6_7","volume-title":"Frontiers of Combining Systems","author":"F. Bobot","year":"2011","unstructured":"Bobot, F., Paskevich, A.: Expressing Polymorphic Types in a Many-Sorted Language. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCos 2011. LNCS, vol.\u00a06989, pp. 87\u2013102. Springer, Heidelberg (2011)"},{"unstructured":"Bodeveix, J.-P., Filali, M., Mu\u00f1oz, C.: A formalization of the B-method in Coq and PVS. In: B-User Group Meeting, Formal Methods, pp. 33\u201349 (1999)","key":"17_CR8"},{"unstructured":"ClearSy. Language Keywords and Operators, 1.8.5 edn., \n                    \n                      http:\/\/www.tools.clearsy.com\/images\/3\/33\/Symboles_en.pdf","key":"17_CR9"},{"unstructured":"Colin, S., Mariano, G.: Coq, l\u2019alpha et l\u2019omega de la preuve pour B ? (February 2009), \n                    \n                      http:\/\/hal.archives-ouvertes.fr\/hal-00361302\/PDF\/bicoax.pdf","key":"17_CR10"},{"unstructured":"Colin, S., Petit, D., Mariano, G., Poirriez, V.: BRILLANT: an open source platform for B. In: Workshop on Tool Building in Formal Methods (February 2010)","key":"17_CR11"},{"issue":"2","key":"17_CR12","first-page":"51","volume":"198","author":"S. Conchon","year":"2008","unstructured":"Conchon, S., Contejean, E., Kanig, J., Lescuyer, S.: CC(X): Semantic combination of congruence closure with solvable theories. ENTCS\u00a0198(2), 51\u201369 (2008)","journal-title":"ENTCS"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"unstructured":"D\u00e9harbe, D.: Integration of SMT-solvers in B and Event-B development environments. Science of Computer Programming (2011)","key":"17_CR14"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-642-24690-6_18","volume-title":"Software Engineering and Formal Methods","author":"M. Jacquel","year":"2011","unstructured":"Jacquel, M., Berkani, K., Delahaye, D., Dubois, C.: Verifying B Proof Rules Using Deep Embedding and Automated Theorem Proving. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol.\u00a07041, pp. 253\u2013268. Springer, Heidelberg (2011)"},{"doi-asserted-by":"crossref","unstructured":"Milner, R.: A theory of type polymorphism in programming. Journal of Computer and System Sciences\u00a017 (1978)","key":"17_CR16","DOI":"10.1016\/0022-0000(78)90014-4"},{"unstructured":"Rocheteau, J., Colin, S., Mariano, G., Poirriez, V.: \u00c9valuation de l\u2019extensibilit\u00e9 de PhoX: B\/PhoX un assistant de preuves pour B. In: JFLA, pp. 139\u2013153 (2004)","key":"17_CR17"}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines, Alloy, B, VDM, and Z"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-30885-7_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:33:10Z","timestamp":1620127990000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-30885-7_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642308840","9783642308857"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-30885-7_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}