{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T11:32:17Z","timestamp":1743075137637,"version":"3.40.3"},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319661063"},{"type":"electronic","value":"9783319661070"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66107-0_27","type":"book-chapter","created":{"date-parts":[[2017,8,20]],"date-time":"2017-08-20T14:13:59Z","timestamp":1503238439000},"page":"427-443","source":"Crossref","is-referenced-by-count":1,"title":["Verified Spilling and Translation Validation with\u00a0Repair"],"prefix":"10.1007","author":[{"given":"Julian","family":"Rosemann","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1948-0596","authenticated-orcid":false,"given":"Sigurd","family":"Schneider","sequence":"additional","affiliation":[]},{"given":"Sebastian","family":"Hack","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"27_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-642-28869-2_3","volume-title":"Programming Languages and Systems","author":"G Barthe","year":"2012","unstructured":"Barthe, G., Demange, D., Pichardie, D.: A formally verified SSA-based middle-end. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 47\u201366. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28869-2_3"},{"key":"27_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-642-11957-6_9","volume-title":"Programming Languages and Systems","author":"S Blazy","year":"2010","unstructured":"Blazy, S., Robillard, B., Appel, A.W.: Formal verification of coalescing graph-coloring register allocation. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 145\u2013164. Springer, Heidelberg (2010). 10.1007\/978-3-642-11957-6_9"},{"key":"27_CR3","doi-asserted-by":"crossref","unstructured":"Bouchez, F., Darte, A., Rastello, F.: On the complexity of spill everywhere under SSA form. In: LCTES, San Diego, California, USA, 13\u201315 June 2007","DOI":"10.1145\/1254766.1254782"},{"key":"27_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-00722-4_13","volume-title":"Compiler Construction","author":"M Braun","year":"2009","unstructured":"Braun, M., Hack, S.: Register spilling and live-range splitting for SSA-form programs. In: de Moor, O., Schwartzbach, M.I. (eds.) CC 2009. LNCS, vol. 5501, pp. 174\u2013189. Springer, Heidelberg (2009). 10.1007\/978-3-642-00722-4_13"},{"key":"27_CR5","doi-asserted-by":"crossref","unstructured":"Chaitin, G.J.: Register allocation & spilling via graph coloring. In: PLDI, Boston, Massachusetts, USA, 23\u201325 June 1982","DOI":"10.1145\/800230.806984"},{"issue":"3","key":"27_CR6","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1145\/229542.229546","volume":"18","author":"L George","year":"1996","unstructured":"George, L., Appel, A.W.: Iterated register coalescing. ACM Trans. Program. Lang. Syst. 18(3), 300\u2013324 (1996)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"27_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/11688839_20","volume-title":"Compiler Construction","author":"S Hack","year":"2006","unstructured":"Hack, S., Grund, D., Goos, G.: Register allocation for programs in SSA-form. In: Mycroft, A., Zeller, A. (eds.) CC 2006. LNCS, vol. 3923, pp. 247\u2013262. Springer, Heidelberg (2006). 10.1007\/11688839_20"},{"issue":"4","key":"27_CR8","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. JAR 43(4), 363\u2013446 (2009)","journal-title":"JAR"},{"issue":"5","key":"27_CR9","doi-asserted-by":"publisher","first-page":"895","DOI":"10.1145\/330249.330250","volume":"21","author":"M Poletto","year":"1999","unstructured":"Poletto, M., Sarkar, V.: Linear scan register allocation. TOPLAS 21(5), 895\u2013913 (1999)","journal-title":"TOPLAS"},{"key":"27_CR10","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). 10.1007\/978-3-642-11970-5_13"},{"key":"27_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/978-3-319-22102-1_23","volume-title":"Interactive Theorem Proving","author":"S Schneider","year":"2015","unstructured":"Schneider, S., Smolka, G., Hack, S.: A linear first-order functional intermediate language for verified compilers. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 344\u2013358. Springer, Cham (2015). 10.1007\/978-3-319-22102-1_23"},{"key":"27_CR12","unstructured":"Schneider, S., Smolka, G., Hack, S.: An inductive proof method for simulation-based compiler correctness (2016). CoRR abs\/1611.09606"},{"key":"27_CR13","doi-asserted-by":"crossref","unstructured":"Tan, Y.K., et al.: A new verified compiler backend for CakeML. In: ICFP, Nara, Japan, 18\u201322 September 2016","DOI":"10.1145\/2951913.2951924"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66107-0_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,29]],"date-time":"2022-09-29T06:08:28Z","timestamp":1664431708000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-66107-0_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661063","9783319661070"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66107-0_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}