{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:53:46Z","timestamp":1750308826146,"version":"3.41.0"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2009,6,1]],"date-time":"2009-06-01T00:00:00Z","timestamp":1243814400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2009,6]]},"abstract":"<jats:p>Proof Carrying Code provides trust in mobile code by requiring certificates that ensure the code adherence to specific conditions. The prominent approach to generate certificates for compiled code is Certifying Compilation, that automatically generates certificates for simple safety properties.<\/jats:p>\n          <jats:p>In this work, we present Certificate Translation, a novel extension for standard compilers that automatically transforms formal proofs for more expressive and complex properties of the source program to certificates for the compiled code.<\/jats:p>\n          <jats:p>The article outlines the principles of certificate translation, instantiated for a nonoptimizing compiler and for standard compiler optimizations in the context of an intermediate RTL Language.<\/jats:p>","DOI":"10.1145\/1538917.1538919","type":"journal-article","created":{"date-parts":[[2009,6,30]],"date-time":"2009-06-30T13:10:17Z","timestamp":1246367417000},"page":"1-45","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Certificate translation for optimizing compilers"],"prefix":"10.1145","volume":"31","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[{"name":"IMDEA Software"}]},{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"additional","affiliation":[{"name":"INRIA Sophia Antipolis\u2014M\u00e9diterran\u00e9e"}]},{"given":"C\u00e9sar","family":"Kunz","sequence":"additional","affiliation":[{"name":"INRIA Sophia Antipolis\u2014M\u00e9diterran\u00e9e"}]},{"given":"Tamara","family":"Rezk","sequence":"additional","affiliation":[{"name":"INRIA Sophia Antipolis\u2014M\u00e9diterran\u00e9e"}]}],"member":"320","published-online":{"date-parts":[[2009,7,3]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_2_1_1_1","DOI":"10.1016\/j.entcs.2005.02.026"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_1","DOI":"10.1007\/11804192_17"},{"doi-asserted-by":"publisher","key":"e_1_2_1_3_1","DOI":"10.1007\/978-3-540-30569-9_3"},{"doi-asserted-by":"publisher","key":"e_1_2_1_4_1","DOI":"10.1007\/11513988_29"},{"key":"e_1_2_1_5_1","volume-title":"Lecture Notes in Computer Science","volume":"4709","author":"Barthe G.","unstructured":"]] Barthe , G. , Burdy , L. , Charles , J. , Gr\u00e9goire , B. , Huisman , M. , Lanet , J.-L. , Pavlova , M. , and Requet , A . 2007. JACK: A tool for validation of security and behaviour of Java applications. In Formal Methods for Components and Objects: Revised Lectures from the 5th International Symposium (FMCO'06) . Lecture Notes in Computer Science , vol. 4709 , Springer-Verlag, 152--174. ]]Barthe, G., Burdy, L., Charles, J., Gr\u00e9goire, B., Huisman, M., Lanet, J.-L., Pavlova, M., and Requet, A. 2007. JACK: A tool for validation of security and behaviour of Java applications. In Formal Methods for Components and Objects: Revised Lectures from the 5th International Symposium (FMCO'06). Lecture Notes in Computer Science, vol. 4709, Springer-Verlag, 152--174."},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.1007\/11823230_20"},{"doi-asserted-by":"publisher","key":"e_1_2_1_7_1","DOI":"10.1007\/978-3-540-71070-7_7"},{"key":"e_1_2_1_8_1","volume-title":"European Symposium on Programming. Lecture Notes in Computer Science","volume":"4960","author":"Barthe G.","unstructured":"]] Barthe , G. and Kunz , C . 2008. Certificate translation in abstract interpretation . In European Symposium on Programming. Lecture Notes in Computer Science , vol. 4960 . Springer-Verlag, 368--382. ]]Barthe, G. and Kunz, C. 2008. Certificate translation in abstract interpretation. In European Symposium on Programming. Lecture Notes in Computer Science, vol. 4960. Springer-Verlag, 368--382."},{"doi-asserted-by":"publisher","key":"e_1_2_1_9_1","DOI":"10.1109\/SP.2006.13"},{"doi-asserted-by":"publisher","key":"e_1_2_1_10_1","DOI":"10.1007\/11679219_9"},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.1007\/11617990_5"},{"doi-asserted-by":"publisher","key":"e_1_2_1_12_1","DOI":"10.1007\/11813040_31"},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of the Workshop on Formal Methods for Industrial Critical Systems. Electronic Notes in Theoretical Computer Science","volume":"80","author":"Burdy L.","unstructured":"]] Burdy , L. , Cheon , Y. , Cok , D. , Ernst , M. , Kiniry , J. , Leavens , G. , Leino , K. , and Poll , E . 2003. An overview of JML tools and applications . In Proceedings of the Workshop on Formal Methods for Industrial Critical Systems. Electronic Notes in Theoretical Computer Science , vol. 80 . Elsevier, 73--89. ]]Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G., Leino, K., and Poll, E. 2003. An overview of JML tools and applications. In Proceedings of the Workshop on Formal Methods for Industrial Critical Systems. Electronic Notes in Theoretical Computer Science, vol. 80. Elsevier, 73--89."},{"doi-asserted-by":"publisher","key":"e_1_2_1_14_1","DOI":"10.1145\/1141277.1141708"},{"doi-asserted-by":"publisher","key":"e_1_2_1_15_1","DOI":"10.1007\/11804192_16"},{"doi-asserted-by":"publisher","key":"e_1_2_1_16_1","DOI":"10.1007\/BF01128406"},{"doi-asserted-by":"publisher","key":"e_1_2_1_17_1","DOI":"10.1016\/j.tcs.2006.08.013"},{"volume-title":"Proceedings of the Ershov Memorial Conference","author":"Leino K. R. M.","unstructured":"]] Leino , K. R. M. 2006. Specifying and verifying programs in spec&num; . In Proceedings of the Ershov Memorial Conference , I. Virbitskaite and A. Voronkov, Eds. Lecture Notes in Computer Science, vol. 4378 . Springer , 20. ]]Leino, K. R. M. 2006. Specifying and verifying programs in spec&num;. In Proceedings of the Ershov Memorial Conference, I. Virbitskaite and A. Voronkov, Eds. Lecture Notes in Computer Science, vol. 4378. Springer, 20.","key":"e_1_2_1_18_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_19_1","DOI":"10.5555\/1030033.1030055"},{"doi-asserted-by":"publisher","key":"e_1_2_1_20_1","DOI":"10.1145\/1040305.1040335"},{"doi-asserted-by":"publisher","key":"e_1_2_1_21_1","DOI":"10.1007\/11693024_5"},{"doi-asserted-by":"publisher","key":"e_1_2_1_22_1","DOI":"10.1145\/1111037.1111042"},{"doi-asserted-by":"publisher","key":"e_1_2_1_23_1","DOI":"10.1145\/1292316.1292321"},{"doi-asserted-by":"publisher","key":"e_1_2_1_25_1","DOI":"10.1145\/263699.263712"},{"doi-asserted-by":"publisher","key":"e_1_2_1_26_1","DOI":"10.1145\/358438.349314"},{"doi-asserted-by":"publisher","key":"e_1_2_1_27_1","DOI":"10.1145\/277650.277752"},{"doi-asserted-by":"crossref","unstructured":"]]Nordio M. M\u00fcller P. and Meyer B. 2008a. Formalizing proof-transforming compilation of eiffel programs. Tech. rep. 587 ETH Zurich.  ]]Nordio M. M\u00fcller P. and Meyer B. 2008a. Formalizing proof-transforming compilation of eiffel programs. Tech. rep. 587 ETH Zurich.","key":"e_1_2_1_28_1","DOI":"10.1007\/978-3-540-69824-1_18"},{"doi-asserted-by":"crossref","unstructured":"]]Nordio M. M\u00fcller P. and Meyer B. 2008b. Proof-transforming compilation of eiffel programs. In TOOLS-EUROPE R. Paige Ed. Lecture Notes in Business and Information Processing. Springer-Verlag.  ]]Nordio M. M\u00fcller P. and Meyer B. 2008b. Proof-transforming compilation of eiffel programs. In TOOLS-EUROPE R. Paige Ed. Lecture Notes in Business and Information Processing. Springer-Verlag.","key":"e_1_2_1_29_1","DOI":"10.1007\/978-3-540-69824-1_18"},{"key":"e_1_2_1_30_1","volume-title":"Ed. Lecture Notes in Computer Science","volume":"1384","author":"Pnueli A.","unstructured":"]] Pnueli , A. , Singerman , E. , and Siegel , M . 1998. Translation validation. In Tools and Algorithms for the Construction and Analysis of Systems, B. Steffen , Ed. Lecture Notes in Computer Science , vol. 1384 . Springer-Verlag, 151--166. ]]Pnueli, A., Singerman, E., and Siegel, M. 1998. Translation validation. In Tools and Algorithms for the Construction and Analysis of Systems, B. Steffen, Ed. Lecture Notes in Computer Science, vol. 1384. Springer-Verlag, 151--166."},{"doi-asserted-by":"publisher","key":"e_1_2_1_31_1","DOI":"10.1145\/964001.964002"},{"doi-asserted-by":"publisher","key":"e_1_2_1_32_1","DOI":"10.1016\/j.jlap.2008.05.007"},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the Asian Programming Languages and Systems Symposium, A. Ohori, Ed. Lecture Notes in Computer Science","volume":"2895","author":"Seo S.","unstructured":"]] Seo , S. , Yang , H. , and Yi , K . 2003. Automatic construction of Hoare proofs from abstract interpretation results . In Proceedings of the Asian Programming Languages and Systems Symposium, A. Ohori, Ed. Lecture Notes in Computer Science , vol. 2895 . Springer-Verlag, 230--245. ]]Seo, S., Yang, H., and Yi, K. 2003. Automatic construction of Hoare proofs from abstract interpretation results. In Proceedings of the Asian Programming Languages and Systems Symposium, A. Ohori, Ed. Lecture Notes in Computer Science, vol. 2895. Springer-Verlag, 230--245."},{"doi-asserted-by":"publisher","key":"e_1_2_1_34_1","DOI":"10.1145\/1053468.1053469"},{"volume-title":"Proceedings of the Conference on Automated Deduction","author":"Strecker M.","unstructured":"]] Strecker , M. 2002. Formal Verification of a Java Compiler in Isabelle . In Proceedings of the Conference on Automated Deduction , A. Voronkov, Ed. Lecture Notes in Computer Science, vol. 2392 . Springer-Verlag , 63--77. ]]Strecker, M. 2002. Formal Verification of a Java Compiler in Isabelle. In Proceedings of the Conference on Automated Deduction, A. Voronkov, Ed. Lecture Notes in Computer Science, vol. 2392. Springer-Verlag, 63--77.","key":"e_1_2_1_35_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_36_1","DOI":"10.1145\/231379.231414"},{"doi-asserted-by":"publisher","key":"e_1_2_1_37_1","DOI":"10.1145\/1328897.1328444"},{"doi-asserted-by":"publisher","key":"e_1_2_1_38_1","DOI":"10.1016\/j.entcs.2005.02.040"},{"doi-asserted-by":"publisher","key":"e_1_2_1_39_1","DOI":"10.1016\/S1571-0661(04)80393-1"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1538917.1538919","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1538917.1538919","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:26:54Z","timestamp":1750278414000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1538917.1538919"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,6]]},"references-count":38,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2009,6]]}},"alternative-id":["10.1145\/1538917.1538919"],"URL":"https:\/\/doi.org\/10.1145\/1538917.1538919","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2009,6]]},"assertion":[{"value":"2007-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-07-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}