{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:09:03Z","timestamp":1770278943622,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642119699","type":"print"},{"value":"9783642119705","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-11970-5_13","type":"book-chapter","created":{"date-parts":[[2010,3,8]],"date-time":"2010-03-08T00:23:33Z","timestamp":1268007813000},"page":"224-243","source":"Crossref","is-referenced-by-count":27,"title":["Validating Register Allocation and Spilling"],"prefix":"10.1007","author":[{"given":"Silvain","family":"Rideau","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xavier","family":"Leroy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/BFb0054170","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"1998","unstructured":"Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 151\u2013166. Springer, Heidelberg (1998)"},{"key":"13_CR2","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1145\/349299.349314","volume-title":"Programming Language Design and Implementation 2000","author":"G.C. Necula","year":"2000","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler. In: Programming Language Design and Implementation 2000, pp. 83\u201395. ACM Press, New York (2000)"},{"key":"13_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/964001.964002","volume-title":"31st symposium Principles of Programming Languages","author":"X. Rival","year":"2004","unstructured":"Rival, X.: Symbolic transfer function-based approaches to certified compilation. In: 31st symposium Principles of Programming Languages, pp. 1\u201313. ACM Press, New York (2004)"},{"key":"13_CR4","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1145\/1542476.1542512","volume-title":"Programming Language Design and Implementation 2009","author":"J.B. Tristan","year":"2009","unstructured":"Tristan, J.B., Leroy, X.: Verified validation of Lazy Code Motion. In: Programming Language Design and Implementation 2009, pp. 316\u2013326. ACM Press, New York (2009)"},{"key":"13_CR5","first-page":"17","volume-title":"35th symposium Principles of Programming Languages","author":"J.B. Tristan","year":"2008","unstructured":"Tristan, J.B., Leroy, X.: Formal verification of translation validators: A case study on instruction scheduling optimizations. In: 35th symposium Principles of Programming Languages, pp. 17\u201327. ACM Press, New York (2008)"},{"key":"13_CR6","unstructured":"Coq development team: The Coq proof assistant. Software and documentation, \n                    \n                      http:\/\/coq.inria.fr\/\n                    \n                    \n                   (1989\u20132010)"},{"key":"13_CR7","series-title":"EATCS Texts in Theoretical Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development \u2013 Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development \u2013 Coq\u2019Art: The Calculus of Inductive Constructions. EATCS Texts in Theoretical Computer Science. Springer, Heidelberg (2004)"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11823230_19","volume-title":"Static Analysis","author":"Y. Huang","year":"2006","unstructured":"Huang, Y., Childers, B.R., Soffa, M.L.: Catching and identifying bugs in register allocation. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 281\u2013300. Springer, Heidelberg (2006)"},{"issue":"7","key":"13_CR9","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X. Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Communications of the ACM\u00a052(7), 107\u2013115 (2009)","journal-title":"Communications of the ACM"},{"issue":"3","key":"13_CR10","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 Transactions on Programming Languages and Systems\u00a018(3), 300\u2013324 (1996)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"4","key":"13_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. Journal of Automated Reasoning\u00a043(4), 363\u2013446 (2009)","journal-title":"Journal of Automated Reasoning"},{"key":"13_CR12","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1145\/378795.378854","volume-title":"Programming Language Design and Implementation 2001","author":"A.W. Appel","year":"2001","unstructured":"Appel, A.W., George, L.: Optimal spilling for CISC machines with few registers. In: Programming Language Design and Implementation 2001, pp. 243\u2013253. ACM Press, New York (2001)"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1007\/978-3-642-11957-6_9","volume-title":"ESOP 2010","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.\u00a06012, pp. 145\u2013164. Springer, Heidelberg (2010)"},{"key":"13_CR14","unstructured":"Samet, H.: Automatically Proving the Correctness of Translations Involving Optimized Code. PhD thesis, Stanford University (1975)"},{"key":"13_CR15","first-page":"280","volume-title":"Int. Conf. on Compilers, Architecture, and Synthesis for Embedded Systems (CASES 2002)","author":"R. Leviathan","year":"2006","unstructured":"Leviathan, R., Pnueli, A.: Validating software pipelining optimizations. In: Int. Conf. on Compilers, Architecture, and Synthesis for Embedded Systems (CASES 2002), pp. 280\u2013287. ACM Press, New York (2006)"},{"issue":"3","key":"13_CR16","first-page":"223","volume":"9","author":"L. Zuck","year":"2003","unstructured":"Zuck, L., Pnueli, A., Fang, Y., Goldberg, B.: VOC: A methodology for translation validation of optimizing compilers. Journal of Universal Computer Science\u00a09(3), 223\u2013247 (2003)","journal-title":"Journal of Universal Computer Science"},{"key":"13_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1007\/11513988_29","volume-title":"Computer Aided Verification","author":"C.W. Barrett","year":"2005","unstructured":"Barrett, C.W., Fang, Y., Goldberg, B., Hu, Y., Pnueli, A., Zuck, L.D.: TVOC: A translation validator for optimizing compilers. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 291\u2013295. Springer, Heidelberg (2005)"},{"key":"13_CR18","volume-title":"37th symposium Principles of Programming Languages","author":"J.B. Tristan","year":"2010","unstructured":"Tristan, J.B., Leroy, X.: A simple, verified validator for software pipelining. In: 37th symposium Principles of Programming Languages. ACM Press, New York (to appear, 2010) (accepted for publication)"},{"key":"13_CR19","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1145\/1542476.1542513","volume-title":"Programming Language Design and Implementation 2009","author":"S. Kundu","year":"2009","unstructured":"Kundu, S., Tatlock, Z., Lerner, S.: Proving optimizations correct using parameterized program equivalence. In: Programming Language Design and Implementation 2009, pp. 327\u2013337. ACM Press, New York (2009)"},{"key":"13_CR20","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1145\/143095.143143","volume-title":"Programming Language Design and Implementation 1992","author":"P. Briggs","year":"1992","unstructured":"Briggs, P., Cooper, K.D., Torczon, L.: Rematerialization. In: Programming Language Design and Implementation 1992, pp. 311\u2013321. ACM Press, New York (1992)"}],"container-title":["Lecture Notes in Computer Science","Compiler Construction"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11970-5_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T02:45:56Z","timestamp":1606185956000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11970-5_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642119699","9783642119705"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11970-5_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}