{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T13:55:13Z","timestamp":1743083713348,"version":"3.40.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031765537"},{"type":"electronic","value":"9783031765544"}],"license":[{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-76554-4_4","type":"book-chapter","created":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T11:18:19Z","timestamp":1731410299000},"page":"53-74","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["VeriCode: Correct Translation of\u00a0Abstract Specifications to\u00a0C Code"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6712-7178","authenticated-orcid":false,"given":"Gerhard","family":"Schellhorn","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4596-2305","authenticated-orcid":false,"given":"Stefan","family":"Bodenm\u00fcller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4086-0043","authenticated-orcid":false,"given":"Wolfgang","family":"Reif","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,11,13]]},"reference":[{"key":"4_CR1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-745-5","volume-title":"Verification of Sequential and Concurrent Programs","author":"KR Apt","year":"2009","unstructured":"Apt, K.R., de Boer, F.S., Olderog, E.-R.: Verification of Sequential and Concurrent Programs, 3rd edn. Springer, London (2009). https:\/\/doi.org\/10.1007\/978-1-84882-745-5","edition":"3"},{"key":"4_CR2","doi-asserted-by":"publisher","unstructured":"Bagnara, R., Bagnara, A., Hill, P.M.: The MISRA C coding standard and its role in the development and analysis of safety- and security-critical embedded software. In: Podelski, A. (ed.) SAS 2018. LNCS, vol. 11002, pp. 5\u201323. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-99725-4_2","DOI":"10.1007\/978-3-319-99725-4_2"},{"key":"4_CR3","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"issue":"8","key":"4_CR4","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1145\/3470569","volume":"64","author":"P Baudin","year":"2021","unstructured":"Baudin, P., et al.: The dogged pursuit of bug-free C programs: the Frama-C software analysis platform. Commun. ACM 64(8), 56\u201368 (2021)","journal-title":"Commun. ACM"},{"key":"4_CR5","series-title":"Texts in Theoretical Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Texts in Theoretical Computer Science, Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-662-07964-5"},{"key":"4_CR6","doi-asserted-by":"publisher","unstructured":"Bodenm\u00fcller, S., Schellhorn, G., Bitterlich, M., Reif, W.: Flashix: modular Verification of a Concurrent and Crash-Safe Flash File System. In: Raschke, A., Riccobene, E., Schewe, K.-D. (eds.) Logic, Computation and Rigorous Methods. LNCS, vol. 12750, pp. 239\u2013265. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-76020-5_14","DOI":"10.1007\/978-3-030-76020-5_14"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/3-540-45587-6_3","volume-title":"Practical Aspects of Declarative Languages","author":"RS Boyer","year":"2002","unstructured":"Boyer, R.S., Strother Moore, J.: Single-threaded objects in ACL2. In: Krishnamurthi, S., Ramakrishnan, C.R. (eds.) PADL 2002. LNCS, vol. 2257, pp. 9\u201327. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45587-6_3"},{"key":"4_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem Proving in Higher Order Logics","author":"E Cohen","year":"2009","unstructured":"Cohen, E., et al.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23\u201342. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_2"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Cola\u00e7o, J.-L., Pagano, B., Pouzet, M.: SCADE 6: a formal language for embedded critical software development. In: Proceedings of International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 1\u201311. IEEE (2017)","DOI":"10.1109\/TASE.2017.8285623"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/978-3-030-39322-9_4","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"N Courant","year":"2020","unstructured":"Courant, N., S\u00e9r\u00e9, A., Shankar, N.: The correctness of a code generator for a functional language. In: Beyer, D., Zufferey, D. (eds.) VMCAI 2020. LNCS, vol. 11990, pp. 68\u201389. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-39322-9_4"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1007\/978-3-030-79876-5_37","volume-title":"Automated Deduction \u2013 CADE 28","author":"L Moura","year":"2021","unstructured":"Moura, L., Ullrich, S.: The lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 625\u2013635. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_37"},{"key":"4_CR12","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 de Moura","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. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-319-40648-0_12","volume-title":"NASA Formal Methods","author":"G F\u00e9rey","year":"2016","unstructured":"F\u00e9rey, G., Shankar, N.: Code generation using a formal model of reference counting. In: Rayadurgam, S., Tkachuk, O. (eds.) NFM 2016. LNCS, vol. 9690, pp. 150\u2013165. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40648-0_12"},{"key":"4_CR14","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher Order Logic","author":"MJC Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)"},{"key":"4_CR15","unstructured":"Hunter, A.: A brief introduction to the design of UBIFS (2008). http:\/\/www.linux-mtd.infradead.org\/doc\/ubifs_whitepaper.pdf"},{"key":"4_CR16","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","volume":"6617","author":"B Jacobs","year":"2011","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. Proc. of NASA Formal Methods (NFM) 6617, 41\u201355 (2011)","journal-title":"Proc. of NASA Formal Methods (NFM)"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/11813040_19","volume-title":"FM 2006: Formal Methods","author":"IT Kassios","year":"2006","unstructured":"Kassios, I.T.: Dynamic frames: support for framing, dependencies and sharing without restrictions. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 268\u2013283. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11813040_19"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-642-19861-8_3","volume-title":"Compiler Construction","author":"N Lameed","year":"2011","unstructured":"Lameed, N., Hendren, L.: Staged static techniques to efficiently implement array copy semantics in a MATLAB JIT compiler. In: Knoop, J. (ed.) CC 2011. LNCS, vol. 6601, pp. 22\u201341. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19861-8_3"},{"key":"4_CR19","unstructured":"Lammich, P.: Generating verified LLVM from Isabelle\/HOL. In: Proceedings of International Conference on Interactive Theorem Proving (ITP). LIPIcs, vol. 141, pp. 22:1\u201322:19. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2019)"},{"key":"4_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-030-51054-1_18","volume-title":"Automated Reasoning","author":"P Lammich","year":"2020","unstructured":"Lammich, P.: Efficient verified implementation of Introsort and Pdqsort. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12167, pp. 307\u2013323. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_18"},{"key":"4_CR21","unstructured":"Lammich, P.: Refinement of parallel algorithms down to LLVM. In: Proceedings of International Conference on Interactive Theorem Proving (ITP), LIPIcs, vol. 237, pp. 24:1\u201324:18. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2022)"},{"key":"4_CR22","unstructured":"X.\u00a0Leroy. The Clight language: a simplified version of Compcert C. http:\/\/compcert.inria.fr\/doc\/html\/compcert.cfrontend.Clight.html"},{"key":"4_CR23","doi-asserted-by":"crossref","unstructured":"M\u00e9ry, D., Singh, N.K.: Automatic code generation from Event-B models. In: Proceedings of Symposium on Information and Communication Technology (SoICT), pp. 179-188. ACM (2011)","DOI":"10.1145\/2069216.2069252"},{"key":"4_CR24","series-title":"LNCS","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"4_CR25","doi-asserted-by":"crossref","unstructured":"O\u2019Connor, L., et al.: Refinement through restraint: bringing down the cost of verification. In: Proceedings of International Conference on Functional Programming (ICFP), pp. 89-102. ACM (2016)","DOI":"10.1145\/2951913.2951940"},{"key":"4_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Computer Aided Verification","author":"S Owre","year":"1996","unstructured":"Owre, S., Rajan, S., Rushby, J.M., Shankar, N., Srivas, M.: PVS: combining specification, proof checking, and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 411\u2013414. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-61474-5_91"},{"key":"4_CR27","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of IEEE Symposium on Logic in Computer Science (LICS), pp. 55\u201374. IEEE (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"4_CR28","doi-asserted-by":"publisher","unstructured":"Schellhorn, G., Bodenm\u00fcller, S., Bitterlich, M., Reif, W.: Separating separation logic \u2013 modular verification of red-black trees. In: Lal, A., Tonetta, S. (eds.) VSTTE 2022. LNCS, vol. 13800, pp. 129\u2013147. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-25803-9_8","DOI":"10.1007\/978-3-031-25803-9_8"},{"key":"4_CR29","doi-asserted-by":"publisher","unstructured":"Schellhorn, G., Bodenm\u00fcller, S., Bitterlich, M., Reif, W.: Software & System Verification with KIV. In: Ahrendt, W., Beckert, B., Bubel, R., Johnsen, E.B. (eds.) The Logic of Software. A Tasting Menu of Formal Methods. LNCS, vol. 13360, pp. 408\u2013436. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-08166-8_20","DOI":"10.1007\/978-3-031-08166-8_20"},{"key":"4_CR30","unstructured":"Schellhorn, G., Bodenm\u00fcller, S., Reif, W.: KIV Specifications for the Code Generator (2024). https:\/\/kiv.isse.de\/projects\/VeriCodeLP.html"},{"key":"4_CR31","doi-asserted-by":"publisher","unstructured":"Schellhorn, G., Bodenm\u00fcller, S., Reif, W.: Refinement and separation: modular verification of wandering trees. In: Herber, P., Wijs, A. (eds.) iFM 2023. LNCS, vol. 14300, pp. 214\u2013234. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-47705-8_12","DOI":"10.1007\/978-3-031-47705-8_12"},{"key":"4_CR32","doi-asserted-by":"crossref","unstructured":"N.\u00a0Schirmer. Verification of Sequential Imperative Programs in Isabelle\/HOL. Ph.D. thesis, TUM (2006)","DOI":"10.1007\/978-3-540-32275-7_26"},{"key":"4_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45607-4_1","volume-title":"Logic Based Program Synthesis and Transformation","author":"N Shankar","year":"2002","unstructured":"Shankar, N.: Static analysis for safe destructive updates in a functional language. In: Pettorossi, A. (ed.) LOPSTR 2001. LNCS, vol. 2372, pp. 1\u201324. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45607-4_1"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-76554-4_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,18]],"date-time":"2025-01-18T11:38:16Z","timestamp":1737200296000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-76554-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,13]]},"ISBN":["9783031765537","9783031765544"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-76554-4_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,11,13]]},"assertion":[{"value":"13 November 2024","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":"Manchester","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 November 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 November 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ifm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ifm2024.cs.manchester.ac.uk\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}