{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T07:07:54Z","timestamp":1750748874766},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642140518"},{"type":"electronic","value":"9783642140525"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14052-5_26","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T14:23:14Z","timestamp":1278944594000},"page":"371-386","source":"Crossref","is-referenced-by-count":16,"title":["A Framework for Formal Verification of Compiler Optimizations"],"prefix":"10.1007","author":[{"given":"William","family":"Mansky","sequence":"first","affiliation":[]},{"given":"Elsa","family":"Gunter","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"26_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/73560.73561","volume-title":"POPL \u201988: Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages","author":"B. Alpern","year":"1988","unstructured":"Alpern, B., Wegman, M.N., Zadeck, F.K.: Detecting equality of variables in programs. In: POPL \u201988: Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, pp. 1\u201311. ACM, New York (1988)"},{"issue":"5","key":"26_CR2","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R. Alur","year":"2002","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM\u00a049(5), 672\u2013713 (2002)","journal-title":"J. ACM"},{"key":"26_CR3","volume-title":"Modern Compiler Implementation in ML","author":"A.W. Appel","year":"2004","unstructured":"Appel, A.W.: Modern Compiler Implementation in ML. Cambridge University Press, New York (2004)"},{"key":"26_CR4","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1145\/567532.567551","volume-title":"POPL \u201981: Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages","author":"M. Ben-Ari","year":"1981","unstructured":"Ben-Ari, M., Manna, Z., Pnueli, A.: The temporal logic of branching time. In: POPL \u201981: Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, pp. 164\u2013176. ACM, New York (1981)"},{"key":"26_CR5","unstructured":"Blech, J.O., Glesner, S.: A formal correctness proof for code generation from ssa form in isabelle\/hol. In: Proceedings der 3. Arbeitstagung Programmiersprachen (ATPS) auf der 34. Jahrestagung der Gesellschaft f\u00fcr Informatik, September 2004. Lecture Notes in Informatics (2004), \n                    \n                      http:\/\/www.info.uni-karlsruhe.de\/papers\/Blech-Glesner-ATPS-2004.pdf"},{"issue":"4","key":"26_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1516507.1516509","volume":"31","author":"S. Kalvala","year":"2009","unstructured":"Kalvala, S., Warburton, R., Lacey, D.: Program transformations using temporal logic side conditions. ACM Trans. Program. Lang. Syst.\u00a031(4), 1\u201348 (2009)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"26_CR7","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1145\/503272.503299","volume-title":"POPL \u201902: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages","author":"D. Lacey","year":"2002","unstructured":"Lacey, D., Jones, N.D., Van Wyk, E., Frederiksen, C.C.: Proving correctness of compiler optimizations by temporal logic. In: POPL \u201902: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, pp. 283\u2013294. ACM, New York (2002)"},{"key":"26_CR8","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1145\/1111037.1111042","volume-title":"POPL \u201906: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages","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 \u201906: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, pp. 42\u201354. ACM, New York (2006)"},{"issue":"4","key":"26_CR9","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.\u00a043(4), 363\u2013446 (2009)","journal-title":"J. Autom. Reason."},{"key":"26_CR10","unstructured":"Mansky, W.: TRANS in Isabelle, \n                    \n                      http:\/\/www.cs.illinois.edu\/homes\/mansky1"},{"issue":"1","key":"26_CR11","first-page":"100","volume":"10","author":"W.M. McKeeman","year":"1998","unstructured":"McKeeman, W.M.: A formally verified compiler backend. Digital Technical Journal\u00a010(1), 100\u2013107 (1998)","journal-title":"Digital Technical Journal"},{"issue":"4","key":"26_CR12","first-page":"461","volume":"5","author":"J.S. Moore","year":"1989","unstructured":"Moore, J.S.: A mechanically verified language implementation. J. Autom. Reason.\u00a05(4), 461\u2013492 (1989)","journal-title":"J. Autom. Reason."},{"key":"26_CR13","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":"26_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/BFb0032686","volume-title":"Languages and Compilers for Parallel Computing","author":"V. Sarkar","year":"1998","unstructured":"Sarkar, V.: Analysis and optimization of explicitly parallel programs using the parallel program graph representation. In: Huang, C.-H., Sadayappan, P., Sehr, D. (eds.) LCPC 1997. LNCS, vol.\u00a01366, pp. 94\u2013113. Springer, Heidelberg (1998)"},{"key":"26_CR15","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1145\/1328438.1328444","volume-title":"POPL \u201908: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on 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: POPL \u201908: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages, pp. 17\u201327. ACM, New York (2008)"},{"issue":"1","key":"26_CR16","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1145\/291251.289425","volume":"34","author":"E. Visser","year":"1999","unstructured":"Visser, E., Benaissa, Z.e.A., Tolmach, A.: Building program optimizers with rewriting strategies. SIGPLAN Not.\u00a034(1), 13\u201326 (1999)","journal-title":"SIGPLAN Not."}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14052-5_26.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T12:17:22Z","timestamp":1619785042000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14052-5_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642140518","9783642140525"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14052-5_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}