{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:13:17Z","timestamp":1770289997365,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642119569","type":"print"},{"value":"9783642119576","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-11957-6_9","type":"book-chapter","created":{"date-parts":[[2010,3,8]],"date-time":"2010-03-08T00:55:38Z","timestamp":1268009738000},"page":"145-164","source":"Crossref","is-referenced-by-count":13,"title":["Formal Verification of Coalescing Graph-Coloring Register Allocation"],"prefix":"10.1007","author":[{"given":"Sandrine","family":"Blazy","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Beno\u00eet","family":"Robillard","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew W.","family":"Appel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/3-540-44880-2_27","volume-title":"ZB 2003: Formal Specification and Development in Z and B","author":"J.-R. Abrial","year":"2003","unstructured":"Abrial, J.-R., Cansell, D., M\u00e9ry, D.: Formal derivation of spanning trees algorithms. In: Bert, D., Bowen, J.P., King, S. (eds.) ZB 2003. LNCS, vol.\u00a02651, pp. 457\u2013476. Springer, Heidelberg (2003)"},{"key":"9_CR2","volume-title":"Modern Compiler Implementation in ML","author":"A.W. Appel","year":"1998","unstructured":"Appel, A.W.: Modern Compiler Implementation in ML. Cambridge University Press, Cambridge (1998)"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Appel, A.W., George, L.: Optimal spilling for CISC machines with few registers. In: PLDI. ACM, New York (2001)","DOI":"10.1145\/378795.378854"},{"key":"9_CR4","doi-asserted-by":"publisher","first-page":"711","DOI":"10.1090\/S0002-9904-1976-14122-5","volume":"82","author":"K. Appel","year":"1976","unstructured":"Appel, K., Haken, W.: Every planar map is four colorable. Bulletin of the American Mathematical Society\u00a082, 711\u2013712 (1976)","journal-title":"Bulletin of the American Mathematical Society"},{"key":"9_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/3-540-45685-6_6","volume-title":"Theorem Proving in Higher Order Logics","author":"G. Bauer","year":"2002","unstructured":"Bauer, G., Nipkow, T.: The 5 colour theorem in Isabelle\/Isar. In: Carre\u00f1o, V.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol.\u00a02410, pp. 67\u201382. Springer, Heidelberg (2002)"},{"key":"9_CR6","series-title":"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. Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, Heidelberg (2004)"},{"key":"9_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.\u00a04085, pp. 460\u2013475. Springer, Heidelberg (2006)"},{"issue":"3","key":"9_CR8","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1145\/177492.177575","volume":"16","author":"P. Briggs","year":"1994","unstructured":"Briggs, P., Cooper, K.D., Torczon, L.: Improvements to graph coloring register allocation. TOPLAS\u00a016(3), 428\u2013455 (1994)","journal-title":"TOPLAS"},{"key":"9_CR9","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/0096-0551(81)90048-5","volume":"6","author":"G.J. Chaitin","year":"1981","unstructured":"Chaitin, G.J., Auslander, M.A., Chandra, A.K., Cocke, J., Hopkins, M.E., Markstein, P.W.: Register allocation via coloring. Computer Languages\u00a06, 47\u201357 (1981)","journal-title":"Computer Languages"},{"key":"9_CR10","unstructured":"Chen, J.-C.: Dijkstra\u2019s shortest path algorithm. Journal of Formalized Mathematics\u00a015 (2003)"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"144","DOI":"10.1007\/3-540-58450-1_40","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"C.-T. Chou","year":"1994","unstructured":"Chou, C.-T.: A formal theory of undirected graphs in higher-order logic. In: Melham, T.F., Camilleri, J. (eds.) HUG 1994. LNCS, vol.\u00a0859, pp. 144\u2013157. Springer, Heidelberg (1994)"},{"key":"9_CR12","unstructured":"Coq. The coq proof assistant, \n                  \n                    http:\/\/coq.inria.fr"},{"issue":"3","key":"9_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":"11","key":"9_CR14","first-page":"1382","volume":"55","author":"G. Gonthier","year":"2008","unstructured":"Gonthier, G.: Formal proof \u2013 the four-color theorem. Notices of the American Mathematical Society\u00a055(11), 1382\u20131393 (2008)","journal-title":"Notices of the American Mathematical Society"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Hack, S., Goos, G.: Copy coalescing by graph recoloring. In: PLDI. ACM, New York (2008)","DOI":"10.1145\/1375581.1375610"},{"key":"9_CR16","doi-asserted-by":"publisher","first-page":"193","DOI":"10.2307\/2369235","volume":"2","author":"A.B. Kempe","year":"1879","unstructured":"Kempe, A.B.: On the geographical problem of the four colors. American Journal of Mathematics\u00a02, 193\u2013200 (1879)","journal-title":"American Journal of Mathematics"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: Programming a compiler with a proof assistant. In: POPL, pp. 42\u201354. ACM, New York (2006)","DOI":"10.1145\/1111320.1111042"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1007\/11541868_24","volume-title":"Theorem Proving in Higher Order Logics","author":"J.S. Moore","year":"2005","unstructured":"Moore, J.S., Zhang, Q.: Proof pearl: Dijkstra\u2019s shortest path algorithm verified with ACL2. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 373\u2013384. Springer, Heidelberg (2005)"},{"issue":"5","key":"9_CR19","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1145\/358438.349314","volume":"35","author":"G.C. Necula","year":"2000","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler. SIGPLAN Not.\u00a035(5), 83\u201394 (2000)","journal-title":"SIGPLAN Not."},{"key":"9_CR20","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":"9_CR21","doi-asserted-by":"crossref","unstructured":"Yamamoto, M., Nishizaki, S.-y., Hagiya, M., Toda, Y.: Formalization of planar graphs. In: Workshop on Higher Order Logic Theorem Proving and Its Applications, pp. 369\u2013384 (1995)","DOI":"10.1007\/3-540-60275-5_77"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/BFb0055153","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Yamamoto","year":"1998","unstructured":"Yamamoto, M., Takahashi, K., Hagiya, M., Nishizaki, S.-y., Tamai, T.: Formalization of graph search algorithms and its applications. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol.\u00a01479, pp. 479\u2013496. Springer, Heidelberg (1998)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11957-6_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T17:32:19Z","timestamp":1558287139000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11957-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642119569","9783642119576"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11957-6_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}