{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:35:44Z","timestamp":1725489344971},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540740605"},{"type":"electronic","value":"9783540740612"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-74061-2_10","type":"book-chapter","created":{"date-parts":[[2007,8,21]],"date-time":"2007-08-21T11:39:13Z","timestamp":1187696353000},"page":"153-169","source":"Crossref","is-referenced-by-count":4,"title":["A Framework for End-to-End Verification and Evaluation of Register Allocators"],"prefix":"10.1007","author":[{"given":"V. Krishna","family":"Nandivada","sequence":"first","affiliation":[]},{"given":"Fernando Magno Quint\u00e3o","family":"Pereira","sequence":"additional","affiliation":[]},{"given":"Jens","family":"Palsberg","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"10_CR1","unstructured":"Standard ML of New Jersey (2000), \n \n http:\/\/www.smlnj.org\/"},{"key":"10_CR2","unstructured":"GNU C compiler (2005), \n \n http:\/\/gcc.gnu.org"},{"key":"10_CR3","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1145\/236337.236342","volume-title":"OOPSLA","author":"A.-R. Adl-Tabatabai","year":"1996","unstructured":"Adl-Tabatabai, A.-R., Gross, T., Lueh, G.-Y.: Code reuse in an optimizing compiler. In: OOPSLA, pp. 51\u201368. ACM Press, New York (1996)"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/BFb0055426","volume-title":"Implementation of Functional Languages","author":"J. Agat","year":"1998","unstructured":"Agat, J.: Types for register allocation. In: Clack, C., Hammond, K., Davie, T. (eds.) IFL 1997. LNCS, vol.\u00a01467, pp. 92\u2013111. Springer, Heidelberg (1998)"},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/3-540-36579-6_3","volume-title":"Compiler Construction","author":"C. Andersson","year":"2003","unstructured":"Andersson, C.: Register allocation by optimal graph coloring. In: Hedin, G. (ed.) CC 2003 and ETAPS 2003. LNCS, vol.\u00a02622, pp. 34\u201345. Springer, Heidelberg (2003)"},{"key":"10_CR6","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1145\/378795.378854","volume-title":"PLDI","author":"A.W. Appel","year":"2001","unstructured":"Appel, A.W., George, L.: Optimal spilling for CISC machines with few registers. In: PLDI, pp. 243\u2013253. ACM Press, New York (2001)"},{"key":"10_CR7","doi-asserted-by":"crossref","unstructured":"Austin, T.M., Breach, S.E., Sohi, G.S.: Efficient detection of all pointer and array access errors. In: PLDI, pp. 290\u2013301 (1994)","DOI":"10.1145\/773473.178446"},{"issue":"6","key":"10_CR8","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1145\/872726.806984","volume":"17","author":"G.J. Chaitin","year":"1982","unstructured":"Chaitin, G.J.: Register allocation and spilling via graph coloring. SIGPLAN Notices\u00a017(6), 98\u2013105 (1982)","journal-title":"SIGPLAN Notices"},{"key":"10_CR9","unstructured":"Elleithy, K.M., Abd-El-Fattah, E.G.: A genetic algorithm for register allocation. In: Ninth Great Lakes Symposium on VLSI, pp. 226\u2013227 (1999)"},{"key":"10_CR10","unstructured":"Fourer, R., Gay, D.M., Kernighan, B.W.: AMPL: A modeling language for mathematical programming. Scientific Press (1993), \n \n http:\/\/www.ampl.com"},{"issue":"11","key":"10_CR11","doi-asserted-by":"publisher","first-page":"638","DOI":"10.1145\/361179.361201","volume":"17","author":"R.A. Freiburghouse","year":"1974","unstructured":"Freiburghouse, R.A.: Register allocation via usage counts. Commun. ACM\u00a017(11), 638\u2013642 (1974)","journal-title":"Commun. ACM"},{"key":"10_CR12","first-page":"245","volume-title":"MICRO","author":"C. Fu","year":"2002","unstructured":"Fu, C., Wilken, K.: A faster optimal register allocator. In: MICRO, pp. 245\u2013256. IEEE Computer Society Press, Los Alamitos (2002)"},{"issue":"3","key":"10_CR13","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. TOPLAS\u00a018(3), 300\u2013324 (1996)","journal-title":"TOPLAS"},{"issue":"8","key":"10_CR14","first-page":"929","volume":"26","author":"D.W. Goodwin","year":"1996","unstructured":"Goodwin, D.W., Wilken, K.D.: Optimal and near-optimal global register allocations using 0-1 integer programming. SPE\u00a026(8), 929\u2013968 (1996)","journal-title":"SPE"},{"issue":"12","key":"10_CR15","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1109\/2.546613","volume":"29","author":"M.W. Hall","year":"1996","unstructured":"Hall, M.W., Anderson, J.-A.M., Amarasinghe, S.P., Murphy, B.R., Liao, S.-W., Bugnion, E., Lam, M.S.: Maximizing multiprocessor performance with the SUIF compiler. IEEE Computer\u00a029(12), 84\u201389 (1996)","journal-title":"IEEE Computer"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Springer, Heidelberg (2006)"},{"key":"10_CR17","first-page":"42","volume-title":"POPL","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: POPL, pp. 42\u201354. ACM Press, New York (2006)"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Lueh, G.-Y., Gross, T., Adl-Tabatabai, A.-R.: Global register allocation based on graph fusion. In: Languages and Compilers for Parallel Computing, pp. 246\u2013265 (1996)","DOI":"10.1007\/BFb0017257"},{"key":"10_CR19","volume-title":"IEEE International Conference Computer-Aided Deisgn","author":"G. Memik","year":"2001","unstructured":"Memik, G., Mangione-Smith, B., Hu, W.: Netbench: A benchmarking suite for network processors. In: IEEE International Conference Computer-Aided Deisgn, IEEE Computer Society Press, Los Alamitos (2001)"},{"issue":"3","key":"10_CR20","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1145\/319301.319345","volume":"21","author":"G. Morrisett","year":"1999","unstructured":"Morrisett, G., Walker, D., Crary, K., Glew, N.: From system F to typed assembly language. TOPLAS\u00a021(3), 527\u2013568 (1999)","journal-title":"TOPLAS"},{"issue":"1","key":"10_CR21","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1145\/972627.972635","volume":"3","author":"M. Naik","year":"2004","unstructured":"Naik, M., Palsberg, J.: Compiling with code size constraints. Transactions on Embedded Computing Systems\u00a03(1), 163\u2013181 (2004)","journal-title":"Transactions on Embedded Computing Systems"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"Krishna Nandivada, V., Palsberg, J.: Efficient spill code for SDRAM. In: CASES, pp. 24\u201331 (2003)","DOI":"10.1145\/951710.951716"},{"key":"10_CR23","series-title":"Lecture Notes in Computer Science","first-page":"232","volume-title":"Compiler Construction","author":"V. Krishna Nandivada","year":"2005","unstructured":"Krishna Nandivada, V., Palsberg, J.: Sara: Combining stack allocation and register allocation. In: Bodik, R. (ed.) CC 2005. LNCS, vol.\u00a03443, pp. 232\u2013246. Springer, Heidelberg (2005)"},{"key":"10_CR24","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1145\/349299.349314","volume-title":"PLDI","author":"G.C. Necula","year":"2000","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler. In: PLDI, pp. 83\u201395. ACM Press, New York (2000)"},{"key":"10_CR25","doi-asserted-by":"crossref","unstructured":"Necula, G.C., Lee, P.: The design and implementation of a certifying compiler. In: PLDI, pp. 333\u2013344 (1998)","DOI":"10.1145\/277652.277752"},{"issue":"1-3","key":"10_CR26","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1016\/j.scico.2004.01.005","volume":"50","author":"A. Ohori","year":"2004","unstructured":"Ohori, A.: Register allocation by proof transformation. Science of Computer Programming\u00a050(1-3), 161\u2013187 (2004)","journal-title":"Science of Computer Programming"},{"key":"10_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/11575467_21","volume-title":"Programming Languages and Systems","author":"F.M.Q. Pereira","year":"2005","unstructured":"Pereira, F.M.Q., Palsberg, J.: Register allocation via coloring of chordal graphs. In: Yi, K. (ed.) APLAS 2005. LNCS, vol.\u00a03780, pp. 315\u2013329. Springer, Heidelberg (2005)"},{"issue":"5","key":"10_CR28","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\u00a021(5), 895\u2013913 (1999)","journal-title":"TOPLAS"},{"key":"10_CR29","doi-asserted-by":"crossref","unstructured":"Tallam, S., Gupta, R.: Bitwidth aware global register allocation. In: POPL, pp. 85\u201396 (2003)","DOI":"10.1145\/640128.604139"},{"key":"10_CR30","doi-asserted-by":"crossref","unstructured":"Traub, O., Holloway, G.H., Smith, M.D.: Quality and speed in linear-scan register allocation. In: PLDI, pp. 142\u2013151 (1998)","DOI":"10.1145\/277652.277714"},{"key":"10_CR31","unstructured":"Vallee-Rai, R., Co, P., Gagnon, E., Hendren, L., Lam, P., Sundaresan, V.: Soot - a Java bytecode optimization framework. In: CASCON (1999)"},{"key":"10_CR32","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","volume-title":"Automated Deduction - CADE-16","author":"F. Pfenning","year":"1999","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf - a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) Automated Deduction - CADE-16. LNCS (LNAI), vol.\u00a01632, pp. 202\u2013206. Springer, Heidelberg (1999)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74061-2_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T21:08:09Z","timestamp":1558472889000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74061-2_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540740605","9783540740612"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74061-2_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}