{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T19:13:16Z","timestamp":1742929996664,"version":"3.40.3"},"publisher-location":"Cham","reference-count":19,"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_8","type":"book-chapter","created":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T11:17:55Z","timestamp":1731410275000},"page":"128-147","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Modeling Register Pairs in\u00a0CompCert"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-7417-2537","authenticated-orcid":false,"given":"Alexander","family":"Loitzl","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1468-8398","authenticated-orcid":false,"given":"Florian","family":"Zuleger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,11,13]]},"reference":[{"key":"8_CR1","unstructured":"Anand, A., et al.: CertiCoq: a verified compiler for Coq. In: The Third International Workshop on Coq for Programming Languages (CoqPL) (2017)"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-19718-5_1","volume-title":"Programming Languages and Systems","author":"AW Appel","year":"2011","unstructured":"Appel, A.W.: Verified software toolchain. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 1\u201317. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19718-5_1"},{"key":"8_CR3","unstructured":"Arm Limited: Arm architecture reference manual for a-profile architecture. https:\/\/developer.arm.com\/documentation\/ddi0487"},{"key":"8_CR4","doi-asserted-by":"publisher","unstructured":"Barthe, G., et al.: Formal verification of a constant-time preserving c compiler. Proc. ACM Program. Lang. 4(POPL) (2019). https:\/\/doi.org\/10.1145\/3371075","DOI":"10.1145\/3371075"},{"key":"8_CR5","doi-asserted-by":"publisher","unstructured":"Barthe, G., Demange, D., Pichardie, D.: Formal verification of an SSA-based middle-end for CompCert. ACM Trans. Program. Lang. Syst. 36(1) (2014). https:\/\/doi.org\/10.1145\/2579080","DOI":"10.1145\/2579080"},{"key":"8_CR6","unstructured":"Bedin\u00a0Fran\u00e7a, R., Blazy, S., Favre-Felix, D., Leroy, X., Pantel, M., Souyris, J.: Formally verified optimizing compilation in ACG-based flight control software. In: ERTS2 2012: Embedded Real Time Software and Systems. AAAF, SEE, Toulouse, France (2012)"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/11813040_31","volume-title":"FM 2006: Formal Methods","author":"S Blazy","year":"2006","unstructured":"Blazy, S., Dargaye, Z., Leroy, X.: Formal verification of a C compiler front-end. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 460\u2013475. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11813040_31"},{"key":"8_CR8","doi-asserted-by":"publisher","unstructured":"Briggs, P., Cooper, K.D., Torczon, L.: Improvements to graph coloring register allocation. ACM Trans. Program. Lang. Syst. 16(3), 428\u2013455 (1994). https:\/\/doi.org\/10.1145\/177492.177575","DOI":"10.1145\/177492.177575"},{"key":"8_CR9","doi-asserted-by":"publisher","unstructured":"George, L., Appel, A.W.: Iterated register coalescing. ACM Trans. Program. Lang. Syst. 18(3), 300\u2013324 (1996). https:\/\/doi.org\/10.1145\/229542.229546","DOI":"10.1145\/229542.229546"},{"key":"8_CR10","unstructured":"K\u00e4stner, D., et al.: CompCert: practical experience on integrating and qualifying a formally verified optimizing compiler. In: ERTS2 2018 - 9th European Congress Embedded Real-Time Software and Systems, pp.\u00a01\u20139. 3AF, SEE, SIE, Toulouse, France (2018)"},{"issue":"4","key":"8_CR11","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: A formally verified compiler back-end. J. Autom. Reason. 43(4), 363\u2013446 (2009). https:\/\/doi.org\/10.1007\/s10817-009-9155-4","journal-title":"J. Autom. Reason."},{"key":"8_CR12","unstructured":"Leroy, X.: The compcert C verified compiler: documentation and user\u2019s manual (2023)"},{"key":"8_CR13","doi-asserted-by":"publisher","unstructured":"Leroy, X., Appel, A.W., Blazy, S., Stewart, G.: The CompCert memory model. In: Appel, A.W. (ed.) Program Logics for Certified Compilers. Cambridge University Press, Cambridge (2014). https:\/\/doi.org\/10.1017\/CBO9781107256552.037","DOI":"10.1017\/CBO9781107256552.037"},{"key":"8_CR14","doi-asserted-by":"publisher","unstructured":"Loitzl, A.: Artifact for \u201cModeling Register Pairs in CompCert\u201d. https:\/\/doi.org\/10.5281\/zenodo.12010656","DOI":"10.5281\/zenodo.12010656"},{"key":"8_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/978-3-642-11970-5_13","volume-title":"Compiler Construction","author":"S Rideau","year":"2010","unstructured":"Rideau, S., Leroy, X.: Validating register allocation and spilling. In: Gupta, R. (ed.) CC 2010. LNCS, vol. 6011, pp. 224\u2013243. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11970-5_13"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/978-3-540-39920-9_17","volume-title":"Software and Compilers for Embedded Systems","author":"J Runeson","year":"2003","unstructured":"Runeson, J., Nystr\u00f6m, S.-O.: Retargetable graph-coloring register allocation for irregular architectures. In: Krall, A. (ed.) SCOPES 2003. LNCS, vol. 2826, pp. 240\u2013254. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-39920-9_17"},{"issue":"6","key":"8_CR17","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1145\/996893.996875","volume":"39","author":"MD Smith","year":"2004","unstructured":"Smith, M.D., Ramsey, N., Holloway, G.: A generalized algorithm for graph-coloring register allocation. SIGPLAN Not. 39(6), 277\u2013288 (2004). https:\/\/doi.org\/10.1145\/996893.996875","journal-title":"SIGPLAN Not."},{"key":"8_CR18","doi-asserted-by":"publisher","unstructured":"Song, Y., Cho, M., Kim, D., Kim, Y., Kang, J., Hur, C.K.: Compcertm: Compcert with c-assembly linking and lightweight modular verification. Proc. ACM Program. Lang. 4(POPL) (2019). https:\/\/doi.org\/10.1145\/3371091","DOI":"10.1145\/3371091"},{"key":"8_CR19","doi-asserted-by":"publisher","unstructured":"Yang, X., Chen, Y., Eide, E., Regehr, J.: Finding and understanding bugs in c compilers. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, pp. 283\u2013294. Association for Computing Machinery, New York (2011). https:\/\/doi.org\/10.1145\/1993498.1993532","DOI":"10.1145\/1993498.1993532"}],"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_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,18]],"date-time":"2025-01-18T11:38:14Z","timestamp":1737200294000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-76554-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,13]]},"ISBN":["9783031765537","9783031765544"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-76554-4_8","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":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"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"}}]}}