{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:03:28Z","timestamp":1770285808500,"version":"3.49.0"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319723433","type":"print"},{"value":"9783319723440","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,11,29]],"date-time":"2017-11-29T00:00:00Z","timestamp":1511913600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-72344-0_3","type":"book-chapter","created":{"date-parts":[[2017,11,28]],"date-time":"2017-11-28T12:23:23Z","timestamp":1511871803000},"page":"50-65","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Formal Verification of Optimizing Compilers"],"prefix":"10.1007","author":[{"given":"Yiji","family":"Zhang","sequence":"first","affiliation":[]},{"given":"Lenore D.","family":"Zuck","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,11,29]]},"reference":[{"key":"3_CR1","unstructured":"Coq development team. The Coq proof assistant. \nhttps:\/\/coq.inria.fr\/"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Alpern, B., Wegman, M.N., Zadeck, F.K.: Detecting equality of variables in programs. In: POPL 1988, pp. 1\u201311. ACM, New York (1988)","DOI":"10.1145\/73560.73561"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/978-3-540-27813-9_49","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2004","unstructured":"Barrett, C., Berezin, S.: CVC lite: a new implementation of the cooperating validity checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 515\u2013518. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-27813-9_49"},{"issue":"1","key":"3_CR4","doi-asserted-by":"crossref","first-page":"4:1","DOI":"10.1145\/2579080","volume":"36","author":"G Barthe","year":"2014","unstructured":"Barthe, G., Demange, D., Pichardie, D.: Formal verification of an SSA-based middle-end for CompCert. TOPLAS 36(1), 4:1\u20134:35 (2014)","journal-title":"TOPLAS"},{"issue":"6","key":"3_CR5","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1145\/966221.966235","volume":"28","author":"MA Dave","year":"2003","unstructured":"Dave, M.A.: Compiler verification: a bibliography. SIGSOFT SEN 28(6), 2 (2003)","journal-title":"SIGSOFT SEN"},{"issue":"3","key":"3_CR6","first-page":"21","volume":"176","author":"Y Fang","year":"2007","unstructured":"Fang, Y., Zuck, L.D.: Improved invariant generation for TVOC. ENTCS 176(3), 21\u201335 (2007)","journal-title":"ENTCS"},{"key":"3_CR7","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume":"19","author":"R Floyd","year":"1967","unstructured":"Floyd, R.: Assigning meanings to programs. Proc. Symp. Appl. Math. 19, 19\u201332 (1967)","journal-title":"Proc. Symp. Appl. Math."},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-662-46081-8_17","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Gjomemo","year":"2015","unstructured":"Gjomemo, R., Namjoshi, K.S., Phung, P.H., Venkatakrishnan, V.N., Zuck, L.D.: From verification to optimizations. In: DSouza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 300\u2013317. Springer, Heidelberg (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-662-46081-8_17"},{"issue":"1","key":"3_CR9","first-page":"53","volume":"132","author":"B Goldberg","year":"2005","unstructured":"Goldberg, B., Zuck, L., Barrett, C.: Into the loops: practical issues in translation validation for optimizing compilers. ENTCS 132(1), 53\u201371 (2005)","journal-title":"ENTCS"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The seahorn verification framework. In: CAV, pp. 343\u2013361 (2015)","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"3_CR11","first-page":"40","volume":"375","author":"WA Hunt Jr","year":"2017","unstructured":"Hunt Jr., W.A., Kaufmann, M., Moore, J.S., Slobodova, A.: Industrial hardware and software verification with ACL2. Philos. Trans. R. Soc. 375, 40 (2017). (Article Number 20150399)","journal-title":"Philos. Trans. R. Soc."},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Le, V., Sun, C., Su, Z.: Randomized stress-testing of link-time optimizers. In: ISSTA, pp. 327\u2013337. ACM(2015)","DOI":"10.1145\/2771783.2771785"},{"key":"3_CR13","first-page":"131","volume":"178","author":"KRM Leino","year":"2008","unstructured":"Leino, K.R.M.: This is boogie 2. Manuscript KRML 178, 131 (2008)","journal-title":"Manuscript KRML"},{"issue":"5","key":"3_CR14","doi-asserted-by":"crossref","first-page":"220","DOI":"10.1145\/780822.781156","volume":"38","author":"S Lerner","year":"2003","unstructured":"Lerner, S., Millstein, T., Chambers, C.: Automatically proving the correctness of compiler optimizations. ACM SIGPLAN Not. 38(5), 220\u2013231 (2003)","journal-title":"ACM SIGPLAN Not."},{"issue":"7","key":"3_CR15","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"issue":"6","key":"3_CR16","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1145\/2813885.2737965","volume":"50","author":"NP Lopes","year":"2015","unstructured":"Lopes, N.P., Menendez, D., Nagarakatte, S., Regehr, J.: Provably correct peephole optimizations with alive. ACM SIGPLAN Not. 50(6), 22\u201332 (2015)","journal-title":"ACM SIGPLAN Not."},{"key":"3_CR17","first-page":"219","volume":"1","author":"J McCarthy","year":"1967","unstructured":"McCarthy, J., Painter, J.: Correctness of a compiler for arithmetic expressions. Math. Aspects Comput. Sci. 1, 219\u2013222 (1967)","journal-title":"Math. Aspects Comput. Sci."},{"key":"3_CR18","unstructured":"Namjoshi, K.S.: Witnessing an SSA transformation. In: VeriSure Workshop and Personal Communication, CAV 2014 (2014). \nhttp:\/\/ect.bell-labs.com\/who\/knamjoshi\/papers\/Namjoshi-VeriSure-CAV-2014.pdf"},{"key":"3_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/978-3-662-53413-7_19","volume-title":"Static Analysis","author":"KS Namjoshi","year":"2016","unstructured":"Namjoshi, K.S., Singhania, N.: Loopy: programmable and formally verified loop transformations. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 383\u2013402. Springer, Heidelberg (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-662-53413-7_19"},{"issue":"5","key":"3_CR20","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1145\/358438.349314","volume":"35","author":"GC Necula","year":"2000","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler. ACM Sigplan Not. 35(5), 83\u201394 (2000)","journal-title":"ACM Sigplan Not."},{"key":"3_CR21","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. 1384, pp. 151\u2013166. Springer, Heidelberg (1998). \nhttps:\/\/doi.org\/10.1007\/BFb0054170"},{"key":"3_CR22","unstructured":"Pnueli, A., Zaks, A.: Translation validation of interprocedural optimizations. In: International Workshop on Software Verification and Validation (2006)"},{"key":"3_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/978-3-319-08867-9_7","volume-title":"Computer Aided Verification","author":"Z Rakamari\u0107","year":"2014","unstructured":"Rakamari\u0107, Z., Emmi, M.: SMACK: decoupling source language details from verifier implementations. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 106\u2013113. Springer, Cham (2014). \nhttps:\/\/doi.org\/10.1007\/978-3-319-08867-9_7"},{"key":"3_CR24","unstructured":"Samet, H.: Automatically proving the correctness of translations involving optimized code. PhD thesis, Stanford University (1975)"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Schmidt, D.A.: Data flow analysis is model checking of abstract interpretations. In: POPL (1998), pp. 38\u201348. ACM (1998)","DOI":"10.1145\/268946.268950"},{"issue":"6","key":"3_CR26","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1145\/1993316.1993532","volume":"46","author":"X Yang","year":"2011","unstructured":"Yang, X., Chen, Y., Eide, E., Regehr, J.: Finding and understanding bugs in C compilers. ACM SIGPLAN Not. 46(6), 283\u2013294 (2011)","journal-title":"ACM SIGPLAN Not."},{"key":"3_CR27","unstructured":"Zaks, G.: Ensuring correctness of compiled code. Ph.D. thesis, New York University (2009)"},{"key":"3_CR28","doi-asserted-by":"crossref","unstructured":"Zhao, J., Nagarakatte, S., Martin, M.M.K., Zdancewic, S.: Formalizing the LLVM intermediate representation for verified program transformations. In: ACM SIGPLAN Notices, pp. 427\u2013440. ACM (2012)","DOI":"10.1145\/2103656.2103709"},{"issue":"6","key":"3_CR29","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1145\/2499370.2462164","volume":"48","author":"J Zhao","year":"2013","unstructured":"Zhao, J., Nagarakatte, S., Martin, M.M.K., Zdancewic, S.: Formal verification of SSA-based optimizations for LLVM. ACM SIGPLAN Not. 48(6), 175\u2013186 (2013)","journal-title":"ACM SIGPLAN Not."},{"issue":"3","key":"3_CR30","first-page":"335","volume":"27","author":"L Zuck","year":"2005","unstructured":"Zuck, L., Pnueli, A., Goldberg, B., Barrett, C., Fang, Y., Hu, Y.: Translation and run-time validation of loop transformations. FMSD 27(3), 335\u2013360 (2005)","journal-title":"FMSD"},{"issue":"3","key":"3_CR31","first-page":"223","volume":"9","author":"LD Zuck","year":"2003","unstructured":"Zuck, L.D., Pnueli, A., Goldberg, B.: VOC: a methodology for the translation validation of optimizing compilers. J. UCS 9(3), 223\u2013247 (2003)","journal-title":"J. UCS"}],"container-title":["Lecture Notes in Computer Science","Distributed Computing and Internet Technology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-72344-0_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,11,28]],"date-time":"2017-11-28T12:25:08Z","timestamp":1511871908000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-72344-0_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,11,29]]},"ISBN":["9783319723433","9783319723440"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-72344-0_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,11,29]]}}}