{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:06:15Z","timestamp":1742911575899,"version":"3.40.3"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031172434"},{"type":"electronic","value":"9783031172441"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-17244-1_20","type":"book-chapter","created":{"date-parts":[[2022,10,9]],"date-time":"2022-10-09T19:33:23Z","timestamp":1665344003000},"page":"334-351","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Model Checking B Models via\u00a0High-Level Code Generation"],"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":"Brandt","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":[[2022,10,10]]},"reference":[{"key":"20_CR1","volume-title":"The B-Book: Assigning Programs to Meanings","author":"J Abrial","year":"2005","unstructured":"Abrial, J., Hoare, A.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)"},{"key":"20_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"key":"20_CR3","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Bendisposto, J., et al: Symbolic Reachability Analysis of B Through ProB and LTSmin. ArXiv, abs\/1603.04401 (2016)","DOI":"10.1007\/978-3-319-33693-0_18"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"Bendisposto, J., Krings, S., Leuschel, M.: Who watches the watchers: validating the prob validation tool. In: Proceedings F-IDE, EPTCS 149. Electronic Proceedings in Theoretical Computer Science (2014)","DOI":"10.4204\/EPTCS.149.3"},{"key":"20_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-642-10373-5_26","volume-title":"Formal Methods and Software Engineering","author":"J Bendisposto","year":"2009","unstructured":"Bendisposto, J., Leuschel, M.: Proof assisted model checking for B. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 504\u2013520. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-10373-5_26"},{"key":"20_CR7","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). https:\/\/doi.org\/10.1007\/978-3-319-57288-8_21"},{"key":"20_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). https:\/\/doi.org\/10.1007\/978-3-319-40648-0_13"},{"key":"20_CR9","unstructured":"ClearSy. Atelier B, User and Reference Manuals. Aix-en-Provence, France (2016). http:\/\/www.atelierb.eu\/"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-319-96145-3_10","volume-title":"Computer Aided Verification","author":"L Cordeiro","year":"2018","unstructured":"Cordeiro, L., Kesseli, P., Kroening, D., Schrammel, P., Trtik, M.: JBMC: a bounded model checking tool for verifying java bytecode. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 183\u2013190. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_10"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-642-16164-3_9","volume-title":"Model Checking Software","author":"M de Jonge","year":"2010","unstructured":"de Jonge, M., Ruys, T.C.: The SpinJa model checker. In: van de Pol, J., Weber, M. (eds.) SPIN 2010. LNCS, vol. 6349, pp. 124\u2013128. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16164-3_9"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Dobrikov, I., Leuschel, M.: Enabling analysis for event-B. In: Proceedings ABZ, pp. 102\u2013118 (2016)","DOI":"10.1007\/978-3-319-33600-8_6"},{"key":"20_CR13","doi-asserted-by":"publisher","unstructured":"Edmunds, A.: Templates for event-B code generation. In : Ait Ameur, Y., Schewe, K.D. (eds) Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2014. Lecture Notes in Computer Science, vol. 8477, pp. 284\u2013289. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-43652-3_25","DOI":"10.1007\/978-3-662-43652-3_25"},{"key":"20_CR14","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). https:\/\/doi.org\/10.1007\/978-3-319-10181-1_20"},{"key":"20_CR15","first-page":"40","volume-title":"Proceedings ABZ, LNCS","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.) Proceedings ABZ, LNCS, vol. 8477, pp. 40\u201355. Springer, Heidelberg (2014)"},{"key":"20_CR16","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"G Holzmann","year":"2011","unstructured":"Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual, 1st edn. Addison-Wesley Professional, Boston (2011)","edition":"1"},{"key":"20_CR17","unstructured":"J\u00f8rgensen, P.W.V., Larsen, M., Couto, L.D.: A code generation platform for VDM. In: Proceedings of the 12th Overture Workshop. School of Computing Science, Newcastle University, UK, Technical Report CS-TR-1446 (2015)"},{"key":"20_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"692","DOI":"10.1007\/978-3-662-46681-0_61","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Kant","year":"2015","unstructured":"Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: LTSmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 692\u2013707. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_61"},{"key":"20_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-319-98938-9_16","volume-title":"Integrated Formal Methods","author":"P K\u00f6rner","year":"2018","unstructured":"K\u00f6rner, P., Leuschel, M., Meijer, J.: State-of-the-art model checking for B and event-B using ProB and LTSmin. In: Furia, C.A., Winter, K. (eds.) IFM 2018. LNCS, vol. 11023, pp. 275\u2013295. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-98938-9_16"},{"key":"20_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/978-3-642-54862-8_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Kroening","year":"2014","unstructured":"Kroening, D., Tautschnig, M.: CBMC \u2013 C bounded model checker. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389\u2013391. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_26"},{"issue":"2","key":"20_CR21","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/s10009-015-0395-9","volume":"19","author":"L Ladenberger","year":"2015","unstructured":"Ladenberger, L., Hansen, D., Wiegard, H., Bendisposto, J., Leuschel, M.: Validation of the ABZ landing gear system using ProB. Int. J. Softw. Tools Technol. Transf. 19(2), 187\u2013203 (2015). https:\/\/doi.org\/10.1007\/s10009-015-0395-9","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"20_CR22","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/978-3-031-07727-2_8","volume-title":"Proceedings iFM","author":"M Leuschel","year":"2022","unstructured":"Leuschel, M.: Operation Caching and State Compression for Model Checking of High-Level Models - How to have your cake and eat it. In: Proceedings iFM. LNCS, vol. 13274, pp. 129\u2013145. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-07727-2_8"},{"key":"20_CR23","unstructured":"Leuschel, M., Bendisposto, J., Hansen, D.: Unlocking the mysteries of a formal model of an interlocking system. In: Proceedings Rodin Workshop (2014)"},{"key":"20_CR24","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). https:\/\/doi.org\/10.1007\/978-3-540-45236-2_46"},{"key":"20_CR25","doi-asserted-by":"crossref","unstructured":"Mehlitz, P., Rungta, N., Visser, W.: A hands-on Java Pathfinder tutorial. In: Proceedings ICSE, pp. 1493\u20131495 (2013)","DOI":"10.1109\/ICSE.2013.6606756"},{"key":"20_CR26","doi-asserted-by":"crossref","unstructured":"M\u00e9ry, D., Singh, N.K.: Automatic code generation from event-B models. In: Proceedings SoICT, pp. 179\u2013188. ACM ICPS (2011)","DOI":"10.1145\/2069216.2069252"},{"key":"20_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/11955757_20","volume-title":"B 2007: Formal Specification and Development in B","author":"I Oliver","year":"2006","unstructured":"Oliver, I.: Experiences in using B and UML in industrial development. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol. 4355, pp. 248\u2013251. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11955757_20"},{"key":"20_CR28","unstructured":"Parr, T.: StringTemplate Website. http:\/\/www.stringtemplate.org\/ (2013). Accessed 23 Sep 2021"},{"issue":"1","key":"20_CR29","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":"20_CR30","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/j.entcs.2013.07.007","volume":"296","author":"FI van der Berg","year":"2013","unstructured":"van der Berg, F.I., Laarman, A.: SpinS: extending LTSmin with Promela through SpinJa. Electron. Notes Theor. Comput. Sci. 296, 95\u2013105 (2013)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"20_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"456","DOI":"10.1007\/978-3-030-34968-4_25","volume-title":"Integrated Formal Methods","author":"F Vu","year":"2019","unstructured":"Vu, F., Hansen, D., K\u00f6rner, P., Leuschel, M.: A multi-target code generator for high-level B. In: Ahrendt, W., Tapia Tarifa, S.L. (eds.) IFM 2019. LNCS, vol. 11918, pp. 456\u2013473. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-34968-4_25"},{"key":"20_CR32","doi-asserted-by":"crossref","unstructured":"Vu, F., Happe, C., Leuschel, M.: Generating domain-specific interactive validation documents. In: Proceedings FMICS, pp. 32\u201349 (2022). To appear in LNCS 13487","DOI":"10.1007\/978-3-031-15008-1_4"},{"key":"20_CR33","unstructured":"Witulski, J.: A Python B Implementation - PyB A Second Tool-Chain. PhD thesis, Universit\u00e4ts-und Landesbibliothek der Heinrich-Heine-Universit\u00e4t D\u00fcsseldorf (2018)"},{"key":"20_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/3-540-48153-2_6","volume-title":"Correct Hardware Design and Verification Methods","author":"Y Yu","year":"1999","unstructured":"Yu, Y., Manolios, P., Lamport, L.: Model checking TLA+ specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 54\u201366. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48153-2_6"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-17244-1_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,28]],"date-time":"2023-01-28T12:26:19Z","timestamp":1674908779000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-17244-1_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031172434","9783031172441"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-17244-1_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"10 October 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICFEM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Engineering Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Madrid","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 October 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 October 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"icfem2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/maude.ucm.es\/ICFEM22\/index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"61","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"23","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"38% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3 invited papers (two papers and one abstract)","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}