{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,15]],"date-time":"2026-03-15T06:52:13Z","timestamp":1773557533587,"version":"3.50.1"},"reference-count":95,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2009,11,4]],"date-time":"2009-11-04T00:00:00Z","timestamp":1257292800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2009,12]]},"DOI":"10.1007\/s10817-009-9155-4","type":"journal-article","created":{"date-parts":[[2009,11,3]],"date-time":"2009-11-03T09:41:34Z","timestamp":1257241294000},"page":"363-446","source":"Crossref","is-referenced-by-count":369,"title":["A Formally Verified Compiler Back-end"],"prefix":"10.1007","volume":"43","author":[{"given":"Xavier","family":"Leroy","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2009,11,4]]},"reference":[{"key":"9155_CR1","volume-title":"Modern Compiler Implementation in ML","author":"AW Appel","year":"1998","unstructured":"Appel, A.W.: Modern Compiler Implementation in ML. Cambridge University Press, Cambridge (1998)"},{"key":"9155_CR2","first-page":"247","volume-title":"Logic in Computer Science 2001","author":"AW Appel","year":"2001","unstructured":"Appel, A.W.: Foundational proof-carrying code. In: Logic in Computer Science 2001, pp.\u00a0247\u2013258. IEEE Computer Society Press, Silver Spring (2001)"},{"key":"9155_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/978-3-540-74591-4_3","volume-title":"Theorem Proving in Higher Order Logics, 20th Int. Conf. TPHOLs 2007","author":"AW Appel","year":"2007","unstructured":"Appel, A.W., Blazy, S.: Separation logic for small-step Cminor. In: Theorem Proving in Higher Order Logics, 20th Int. Conf. TPHOLs 2007. Lecture Notes in Computer Science, vol. 4732, pp.\u00a05\u201321. Springer, New York (2007)"},{"key":"9155_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1007\/11513988_29","volume-title":"Computer Aided Verification, 17th International Conference, CAV 2005","author":"CW Barrett","year":"2005","unstructured":"Barrett, C.W., Fang, Y., Goldberg, B., Hu, Y., Pnueli, A, Zuck, L.D.: TVOC: a translation validator for optimizing compilers. In: Computer Aided Verification, 17th International Conference, CAV 2005. Lecture Notes in Computer Science, vol. 3576, pp.\u00a0291\u2013295. Springer, New York (2005)"},{"key":"9155_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/3-540-45719-4_4","volume-title":"Proceedings of AMAST\u201902","author":"G Barthe","year":"2002","unstructured":"Barthe, G., Courtieu, P., Dufay, G., Melo de Sousa, S.: Tool-assisted specification and verification of the JavaCard platform. In: Proceedings of AMAST\u201902. Lecture Notes in Computer Science, vol. 2422, pp.\u00a041\u201359. Springer, New York (2002)"},{"key":"9155_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1007\/11737414_9","volume-title":"Functional and Logic Programming, 8th Int. Symp. FLOPS 2006","author":"G Barthe","year":"2006","unstructured":"Barthe, G., Forest, J., Pichardie, D., Rusu, V.: Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant. In: Functional and Logic Programming, 8th Int. Symp. FLOPS 2006. Lecture Notes in Computer Science, vol. 3945, pp.\u00a0114\u2013129. Springer, New York (2006)","edition":"3945"},{"key":"9155_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"301","DOI":"10.1007\/11823230_20","volume-title":"Static Analysis, 13th Int. Symp., SAS 2006","author":"G Barthe","year":"2006","unstructured":"Barthe, G., Gr\u00e9goire, B., Kunz, C., Rezk, T.: Certificate translation for optimizing compilers. In: Static Analysis, 13th Int. Symp., SAS 2006. Lecture Notes in Computer Science, vol. 4134, pp.\u00a0301\u2013317. Springer, New York (2006)"},{"key":"9155_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"368","DOI":"10.1007\/978-3-540-78739-6_28","volume-title":"Programming Languages and Systems, 17th European Symposium on Programming, ESOP 2008","author":"G Barthe","year":"2008","unstructured":"Barthe, G., Kunz, C.: Certificate translation in abstract interpretation. In: Programming Languages and Systems, 17th European Symposium on Programming, ESOP 2008. Lecture Notes in Computer Science, vol. 4960, pp.\u00a0368\u2013382. Springer, New York (2008)"},{"key":"9155_CR9","first-page":"97","volume-title":"International Conference on Functional Programming 2009","author":"N Benton","year":"2009","unstructured":"Benton, N., Hur, C.-K.: Biorthogonality, step-indexing and compiler correctness. In: International Conference on Functional Programming 2009, pp.\u00a097\u2013108. ACM, New York (2009)"},{"key":"9155_CR10","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"3","volume-title":"Proc. 5th Workshop on Compiler Optimization Meets Compiler Verification (COCV 2006)","author":"L Beringer","year":"2007","unstructured":"Beringer, L.: Functional elimination of phi-instructions. In: Proc. 5th Workshop on Compiler Optimization Meets Compiler Verification (COCV 2006). Electronic Notes in Theoretical Computer Science, vol. 176, no. 3, pp.\u00a03\u201320. Elsevier, Amsterdam (2007)"},{"key":"9155_CR11","volume-title":"Interactive Theorem Proving and Program Development\u2014Coq\u2019Art: The Calculus of Inductive Constructions. EATCS Texts in Theoretical Computer Science.","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development\u2014Coq\u2019Art: The Calculus of Inductive Constructions. EATCS Texts in Theoretical Computer Science. Springer, New York (2004)"},{"key":"9155_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1007\/11617990_5","volume-title":"Types for Proofs and Programs, Workshop TYPES 2004","author":"Y Bertot","year":"2006","unstructured":"Bertot, Y., Gr\u00e9goire, B., Leroy, X.: A structured approach to proving compiler optimizations based on dataflow analysis. In: Types for Proofs and Programs, Workshop TYPES 2004. Lecture Notes in Computer Science, vol. 3839, pp.\u00a066\u201381. Springer, New York (2006)","edition":"3839"},{"key":"9155_CR13","first-page":"89","volume-title":"10th Int. Conf. on Principles and Practice of Declarative Programming (PPDP 2008)","author":"Y Bertot","year":"2008","unstructured":"Bertot, Y., Komendantsky, V.: Fixed point semantics and partial recursion in Coq. In: 10th Int. Conf. on Principles and Practice of Declarative Programming (PPDP 2008), pp.\u00a089\u201396. ACM, New York (2008)"},{"key":"9155_CR14","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/s10009-006-0204-6","volume":"8","author":"S Beyer","year":"2006","unstructured":"Beyer, S., Jacobi, C., Kr\u00f6ning, D., Leinenbach, D., Paul, W.: Putting it all together? Formal verification of the VAMP. Int. J. Softw. Tools Technol. Transf. 8, 411\u2013430 (2006)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"9155_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"460","DOI":"10.1007\/11813040_31","volume-title":"FM 2006: Int. Symp. on Formal Methods","author":"S Blazy","year":"2006","unstructured":"Blazy, S., Dargaye, Z., Leroy, X.: Formal verification of a C compiler front-end. In: FM 2006: Int. Symp. on Formal Methods. Lecture Notes in Computer Science, vol. 4085, pp.\u00a0460\u2013475. Springer, New York (2006)","edition":"4085"},{"issue":"3","key":"9155_CR16","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1007\/s10817-009-9148-3","volume":"43","author":"S Blazy","year":"2009","unstructured":"Blazy, S., Leroy, X.: Mechanized semantics for the Clight subset of the C language. J. Autom. Reason. 43(3), 263\u2013288 (2009)","journal-title":"J. Autom. Reason."},{"key":"9155_CR17","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"33","volume-title":"Proc. COCV Workshop (Compiler Optimization meets Compiler Verification","author":"JO Blech","year":"2005","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: Proc. COCV Workshop (Compiler Optimization meets Compiler Verification). Electronic Notes in Theoretical Computer Science, vol. 141, no. 2, pp.\u00a033\u201351. Elsevier, Amsterdam (2005)"},{"key":"9155_CR18","first-page":"261","volume-title":"Programming Language Design and Implementation 2005","author":"H-J Boehm","year":"2005","unstructured":"Boehm, H.-J.: Threads cannot be implemented as a library. In: Programming Language Design and Implementation 2005, pp.\u00a0261\u2013268. ACM, New York (2005)"},{"issue":"1","key":"9155_CR19","doi-asserted-by":"crossref","first-page":"56","DOI":"10.1016\/j.tcs.2005.06.004","volume":"342","author":"D Cachera","year":"2005","unstructured":"Cachera, D., Jensen, T.P., Pichardie, D., Rusu, V.: Extracting a data flow analyser in constructive logic. Theor. Comp. Sci. 342(1), 56\u201378 (2005)","journal-title":"Theor. Comp. Sci."},{"key":"9155_CR20","series-title":"SIGPLAN Notices","first-page":"98","volume-title":"Symposium on Compiler Construction","author":"GJ Chaitin","year":"1982","unstructured":"Chaitin, G.J.: Register allocation and spilling via graph coloring. In: Symposium on Compiler Construction. SIGPLAN Notices, vol. 17, no. 6, pp.\u00a098\u2013105. ACM, New York (1982)","edition":"17"},{"key":"9155_CR21","first-page":"183","volume-title":"Programming Language Design and Implementation 2008","author":"J Chen","year":"2008","unstructured":"Chen, J., Hawblitzel, C., Perry, F., Emmi, M., Condit, J., Coetzee, D., Pratikaki, P.: Type-preserving compilation for large-scale optimizing object-oriented compilers. In: Programming Language Design and Implementation 2008, pp.\u00a0183\u2013192. ACM, New York (2008)"},{"issue":"2","key":"9155_CR22","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1145\/5397.30847","volume":"8","author":"L Chirica","year":"1986","unstructured":"Chirica, L., Martin, A.: Toward compiler implementation correctness proofs. ACM Trans. Program. Lang. Syst. 8(2), 185\u2013214 (1986)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9155_CR23","first-page":"54","volume-title":"Programming Language Design and Implementation 2007","author":"AJ Chlipala","year":"2007","unstructured":"Chlipala, A.J.: A certified type-preserving compiler from lambda calculus to assembly language. In: Programming Language Design and Implementation 2007, pp.\u00a054\u201365. ACM, New York (2007)"},{"key":"9155_CR24","first-page":"430","volume-title":"IEEE Conf. on Soft. Engineering","author":"G Clemmensen","year":"1984","unstructured":"Clemmensen, G., Oest, O.: Formal specification and development of an Ada compiler. In: IEEE Conf. on Soft. Engineering, pp.\u00a0430\u2013440. IEEE Computer Society Press, Silver Spring (1984)"},{"key":"9155_CR25","unstructured":"Coq Development Team: The Coq proof assistant. http:\/\/coq.inria.fr\/ (1989\u20132009)"},{"key":"9155_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/11617990_8","volume-title":"Types for Proofs and Programs, Workshop TYPES 2004","author":"S Coupet-Grimal","year":"2006","unstructured":"Coupet-Grimal, S., Delobel, W.: A uniform and certified approach for two static analyses. In: Types for Proofs and Programs, Workshop TYPES 2004. Lecture Notes in Computer Science, vol.\u00a03839, pp.\u00a0115\u2013137. Springer, New York (2006)"},{"key":"9155_CR27","unstructured":"Dargaye, Z.: V\u00e9rification formelle d\u2019un compilateur pour langages fonctionnels. Ph.D. thesis, University Paris\u00a07 Denis Diderot (2009)"},{"issue":"6","key":"9155_CR28","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 Softw. Eng. Notes 28(6), 2 (2003)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"9155_CR29","series-title":"BRICS Notes","first-page":"13","volume-title":"Int. Workshop on Software Tools for Technology Transfer, STTT 1998","author":"A Dold","year":"1998","unstructured":"Dold, A., Gaul, T., Zimmermann, W.: Mechanized verification of compiler backends. In: Int. Workshop on Software Tools for Technology Transfer, STTT 1998. BRICS Notes, vol. NS-98-4, pp.\u00a013\u201324. University of Aarhus, Aarhus (1998)"},{"key":"9155_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"144","DOI":"10.1007\/3-540-45294-X_13","volume-title":"Proc. FST TCS 2001","author":"A Dold","year":"2001","unstructured":"Dold, A., Vialard, V.: A mechanically verified compiling specification for a Lisp compiler. In: Proc. FST TCS 2001. Lecture Notes in Computer Science, vol. 2245, pp.\u00a0144\u2013155. Springer, New York (2001)"},{"key":"9155_CR31","first-page":"255","volume-title":"Proceedings of the 8th ACM & IEEE International Conference on Embedded Software, EMSOFT 2008","author":"E Eide","year":"2008","unstructured":"Eide, E., Regehr, J.: Volatiles are miscompiled, and what to do about it. In: Proceedings of the 8th ACM & IEEE International Conference on Embedded Software, EMSOFT 2008, pp.\u00a0255\u2013264. ACM, New York (2008)"},{"key":"9155_CR32","volume-title":"Bulldog: a compiler for VLSI architectures. ACM Doctoral Dissertation Awards series","author":"JR Ellis","year":"1986","unstructured":"Ellis, J.R.: Bulldog: a compiler for VLSI architectures. ACM Doctoral Dissertation Awards series. The MIT Press, Cambridge (1986)"},{"key":"9155_CR33","first-page":"67","volume-title":"Int. Workshop on Types in Language Design and Implementation (TLDI\u201907)","author":"X Feng","year":"2007","unstructured":"Feng, X., Ni, Z., Shao, Z., Guo, Y.: An open framework for foundational proof-carrying code. In: Int. Workshop on Types in Language Design and Implementation (TLDI\u201907), pp.\u00a067\u201378. ACM, New York (2007)"},{"key":"9155_CR34","series-title":"Lecture Notes in Computer Science","first-page":"25","volume-title":"Theorem Proving in Higher Order Logics, 16th International Conference, TPHOLs 2003","author":"ACJ Fox","year":"2003","unstructured":"Fox, A.C.J.: Formal specification and verification of ARM6. In: Theorem Proving in Higher Order Logics, 16th International Conference, TPHOLs 2003. Lecture Notes in Computer Science, vol. 2758, pp.\u00a025\u201340. Springer, New York (2003)"},{"issue":"3","key":"9155_CR35","doi-asserted-by":"crossref","first-page":"300","DOI":"10.1145\/229542.229546","volume":"18","author":"L George","year":"1996","unstructured":"George, L., Appel, A.W.: Iterated register coalescing. ACM Trans. Program. Lang. Syst. 18(3), 300\u2013324 (1996)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9155_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1007\/3-540-48092-7_10","volume-title":"Correct System Design, Recent Insight and Advances","author":"G Goos","year":"1999","unstructured":"Goos, G., Zimmermann, W.: Verification of compilers. In: Correct System Design, Recent Insight and Advances. Lecture Notes in Computer Science, vol. 1710, pp.\u00a0201\u2013230. Springer, New York (1999)"},{"key":"9155_CR37","unstructured":"Gr\u00e9goire, B.: Compilation des termes de preuves: un (nouveau) mariage entre Coq et OCaml. Ph.D. thesis, University Paris 7 (2003)"},{"key":"9155_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1007\/978-3-540-27864-1_17","volume-title":"Static Analysis, 11th Int. Symposium, SAS 2004","author":"S Gulwani","year":"2004","unstructured":"Gulwani, S., Necula, G.C.: A polynomial-time algorithm for global value numbering. In: Static Analysis, 11th Int. Symposium, SAS 2004. Lecture Notes in Computer Science, vol. 3148, pp.\u00a0212\u2013227. Springer, New York (2004)"},{"issue":"1\u20132","key":"9155_CR39","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/BF01128407","volume":"8","author":"J Guttman","year":"1995","unstructured":"Guttman, J., Monk, L., Ramsdell, J., Farmer, W., Swarup, V.: The VLISP verified scheme system. LISP Symb. Comput. 8(1\u20132), 33\u2013110 (1995)","journal-title":"LISP Symb. Comput."},{"issue":"11","key":"9155_CR40","first-page":"1370","volume":"55","author":"TC Hales","year":"2008","unstructured":"Hales, T.C.: Formal proof. Not. Am. Math. Soc. 55(11), 1370\u20131380 (2008)","journal-title":"Not. Am. Math. Soc."},{"issue":"4","key":"9155_CR41","doi-asserted-by":"crossref","first-page":"517","DOI":"10.1145\/503112.503115","volume":"33","author":"PH Hartel","year":"2001","unstructured":"Hartel, P.H., Moreau, L.A.V.: Formalizing the safety of Java, the Java virtual machine and Java Card. ACM Comput. Surv. 33(4), 517\u2013558 (2001)","journal-title":"ACM Comput. Surv."},{"key":"9155_CR42","series-title":"SIGPLAN Notices","first-page":"150","volume-title":"International Symposium on Memory Management 2002","author":"F Henderson","year":"2003","unstructured":"Henderson, F.: Accurate garbage collection in an uncooperative environment. In: International Symposium on Memory Management 2002. SIGPLAN Notices, vol. 38, no. 2, pp.\u00a0150\u2013156. ACM, New York (2003)"},{"key":"9155_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/978-3-540-78739-6_27","volume-title":"Programming Languages and Systems, 17th European Symposium on Programming, ESOP 2008","author":"A Hobor","year":"2008","unstructured":"Hobor, A., Appel, A.W., Zappa Nardelli, F.: Oracle semantics for concurrent separation logic. In: Programming Languages and Systems, 17th European Symposium on Programming, ESOP 2008. Lecture Notes in Computer Science, vol. 4960, pp.\u00a0353\u2013367. Springer, New York (2008)"},{"key":"9155_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1007\/11823230_19","volume-title":"Static Analysis, 13th Int. Symp., SAS 2006","author":"Q Huang","year":"2006","unstructured":"Huang, Q., Childers, B.R., Soffa, M.L.: Catching and identifying bugs in register allocation. In: Static Analysis, 13th Int. Symp., SAS 2006. Lecture Notes in Computer Science, vol. 4134, pp.\u00a0281\u2013300. Springer, New York (2006)"},{"issue":"5","key":"9155_CR45","doi-asserted-by":"crossref","first-page":"549","DOI":"10.1017\/S0956796897002864","volume":"7","author":"GP Huet","year":"1997","unstructured":"Huet, G.P.: The zipper. J. Funct. Program. 7(5), 549\u2013554 (1997)","journal-title":"J. Funct. Program."},{"key":"9155_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"284","DOI":"10.1007\/3-540-46428-X_20","volume-title":"Fundamental Approaches to Software Engineering, 3rd Int. Conf. FASE 2000","author":"M Huisman","year":"2000","unstructured":"Huisman, M., Jacobs, B.: Java program verification via a Hoare logic with abrupt termination. In: Fundamental Approaches to Software Engineering, 3rd Int. Conf. FASE 2000. Lecture Notes in Computer Science, vol. 1783, pp.\u00a0284\u2013303. Springer, New York (2000)"},{"key":"9155_CR47","volume-title":"The PowerPC Architecture","author":"IBM Corporation","year":"1994","unstructured":"IBM Corporation: The PowerPC Architecture. Morgan Kaufmann, San Francisco (1994)"},{"key":"9155_CR48","first-page":"194","volume-title":"1st Symposium Principles of Programming Languages","author":"GA Kildall","year":"1973","unstructured":"Kildall, G.A.: A unified approach to global program optimization. In: 1st Symposium Principles of Programming Languages, pp.\u00a0194\u2013206. ACM, New York (1973)"},{"issue":"4","key":"9155_CR49","doi-asserted-by":"crossref","first-page":"619","DOI":"10.1145\/1146809.1146811","volume":"28","author":"G Klein","year":"2006","unstructured":"Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. ACM Trans. Program. Lang. Syst. 28(4), 619\u2013695 (2006)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9155_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1007\/BFb0026423","volume-title":"Proc. Compiler Construction \u201998","author":"J Knoop","year":"1998","unstructured":"Knoop, J., Kosch\u00fctzki, D., Steffen, B.: Basic-block graphs: living dinosaurs? In: Proc. Compiler Construction \u201998. Lecture Notes in Computer Science, vol. 1383, pp.\u00a065\u201379. Springer, New York (1998)"},{"issue":"4","key":"9155_CR51","doi-asserted-by":"crossref","first-page":"1117","DOI":"10.1145\/183432.183443","volume":"16","author":"J Knoop","year":"1994","unstructured":"Knoop, J., R\u00fcthing, O., Steffen, B.: Optimal code motion: theory and practice. ACM Trans. Program. Lang. Syst. 16(4), 1117\u20131155 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9155_CR52","first-page":"283","volume-title":"29th Symposium 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: 29th Symposium Principles of Programming Languages, pp.\u00a0283\u2013294. ACM, New York (2002)"},{"key":"9155_CR53","first-page":"2","volume-title":"Int. Conf. on Software Engineering and Formal Methods (SEFM 2005)","author":"D Leinenbach","year":"2005","unstructured":"Leinenbach, D., Paul, W., Petrova, E.: Towards the formal verification of a C0 compiler: code generation and implementation correctness. In: Int. Conf. on Software Engineering and Formal Methods (SEFM 2005), pp.\u00a02\u201311. IEEE Computer Society Press, Silver Spring (2005)"},{"key":"9155_CR54","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"23","volume-title":"3rd Int. Workshop on Systems Software Verification (SSV 2008)","author":"D Leinenbach","year":"2008","unstructured":"Leinenbach, D., Petrova, E.: Pervasive compiler verification. In: 3rd Int. Workshop on Systems Software Verification (SSV 2008). Electronic Notes in Theoretical Computer Science, vol. 217, no. 21, pp.\u00a023\u201340. Elsevier, Amsterdam (2008)"},{"key":"9155_CR55","first-page":"364","volume-title":"32nd Symposium Principles of Programming Languages","author":"S Lerner","year":"2005","unstructured":"Lerner, S., Millstein, T., Rice, E., Chambers, C.: Automated soundness proofs for dataflow analyses and transformations via local rules. In: 32nd Symposium Principles of Programming Languages, pp.\u00a0364\u2013377. ACM, New York (2005)"},{"issue":"3\u20134","key":"9155_CR56","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1023\/A:1025055424017","volume":"30","author":"X Leroy","year":"2003","unstructured":"Leroy, X.: Java bytecode verification: algorithms and formalizations. J. Autom. Reason. 30(3\u20134), 235\u2013269 (2003)","journal-title":"J. Autom. Reason."},{"key":"9155_CR57","first-page":"42","volume-title":"33rd Symposium 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: 33rd Symposium Principles of Programming Languages, pp.\u00a042\u201354. ACM, New York (2006)"},{"key":"9155_CR58","unstructured":"Leroy, X.: The Compcert verified compiler, software and commented proof. http:\/\/compcert.inria.fr\/ (2009)"},{"issue":"1","key":"9155_CR59","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/s10817-008-9099-0","volume":"41","author":"X Leroy","year":"2008","unstructured":"Leroy, X., Blazy, S.: Formal verification of a C-like memory model and its uses for verifying program transformations. J. Autom. Reason. 41(1), 1\u201331 (2008)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"9155_CR60","doi-asserted-by":"crossref","first-page":"284","DOI":"10.1016\/j.ic.2007.12.004","volume":"207","author":"X Leroy","year":"2009","unstructured":"Leroy, X., Grall, H.: Coinductive big-step operational semantics. Inf. Comput. 207(2), 284\u2013304 (2009)","journal-title":"Inf. Comput."},{"key":"9155_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/3-540-39185-1_12","volume-title":"Types for Proofs and Programs, Workshop TYPES 2002","author":"P Letouzey","year":"2003","unstructured":"Letouzey, P.: A new extraction for Coq. In: Types for Proofs and Programs, Workshop TYPES 2002. Lecture Notes in Computer Science, vol. 2646, pp.\u00a0200\u2013219. Springer, New York (2003)"},{"key":"9155_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1007\/978-3-540-69407-6_39","volume-title":"Logic and Theory of Algorithms, Fourth Conference on Computability in Europe, CiE 2008","author":"P Letouzey","year":"2008","unstructured":"Letouzey, P.: Extraction in Coq: an overview. In: Logic and Theory of Algorithms, Fourth Conference on Computability in Europe, CiE 2008. Lecture Notes in Computer Science, vol. 5028, pp.\u00a0359\u2013369. Springer, New York (2008)"},{"key":"9155_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1007\/978-3-540-71316-6_15","volume-title":"Programming Languages and Systems, 16th European Symposium on Programming, ESOP 2007","author":"G Li","year":"2007","unstructured":"Li, G., Owens, S., Slind, K.: Structure of a proof-producing compiler for a subset of higher order logic. In: Programming Languages and Systems, 16th European Symposium on Programming, ESOP 2007. Lecture Notes in Computer Science, vol. 4421, pp.\u00a0205\u2013219. Springer, New York (2007)"},{"key":"9155_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/978-3-540-73595-3_3","volume-title":"Automated Deduction, CADE-21","author":"G Li","year":"2007","unstructured":"Li, G., Slind, K.: Compilation as rewriting in higher order logic. In: Automated Deduction, CADE-21. Lecture Notes in Computer Science, vol. 4603, pp.\u00a019\u201334. Springer, New York (2007)"},{"key":"9155_CR65","first-page":"3","volume-title":"Proceedings of the Sixth International Workshop on Automated Debugging, AADEBUG 2005","author":"C Lindig","year":"2005","unstructured":"Lindig, C.: Random testing of C calling conventions. In: Proceedings of the Sixth International Workshop on Automated Debugging, AADEBUG 2005, pp.\u00a03\u201312. ACM, New York (2005)"},{"key":"9155_CR66","series-title":"Proc. of Symposia in Applied Mathematics","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1090\/psapm\/019\/0242403","volume-title":"Mathematical Aspects of Computer Science","author":"J McCarthy","year":"1967","unstructured":"McCarthy, J., Painter, J.: Correctness of a compiler for arithmetical expressions. In: Mathematical Aspects of Computer Science. Proc. of Symposia in Applied Mathematics, vol.\u00a019, pp.\u00a033\u201341. American Mathematical Society, Providence (1967)"},{"issue":"1","key":"9155_CR67","first-page":"100","volume":"10","author":"WM McKeeman","year":"1998","unstructured":"McKeeman, W.M.: Differential testing for software. Digit. Tech. J. 10(1), 100\u2013107 (1998)","journal-title":"Digit. Tech. J."},{"key":"9155_CR68","series-title":"Machine Intelligence","volume-title":"Proc. 7th Annual Machine Intelligence Workshop","author":"R Milner","year":"1972","unstructured":"Milner, R., Weyhrauch, R.: Proving compiler correctness in a mechanized logic. In: Meltzer, B., Michie, D. (eds.) Proc. 7th Annual Machine Intelligence Workshop. Machine Intelligence, vol.\u00a07, pp.\u00a051\u201372. Edinburgh University Press, Edinburgh (1972)"},{"issue":"4","key":"9155_CR69","first-page":"461","volume":"5","author":"JS Moore","year":"1989","unstructured":"Moore, J.S.: A mechanically verified language implementation. J. Autom. Reason. 5(4), 461\u2013492 (1989)","journal-title":"J. Autom. Reason."},{"key":"9155_CR70","volume-title":"Piton: a Mechanically Verified Assembly-Language","author":"JS Moore","year":"1996","unstructured":"Moore, J.S.: Piton: a Mechanically Verified Assembly-Language. Kluwer, Dordrecht (1996)"},{"issue":"1","key":"9155_CR71","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1017\/S0956796801004178","volume":"12","author":"G Morrisett","year":"2002","unstructured":"Morrisett, G., Crary, K., Glew, N., Walker, D.: Stack-based typed assembly language. J. Funct. Program. 12(1), 43\u201388 (2002)","journal-title":"J. Funct. Program."},{"issue":"3","key":"9155_CR72","doi-asserted-by":"crossref","first-page":"528","DOI":"10.1145\/319301.319345","volume":"21","author":"G Morrisett","year":"1999","unstructured":"Morrisett, G., Walker, D., Crary, K., Glew, N.: From System F to typed assembly language. ACM Trans. Program. Lang. Syst. 21(3), 528\u2013569 (1999)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9155_CR73","volume-title":"Advanced Compiler Design and Implementation","author":"SS Muchnick","year":"1997","unstructured":"Muchnick, S.S.: Advanced Compiler Design and Implementation. Morgan Kaufmann, San Francisco (1997)"},{"key":"9155_CR74","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0027453","volume-title":"Modular Compiler Verification: a Refinement-Algebraic Approach Advocating Stepwise Abstraction","author":"M M\u00fcller-Olm","year":"1997","unstructured":"M\u00fcller-Olm, M.: Modular Compiler Verification: a Refinement-Algebraic Approach Advocating Stepwise Abstraction. Lecture Notes in Computer Science, vol. 1283. Springer, New York (1997)"},{"key":"9155_CR75","first-page":"106","volume-title":"24th Symposium Principles of Programming Languages","author":"GC Necula","year":"1997","unstructured":"Necula, G.C.: Proof-carrying code. In: 24th Symposium Principles of Programming Languages, pp.\u00a0106\u2013119. ACM, New York (1997)"},{"key":"9155_CR76","first-page":"83","volume-title":"Programming Language Design and Implementation 2000","author":"GC Necula","year":"2000","unstructured":"Necula, G.C.: Translation validation for an optimizing compiler. In: Programming Language Design and Implementation 2000, pp.\u00a083\u201395. ACM, New York (2000)"},{"key":"9155_CR77","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/3-540-45937-5_16","volume-title":"Compiler Construction, 11th International Conference, CC 2002","author":"GC Necula","year":"2002","unstructured":"Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: intermediate language and tools for analysis and transformation of C programs. In: Compiler Construction, 11th International Conference, CC 2002. Lecture Notes in Computer Science, vol. 2304, pp.\u00a0213\u2013228. Springer, New York (2002)"},{"key":"9155_CR78","first-page":"142","volume-title":"28th Symposium Principles of Programming Languages","author":"GC Necula","year":"2001","unstructured":"Necula, G.C., Rahul, S.P.: Oracle-based checking of untrusted software. In: 28th Symposium Principles of Programming Languages, pp.\u00a0142\u2013154. ACM, New York (2001)"},{"issue":"1\u20133","key":"9155_CR79","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"PW O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency and local reasoning. Theor. Comp. Sci. 375(1\u20133), 271\u2013307 (2007)","journal-title":"Theor. Comp. Sci."},{"key":"9155_CR80","unstructured":"Paul, W., et\u00a0al.: The Verisoft project. http:\/\/www.verisoft.de\/ (2003\u20132008)"},{"key":"9155_CR81","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/10704567_1","volume-title":"PPDP\u201999: International Conference on Principles and Practice of Declarative Programming","author":"SL Peyton Jones","year":"1999","unstructured":"Peyton Jones, S.L., Ramsey, N., Reig, F.: C- -: a portable assembly language that supports garbage collection. In: PPDP\u201999: International Conference on Principles and Practice of Declarative Programming. Lecture Notes in Computer Science, vol. 1702, pp.\u00a01\u201328. Springer, New York (1999)"},{"key":"9155_CR82","unstructured":"Pichardie, D.: Interpr\u00e9tation abstraite en logique intuitionniste: extraction d\u2019analyseurs Java certifi\u00e9s. Ph.D. thesis, University Rennes 1 (2005)"},{"key":"9155_CR83","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/BFb0054170","volume-title":"Tools and Algorithms for Construction and Analysis of Systems, TACAS \u201998","author":"A Pnueli","year":"1998","unstructured":"Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Tools and Algorithms for Construction and Analysis of Systems, TACAS \u201998. Lecture Notes in Computer Science, vol. 1384, pp.\u00a0151\u2013166. Springer, New York (1998)"},{"key":"9155_CR84","unstructured":"Pop, S.: The SSA representation framework: semantics, analyses and GCC implementation. Ph.D. thesis, \u00c9cole des Mines de Paris (2006)"},{"issue":"4","key":"9155_CR85","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1007\/s10817-007-9096-8","volume":"40","author":"L Rideau","year":"2008","unstructured":"Rideau, L., Serpette, B.P., Leroy, X.: Tilting at windmills with Coq: formal verification of a compilation algorithm for parallel moves. J. Autom. Reason. 40(4), 307\u2013326 (2008)","journal-title":"J. Autom. Reason."},{"key":"9155_CR86","unstructured":"Rinard, M., Marinov, D.: Credible compilation with pointers. In: Proc. FLoC Workshop on Run-Time Result Verification (1999)"},{"key":"9155_CR87","first-page":"1","volume-title":"31st Symposium Principles of Programming Languages","author":"X Rival","year":"2004","unstructured":"Rival, X.: Symbolic transfer function-based approaches to certified compilation. In: 31st Symposium Principles of Programming Languages, pp.\u00a01\u201313. ACM, New York (2004)"},{"key":"9155_CR88","first-page":"12","volume-title":"15th Symposium Principles of Programming Languages","author":"BK Rosen","year":"1988","unstructured":"Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Global value numbers and redundant computations. In: 15th Symposium Principles of Programming Languages, pp.\u00a012\u201327. ACM, New York (1988)"},{"issue":"1","key":"9155_CR89","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1053468.1053469","volume":"27","author":"Z Shao","year":"2005","unstructured":"Shao, Z., Trifonov, V., Saha, B., Papaspyrou, N.: A type system for certified binaries. ACM Trans. Program. Lang. Syst. 27(1), 1\u201345 (2005)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9155_CR90","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-59495-3","volume-title":"Java and the Java Virtual Machine","author":"R St\u00e4rk","year":"2001","unstructured":"St\u00e4rk, R., Schmid, J., B\u00f6rger, E.: Java and the Java Virtual Machine. Springer, New York (2001)"},{"key":"9155_CR91","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1007\/3-540-45620-1_5","volume-title":"Proc. Conference on Automated Deduction (CADE)","author":"M Strecker","year":"2002","unstructured":"Strecker, M.: Formal verification of a Java compiler in Isabelle. In: Proc. Conference on Automated Deduction (CADE). Lecture Notes in Computer Science, vol. 2392, pp.\u00a063\u201377. Springer, New York (2002)"},{"key":"9155_CR92","unstructured":"Strecker, M.: Compiler verification for C0 (intermediate report). Technical report, Universit\u00e9 Paul Sabatier, Toulouse (2005)"},{"key":"9155_CR93","first-page":"17","volume-title":"35th Symposium 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: 35th Symposium Principles of Programming Languages, pp.\u00a017\u201327. ACM, New York (2008)"},{"key":"9155_CR94","first-page":"316","volume-title":"Programming Language Design and Implementation 2009","author":"J-B Tristan","year":"2009","unstructured":"Tristan, J.-B., Leroy, X.: Verified validation of Lazy Code Motion. In: Programming Language Design and Implementation 2009, pp.\u00a0316\u2013326. ACM, New York (2009)"},{"key":"9155_CR95","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"2","volume-title":"COCV\u201902, Compiler Optimization Meets Compiler Verification","author":"LD Zuck","year":"2002","unstructured":"Zuck, L.D., Pnueli, A., Fang, Y., Goldberg, B.: VOC: a translation validator for optimizing compilers. In: COCV\u201902, Compiler Optimization Meets Compiler Verification. Electronic Notes in Theoretical Computer Science, vol. 65, no. 2, pp.\u00a02\u201318. Elsevier, Amsterdam (2002)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9155-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-009-9155-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-009-9155-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T01:21:49Z","timestamp":1559265709000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-009-9155-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,11,4]]},"references-count":95,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2009,12]]}},"alternative-id":["9155"],"URL":"https:\/\/doi.org\/10.1007\/s10817-009-9155-4","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,11,4]]}}}