{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,12]],"date-time":"2026-06-12T04:35:38Z","timestamp":1781238938308,"version":"3.54.1"},"publisher-location":"Cham","reference-count":12,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319150741","type":"print"},{"value":"9783319150758","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-15075-8_1","type":"book-chapter","created":{"date-parts":[[2015,1,6]],"date-time":"2015-01-06T10:05:27Z","timestamp":1420538727000},"page":"1-16","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["LLVM-Based Code Generation for B"],"prefix":"10.1007","author":[{"given":"Richard","family":"Bonichon","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David","family":"D\u00e9harbe","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thierry","family":"Lecomte","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"suffix":"Jr","given":"Val\u00e9rio","family":"Medeiros","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,1,7]]},"reference":[{"key":"1_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. University Press, Cambridge (1996)"},{"key":"1_CR2","unstructured":"Ambert, F., Bouquet, F., Legeard, B., Peureux, F., et al.: BZ-Testing-Tools (2002)"},{"key":"1_CR3","unstructured":"Bodeveix, J.-P., Filali, M., Mu\u00f1oz, C.: A formalization of the B-method in Coq and PVS. In: Electronic Proc. B-User Group Meeting FM 99, pp. 33\u201349 (1999)"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/BFb0053356","volume-title":"B 1998: 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. 1393, pp. 66\u201382. Springer, Heidelberg (1998)"},{"key":"1_CR5","unstructured":"ClearSy. ComenC, B0 implementation translation into C language (2008). http:\/\/www.comenc.eu"},{"key":"1_CR6","unstructured":"ClearSy. Atelier B User Manual Version 4.0. Clearsy System Engineering (2009)"},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science (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. 4790, pp. 288\u2013302. Springer, Heidelberg (2007)"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Lattner, C., Adve, V.S.: LLVM: a compilation framework for lifelong program analysis & transformation. In: 2nd IEEE\/ACM International Symposium on Code Generation and Optimization, pp. 75\u201388 (2004)","DOI":"10.1109\/CGO.2004.1281665"},{"issue":"7","key":"1_CR9","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Communications of the ACM 52(7), 107\u2013115 (2009)","journal-title":"Communications of the ACM"},{"issue":"2","key":"1_CR10","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s10009-007-0063-9","volume":"10","author":"M Leuschel","year":"2008","unstructured":"Leuschel, M., Butler, M.: ProB: An automated analysis toolset for the B method. Software Tools for Technology Transfer (STTT) 10(2), 185\u2013203 (2008)","journal-title":"Software Tools for Technology Transfer (STTT)"},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-642-33296-8_6","volume-title":"Formal Methods: Foundations and Applications","author":"ECB de Matos","year":"2012","unstructured":"de Matos, E.C.B., Moreira, A.M.: Beta: A B based testing approach. In: Gheyi, R., Naumann, D. (eds.) SBMF 2012. LNCS, vol. 7498, pp. 51\u201366. Springer, Heidelberg (2012)"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Zhao, J., Nagarakatte, S., Martin, M.M.K., Zdancewic, S.: Formalizing the LLVM intermediate representation for verified program transformations. In: POPL, pp. 427\u2013440 (2012)","DOI":"10.1145\/2103621.2103709"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Foundations and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-15075-8_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,16]],"date-time":"2025-05-16T01:12:03Z","timestamp":1747357923000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-15075-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319150741","9783319150758"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-15075-8_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"7 January 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}