{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:45:25Z","timestamp":1770291925830,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662466629","type":"print"},{"value":"9783662466636","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-662-46663-6_12","type":"book-chapter","created":{"date-parts":[[2015,4,1]],"date-time":"2015-04-01T18:37:47Z","timestamp":1427913467000},"page":"233-252","source":"Crossref","is-referenced-by-count":13,"title":["Verifying Fast and Sparse SSA-Based Optimizations in Coq"],"prefix":"10.1007","author":[{"given":"Delphine","family":"Demange","sequence":"first","affiliation":[]},{"given":"David","family":"Pichardie","sequence":"additional","affiliation":[]},{"given":"L\u00e9o","family":"Stefanesco","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Alpern, B., Wegman, M.N., Zadeck, F.K.: Detecting Equality of Variables in Programs. In: Proc. of POPL 1988, pp. 1\u201311. ACM, San Diego (1988) ISBN: 0-89791-252-7","DOI":"10.1145\/73560.73561"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"Barthe, G., Demange, D., Pichardie, D.: Formal Verification of an SSA- Based Middle-End for CompCert. ACM TOPLAS\u00a036(1), 4:1\u20134:35 (2014) ISSN: 0164-0925","DOI":"10.1145\/2579080"},{"key":"12_CR3","series-title":"ENTCS","first-page":"33","volume-title":"COCV 2005","author":"J. Blech","year":"2005","unstructured":"Blech, J., et al.: Optimizing Code Generation from SSA Form: A Comparison Between Two Formal Correctness Proofs in Isabelle\/HOL. In: COCV 2005. ENTCS, pp. 33\u201351. Elsevier, Amsterdam (2005)"},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"Boissinot, B., et al.: Revisiting Out-of-SSA Translation for Correctness, Code Quality and Efficiency. In: Proc. of the 7th Annual IEEE\/ACM International Symposium on Code Generation and Optimization, CGO 2009, pp. 114\u2013125. IEEE Computer Society, Washington, DC (2009) ISBN: 978-0-7695-3576-0","DOI":"10.1109\/CGO.2009.19"},{"issue":"6","key":"12_CR5","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1002\/(SICI)1097-024X(199706)27:6<701::AID-SPE104>3.0.CO;2-0","volume":"27","author":"P. Briggs","year":"1997","unstructured":"Briggs, P., Cooper, K.D., Simpson, L.T.: Value Numbering. Software, Practice and Experience\u00a027(6), 701\u2013724 (1997)","journal-title":"Software, Practice and Experience"},{"key":"12_CR6","first-page":"93","volume-title":"POPL 2010","author":"A. Chlipala","year":"2010","unstructured":"Chlipala, A.: A verified compiler for an impure functional language. In: POPL 2010, pp. 93\u2013106. ACM, New York (2010)"},{"key":"12_CR7","first-page":"273","volume-title":"Proc. of PLDI 1997","author":"F. Chow","year":"1997","unstructured":"Chow, F., et al.: A New Algorithm for Partial Redundancy Elimination Based on SSA Form. In: Proc. of PLDI 1997, pp. 273\u2013286. ACM, New York (1997)"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Kumar, R., et al.: CakeML: A verified implementation of ML. In: Proc. of POPL 2014, pp. 179\u2013192 (2014)","DOI":"10.1145\/2535838.2535841"},{"issue":"1","key":"12_CR9","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1145\/357062.357071","volume":"1","author":"T. Lengauer","year":"1979","unstructured":"Lengauer, T., Tarjan, R.: A fast algorithm for finding dominators in a flowgraph. ACM TOPLAS\u00a01(1), 121\u2013141 (1979)","journal-title":"ACM TOPLAS"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Leroy, X.: A Formally Verified Compiler Back-end. JAR\u00a043(4), 363\u2013446 (2009)","DOI":"10.1007\/s10817-009-9155-4"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/978-3-642-14052-5_26","volume-title":"Interactive Theorem Proving","author":"W. Mansky","year":"2010","unstructured":"Mansky, W., Gunter, E.: A Framework for Formal Verification of Compiler Optimizations. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 371\u2013386. Springer, Heidelberg (2010)"},{"key":"12_CR12","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.D., Singerman, E.: Translation validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 151\u2013166. Springer, Heidelberg (1998)"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/978-3-642-11970-5_13","volume-title":"Compiler Construction","author":"S. Rideau","year":"2010","unstructured":"Rideau, S., Leroy, X.: Validating Register Allocation and Spilling. In: Gupta, R. (ed.) CC 2010. LNCS, vol.\u00a06011, pp. 224\u2013243. Springer, Heidelberg (2010)"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Global Value Numbers and Redundant Computations. In: Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1988, pp. 12\u201327. ACM, San Diego (1988) ISBN:0- 89791-252-7","DOI":"10.1145\/73560.73562"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/978-3-642-22110-1_59","volume-title":"Computer Aided Verification","author":"M. Stepp","year":"2011","unstructured":"Stepp, M., Tate, R., Lerner, S.: Equality-Based Translation Validator for LLVM. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 737\u2013742. Springer, Heidelberg (2011)"},{"key":"12_CR16","first-page":"295","volume-title":"PLDI 2011","author":"J. Tristan","year":"2011","unstructured":"Tristan, J., Govereau, P., Morrisett, G.: Evaluating value-graph translation validation for LLVM. In: PLDI 2011, pp. 295\u2013305. ACM, New York (2011)"},{"key":"12_CR17","first-page":"83","volume-title":"POPL 2010","author":"J. Tristan","year":"2010","unstructured":"Tristan, J., Leroy, X.: A simple, verified validator for software pipelining. In: POPL 2010, pp. 83\u201392. ACM, New York (2010)"},{"key":"12_CR18","first-page":"316","volume-title":"PLDI 2009","author":"J. Tristan","year":"2009","unstructured":"Tristan, J., Leroy, X.: Verified validation of lazy code motion. In: PLDI 2009, pp. 316\u2013326. ACM, New York (2009)"},{"issue":"2","key":"12_CR19","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1145\/103135.103136","volume":"13","author":"M.N. Wegman","year":"1991","unstructured":"Wegman, M.N., Zadeck, F.K.: Constant Propagation with Conditional Branches. ACM Trans. Program. Lang. Syst.\u00a013(2), 181\u2013210 (1991)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"12_CR20","unstructured":"Yang, X., et al.: Finding and Understanding Bugs in C Compilers. In: Proc. of PLDI 2011, pp. 978\u2013971. ACM, New York (2011) ISBN:978-1-4503-0663-8"},{"key":"12_CR21","first-page":"175","volume-title":"PLDI 2013","author":"J. Zhao","year":"2013","unstructured":"Zhao, J., et al.: Formal verification of SSA-based optimizations for LLVM. In: PLDI 2013, pp. 175\u2013186. ACM, New York (2013)"},{"key":"12_CR22","first-page":"427","volume-title":"POPL 2012","author":"J. Zhao","year":"2012","unstructured":"Zhao, J., et al.: Formalizing the LLVM Intermediate Representation for Verified Program Transformation. In: POPL 2012, pp. 427\u2013440. ACM, New York (2012)"}],"container-title":["Lecture Notes in Computer Science","Compiler Construction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-46663-6_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T20:23:59Z","timestamp":1747859039000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-46663-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662466629","9783662466636"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-46663-6_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}