{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,8]],"date-time":"2025-09-08T06:55:57Z","timestamp":1757314557476,"version":"3.37.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030349677"},{"type":"electronic","value":"9783030349684"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"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":[[2019]]},"DOI":"10.1007\/978-3-030-34968-4_25","type":"book-chapter","created":{"date-parts":[[2019,11,21]],"date-time":"2019-11-21T19:14:54Z","timestamp":1574363694000},"page":"456-473","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["A Multi-target Code Generator for High-Level B"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2556-5553","authenticated-orcid":false,"given":"Fabian","family":"Vu","sequence":"first","affiliation":[]},{"given":"Dominik","family":"Hansen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7256-9560","authenticated-orcid":false,"given":"Philipp","family":"K\u00f6rner","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4595-1518","authenticated-orcid":false,"given":"Michael","family":"Leuschel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,11,22]]},"reference":[{"key":"25_CR1","unstructured":"Abrial, J., Hoare, A.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)"},{"key":"25_CR2","unstructured":"Sethi, R., Aho, A.V., Lam, M.S.: The structure of a compiler. In: Compilers Principles, Techniques & Tools, 2nd edn. Addison Wesley, Boston (1986)"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Backhouse, R., Gibbons, J.: Generic Programming. Springer, Heidelberg (2003)","DOI":"10.1007\/b12027"},{"key":"25_CR4","unstructured":"Bagwell, P.: Ideal Hash Trees. Es Grands Champs, 1195 (2001)"},{"key":"25_CR5","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"25_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-319-57288-8_21","volume-title":"NASA Formal Methods","author":"S Bonfanti","year":"2017","unstructured":"Bonfanti, S., Carissoni, M., Gargantini, A., Mashkoor, A.: Asm2C++: a tool for code generation from abstract state machines to arduino. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 295\u2013301. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-57288-8_21"},{"key":"25_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-15075-8_1","volume-title":"Formal Methods: Foundations and Applications","author":"R Bonichon","year":"2015","unstructured":"Bonichon, R., D\u00e9harbe, D., Lecomte, T., Medeiros, V.: LLVM-based code generation for B. In: Braga, C., Mart\u00ed-Oliet, N. (eds.) SBMF 2014. LNCS, vol. 8941, pp. 1\u201316. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-15075-8_1"},{"key":"25_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-319-40648-0_13","volume-title":"NASA Formal Methods","author":"N Cata\u00f1o","year":"2016","unstructured":"Cata\u00f1o, N., Rivera, V.: EventB2Java: a code generator for event-B. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 166\u2013171. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-40648-0_13"},{"key":"25_CR9","unstructured":"ClearSy. Atelier B, User and Reference Manuals. Aix-en-Provence, France (2016). \nhttp:\/\/www.atelierb.eu\/"},{"key":"25_CR10","doi-asserted-by":"crossref","unstructured":"Doll\u00e9, D., Essam\u00e9, D., Falampin, J.: B dans le transport ferroviaire. L\u2019exp\u00e9rience de Siemens Transportation Systems. Technique et Science Informatiques 22(1), 11\u201332 (2003)","DOI":"10.3166\/tsi.22.11-32"},{"key":"25_CR11","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/978-3-662-43652-3_25","volume-title":"ABZ 2014","author":"A Edmunds","year":"2014","unstructured":"Edmunds, A.: Templates for event-B code generation. In: Ait Ameur, Y., Schewe, K.D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 284\u2013289. Springer, Heidelberg (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-662-43652-3_25"},{"key":"25_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/11955757_21","volume-title":"B 2007: Formal Specification and Development in B","author":"D Essam\u00e9","year":"2006","unstructured":"Essam\u00e9, D., Doll\u00e9, D.: B in large-scale projects: the canarsie line CBTC experience. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol. 4355, pp. 252\u2013254. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11955757_21"},{"key":"25_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/978-3-319-10181-1_20","volume-title":"Integrated Formal Methods","author":"A F\u00fcrst","year":"2014","unstructured":"F\u00fcrst, A., Hoang, T.S., Basin, D., Desai, K., Sato, N., Miyazaki, K.: Code generation for event-B. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 323\u2013338. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-10181-1_20"},{"key":"25_CR14","unstructured":"Granlund, T.: GNU MP. The GNU Multiple Precision Arithmetic Library, vol. 2, no. 2 (1996)"},{"key":"25_CR15","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-662-43652-3_4","volume-title":"ABZ 2014","author":"D Hansen","year":"2014","unstructured":"Hansen, D., Leuschel, M.: Translating B to TLA + for validation with TLC. In: Ait Ameur, Y., Schewe, K.D. (eds.) ABZ 2014. LNCS, vol. 8477, pp. 40\u201355. Springer, Heidelberg (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-662-43652-3_4"},{"key":"25_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-319-91271-4_20","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"D Hansen","year":"2018","unstructured":"Hansen, D., et al.: Using a formal B model at runtime in a demonstration of the ETCS hybrid level 3 concept with real trains. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) ABZ 2018. LNCS, vol. 10817, pp. 292\u2013306. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-91271-4_20"},{"key":"25_CR17","doi-asserted-by":"crossref","unstructured":"Hickey, R.: The Clojure programming language. In: Proceedings of DLS. ACM (2008)","DOI":"10.1145\/1408681.1408682"},{"key":"25_CR18","unstructured":"Hunt, A., Thomas, D.: The evils of duplication. In: The Pragmatic Programmer: From Journeyman to Master, p. 26. The Pragmatic Bookshelf (1999)"},{"key":"25_CR19","unstructured":"J\u00f8rgensen, P.W.V., Larsen, M., Couto, L.D.: A code generation platform for VDM. In: Battle, N., Fitzgerald, J. (eds.) Proceedings of the 12th Overture Workshop. School of Computing Science, Newcastle University, UK, Technical report CS-TR-1446, January 2015"},{"key":"25_CR20","first-page":"31-1-31-26","volume-title":"Handbook of Data Structures and Applications","author":"Haim Kaplan","year":"2004","unstructured":"Kaplan, H.: Persistent data structures. In: Handbook of Data Structures and Applications (2004)"},{"key":"25_CR21","unstructured":"Krings, S.: Towards infinite-state symbolic model checking for B and event-B. Ph.D. thesis, Heinrich Heine Universit\u00e4t D\u00fcsseldorf, August 2017"},{"key":"25_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-030-30942-8_31","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"P K\u00f6rner","year":"2019","unstructured":"K\u00f6rner, P., Bendisposto, J., Dunkelau, J., Krings, S., Leuschel, M.: Embedding high-level formal specifications into applications. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 519\u2013535. Springer, Cham (2019). \nhttps:\/\/doi.org\/10.1007\/978-3-030-30942-8_31"},{"key":"25_CR23","unstructured":"Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc. (2002)"},{"key":"25_CR24","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: 33rd Symposium Principles of Programming Languages, POPL, pp. 42\u201354. ACM Press (2006)","DOI":"10.1145\/1111320.1111042"},{"key":"25_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"FME 2003: Formal Methods","author":"M Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855\u2013874. Springer, Heidelberg (2003). \nhttps:\/\/doi.org\/10.1007\/978-3-540-45236-2_46"},{"issue":"12","key":"25_CR26","first-page":"2350","volume":"48","author":"Atif Mashkoor","year":"2018","unstructured":"Mashkoor, A., Kossak, F., Egyed, A.: Evaluating the suitability of state-based formal methods for industrial deployment. Softw. Pract. Exper. 48(12), 2350\u20132379 (2018)","journal-title":"Software: Practice and Experience"},{"key":"25_CR27","doi-asserted-by":"crossref","unstructured":"M\u00e9ry, D., Singh, N.K.: Automatic code generation from event-B models. In: Proceedings SoICT 2011, pp. 179\u2013188. ACM ICPS (2011)","DOI":"10.1145\/2069216.2069252"},{"key":"25_CR28","unstructured":"Parr, T.: Enforcing Strict Model-View Separation in Template Engines. \nhttps:\/\/www.cs.usfca.edu\/~parrt\/papers\/mvc.templates.pdf\n\n. Accessed 14 May 2019"},{"issue":"1","key":"25_CR29","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/s10009-009-0132-3","volume":"12","author":"Daniel Plagge","year":"2009","unstructured":"Plagge, D., Leuschel, M.: Seven at a stroke: LTL model checking for high-level specifications in B, Z, CSP, and more. Int. J. Softw. Tools Technol. Transf. 12, 9\u201321 (2007)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"ICFP","key":"25_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3110260","volume":"1","author":"Juan Pedro Bol\u00edvar Puente","year":"2017","unstructured":"Puente, J.P.B.: Persistence for the masses: RRB-vectors in a systems language. In: Proceedings of ACM Programming Languages, vol. 1, no. ICFP, pp. 16:1\u201316:28 (2017)","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"25_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-540-87603-8_33","volume-title":"Abstract State Machines, B and Z","author":"A Requet","year":"2008","unstructured":"Requet, A.: BART: a tool for automatic refinement. In: B\u00f6rger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 345\u2013345. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-87603-8_33"},{"issue":"1","key":"25_CR32","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10009-015-0381-2","volume":"19","author":"V Rivera","year":"2017","unstructured":"Rivera, V., Cata\u00f1o, N., Wahls, T., Rueda, C.: Code generation for Event-B. STTT 19(1), 31\u201352 (2017)","journal-title":"STTT"},{"key":"25_CR33","unstructured":"Voisinet, J.-C.: JBTools: an experimental platform for the formal B method. In: Proceedings of the Inaugural International Symposium on Principles and Practice of Programming in Java, pp. 137\u2013139 (2002)"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-34968-4_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,21]],"date-time":"2019-11-21T19:19:08Z","timestamp":1574363948000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-34968-4_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030349677","9783030349684"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-34968-4_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"22 November 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Integrated Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bergen","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Norway","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 December 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 December 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ifm2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/ifm2019.hvl.no\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}