{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,22]],"date-time":"2026-01-22T09:01:17Z","timestamp":1769072477006,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642288685","type":"print"},{"value":"9783642288692","type":"electronic"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"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":[[2012]]},"DOI":"10.1007\/978-3-642-28869-2_3","type":"book-chapter","created":{"date-parts":[[2012,3,22]],"date-time":"2012-03-22T16:44:36Z","timestamp":1332434676000},"page":"47-66","source":"Crossref","is-referenced-by-count":17,"title":["A Formally Verified SSA-Based Middle-End"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[]},{"given":"Delphine","family":"Demange","sequence":"additional","affiliation":[]},{"given":"David","family":"Pichardie","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Alpern, B., Wegman, M.N., Zadeck, F.K.: Detecting equality of variables in programs. In: POPL 1988. ACM (1988)","DOI":"10.1145\/73560.73561"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"Appel, A.W.: SSA is functional programming. SIGPLAN Notices\u00a033 (1998)","DOI":"10.1145\/278283.278285"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"Blech, J.O., Glesner, S., Leitner, J., M\u00fclling, S.: Optimizing code generation from SSA form: A comparison between two formal correctness proofs in Isabelle\/HOL. In: COCV 2005. ENTCS. Elsevier (2005)","DOI":"10.1016\/j.entcs.2005.02.042"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Briggs, P., Cooper, K.D., Harvey, T.J., Simpson, L.T.: Practical improvements to the construction and destruction of static single assignment form. In: SPE (1998)","DOI":"10.1002\/(SICI)1097-024X(19980710)28:8<859::AID-SPE188>3.0.CO;2-8"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Briggs, P., Cooper, K.D., Simpson, L.T.: Value numbering. In: SPE (1997)","DOI":"10.1002\/(SICI)1097-024X(199706)27:6<701::AID-SPE104>3.0.CO;2-0"},{"key":"3_CR6","unstructured":"Companion web page, \n                  \n                    http:\/\/www.irisa.fr\/celtique\/ext\/compcertSSA"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Efficiently computing static single assignment form and the control dependence graph. In: ACM TOPLAS (1991)","DOI":"10.1145\/115372.115320"},{"key":"3_CR8","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-540-75560-9_17","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"Z. Dargaye","year":"2007","unstructured":"Dargaye, Z., Leroy, X.: Mechanized Verification of CPS Transformations. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol.\u00a04790, pp. 211\u2013225. Springer, Heidelberg (2007)"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/11688839_20","volume-title":"Compiler Construction","author":"S. Hack","year":"2006","unstructured":"Hack, S., Grund, D., Goos, G.: Register Allocation for Programs in SSA-Form. In: Mycroft, A., Zeller, A. (eds.) CC 2006. LNCS, vol.\u00a03923, pp. 247\u2013262. Springer, Heidelberg (2006)"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/BFb0026423","volume-title":"Compiler Construction","author":"J. Knoop","year":"1998","unstructured":"Knoop, J., Kosch\u00fctzki, D., Steffen, B.: Basic-Block Graphs: Living Dinosaurs? In: Koskimies, K. (ed.) CC 1998. LNCS, vol.\u00a01383, pp. 65\u201379. Springer, Heidelberg (1998)"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Knoop, J., R\u00fcthing, O., Steffen, B.: Lazy code motion. In: PLDI 1992 (1992)","DOI":"10.1145\/143095.143136"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Lengauer, T., Tarjan, R.E.: A fast algorithm for finding dominators in a flowgraph. In: ACM TOPLAS (1979)","DOI":"10.1145\/357062.357071"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Leroy, X.: A formally verified compiler back-end. JAR\u00a043(4) (2009)","DOI":"10.1007\/s10817-009-9155-4"},{"key":"3_CR14","unstructured":"The LLVM compiler infrastructure, \n                  \n                    http:\/\/llvm.org\/"},{"key":"3_CR15","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":"3_CR16","doi-asserted-by":"crossref","unstructured":"Matsuno, Y., Ohori, A.: A type system equivalent to static single assignment. In: PPDP 2006. ACM (2006)","DOI":"10.1145\/1140335.1140365"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Menon, V., Glew, N., Murphy, B.R., McCreight, A., Shpeisman, T., Adl-Tabatabai, A.R., Petersen, L.: A verifiable SSA program representation for aggressive compiler optimization. In: POPL 2006, ACM (2006)","DOI":"10.1145\/1111037.1111072"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Necula, G.: Translation validation for an optimizing compiler. In: PLDI 2000. ACM (2000)","DOI":"10.1145\/349299.349314"},{"key":"3_CR19","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":"3_CR20","doi-asserted-by":"crossref","unstructured":"Rideau, L., Serpette, B.P., Leroy, X.: Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves. In: JAR (2008)","DOI":"10.1007\/s10817-007-9096-8"},{"key":"3_CR21","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":"3_CR22","doi-asserted-by":"crossref","unstructured":"Tate, R., Stepp, M., Tatlock, Z., Lerner, S.: Equality saturation: a new approach to optimization. In: POPL 2009. ACM (2009)","DOI":"10.1145\/1594834.1480915"},{"key":"3_CR23","doi-asserted-by":"crossref","unstructured":"Tristan, J.B., Govereau, P., Morrisett, G.: Evaluating value-graph translation validation for LLVM. In: PLDI 2011. ACM (2011)","DOI":"10.1145\/1993498.1993533"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Tristan, J.B., Leroy, X.: Verified validation of lazy code motion. In: PLDI 2009. ACM (2009)","DOI":"10.1145\/1542476.1542512"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Tristan, J.B., Leroy, X.: A simple, verified validator for software pipelining. In: POPL 2010. ACM (2010)","DOI":"10.1145\/1706299.1706311"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Zhao, J., Zdancewic, S., Nagarakatte, S., Martin, M.: Formalizing the LLVM intermediate representation for verified program transformation. In: POPL 2012. ACM (2012)","DOI":"10.1145\/2103656.2103709"}],"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-28869-2_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,9]],"date-time":"2020-01-09T03:33:15Z","timestamp":1578540795000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28869-2_3"}},"subtitle":["Static Single Assignment Meets CompCert"],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642288685","9783642288692"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28869-2_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}