{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T13:05:00Z","timestamp":1725541500584},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642106712"},{"type":"electronic","value":"9783642106729"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-10672-9_20","type":"book-chapter","created":{"date-parts":[[2009,12,2]],"date-time":"2009-12-02T09:08:11Z","timestamp":1259744891000},"page":"275-293","source":"Crossref","is-referenced-by-count":1,"title":["Certify Once, Trust Anywhere: Modular Certification of Bytecode Programs for Certified Virtual Machine"],"prefix":"10.1007","author":[{"given":"Yuan","family":"Dong","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kai","family":"Ren","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shengyuan","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Suqin","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"20_CR1","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1109\/LICS.2001.932501","volume-title":"Proc. 16th IEEE Symposium on Logic in Computer Science","author":"A.W. Appel","year":"2001","unstructured":"Appel, A.W.: Foundational proof-carrying code. In: Proc. 16th IEEE Symposium on Logic in Computer Science, pp. 247\u2013258. IEEE Computer Society, Los Alamitos (2001)"},{"key":"20_CR2","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"255","volume-title":"Proceedings of Bytecode ?5","author":"F. Bannwart","year":"2005","unstructured":"Bannwart, F., M\u00fcller, P.: A program logic for bytecode. In: Proceedings of Bytecode?5. Electronic Notes in Theoretical Computer Science, pp. 255\u2013273. Elsevier, Amsterdam (2005)"},{"issue":"5","key":"20_CR3","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1538917.1538919","volume":"31","author":"G. Barthe","year":"2009","unstructured":"Barthe, G., Gr\u00e9goire, B., Kunz, C., Rezk, T.: Certificate translation for optimizing compilers. ACM Transactions on Programming Languages and Systems\u00a031(5), 18:1\u201318:45 (2009)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"20_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11575467_24","volume-title":"Programming Languages and Systems","author":"N. Benton","year":"2005","unstructured":"Benton, N.: A typed, compositional logic for a stack-based abstract machine. In: Yi, K. (ed.) APLAS 2005. LNCS, vol.\u00a03780, pp. 364\u2013380. Springer, Heidelberg (2005)"},{"key":"20_CR5","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1145\/1375581.1375604","volume-title":"Prog. Lang. Design and Impl. (PLDI 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: Prog. Lang. Design and Impl (PLDI 2008), pp. 183\u2013192. ACM, New York (2008)"},{"key":"20_CR6","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1145\/1250734.1250742","volume-title":"Prog. Lang. Design and Impl. (PLDI 2007)","author":"A. Chlipala","year":"2007","unstructured":"Chlipala, A.: A certified type-preserving compiler from lambda calculus to assembly language. In: Prog. Lang. Design and Impl (PLDI 2007), pp. 54\u201365. ACM, New York (2007)"},{"key":"20_CR7","unstructured":"Coq Development Team. The Coq proof assistant reference manual. Version 8.2 (2008)"},{"key":"20_CR8","unstructured":"ECMA. Standard ECMA-335 Common Language Infrastructure (2006)"},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"Feng, X., Ni, Z., Shao, Z., Guo, Y.: An open framework for foundational proof-carrying code. In: Proc. 2007 Workshop on Types in Lang. Design and Impl., pp. 67\u201378 (2007)","DOI":"10.1145\/1190315.1190325"},{"key":"20_CR10","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1145\/1133981.1134028","volume-title":"Prog. Lang. Design and Impl. (PLDI 2006)","author":"X. Feng","year":"2006","unstructured":"Feng, X., Shao, Z., Vaynberg, A., Xiang, S., Ni, Z.: Modular verification of assembly code with stack-based control abstractions. In: Prog. Lang. Design and Impl (PLDI 2006), pp. 401\u2013414. ACM Press, New York (2006)"},{"issue":"1","key":"20_CR11","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1145\/357980.358001","volume":"26","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM\u00a026(1), 53\u201356 (1969)","journal-title":"Communications of the ACM"},{"key":"20_CR12","unstructured":"Lawton, K., Denney, B., Guarneri, N.D., Ruppert, V., Bothamy, C.: Bochs user manual (2008), \n                    \n                      http:\/\/bochs.sourceforge.net\/"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/3-540-36579-6_8","volume-title":"Compiler Construction","author":"C. League","year":"2003","unstructured":"League, C., Shao, Z., Trifonov, V.: Precision in practice: A type-preserving java compiler. In: Hedin, G. (ed.) CC 2003. LNCS, vol.\u00a02622, pp. 106\u2013120. Springer, Heidelberg (2003)"},{"key":"20_CR14","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1109\/SEFM.2005.51","volume-title":"SEFM 2005: Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods","author":"D. Leinenbach","year":"2005","unstructured":"Leinenbach, D., Paul, W., Petrova, E.: Towards the formal verification of a c0 compiler: Code generation and implementation correctnes. In: SEFM 2005: Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods, Washington, DC, USA, pp. 2\u201312. IEEE Computer Society, Los Alamitos (2005)"},{"key":"20_CR15","unstructured":"Leroy, X.: A formally verified compiler back-end. Draft (2008), \n                    \n                      http:\/\/pauillac.inria.fr\/~leroy\/publi\/compcert-backend.pdf"},{"key":"20_CR16","unstructured":"Lindholm, T., Yellin, F.: The java virtual machine specification, 2nd edn. (1999)"},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"Ni, Z., Shao, Z.: Certified assembly programming with embedded code pointers. In: POPL 2006, pp. 320\u2013333 (2006)","DOI":"10.1145\/1111037.1111066"},{"key":"20_CR18","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/10930755_3","volume-title":"Proc. of 16th Int. Conf. on Theorem Proving in Higher-Order Logics","author":"C.L. Quigley","year":"2003","unstructured":"Quigley, C.L.: A programming logic for java bytecode programs. In: Proc. of 16th Int. Conf. on Theorem Proving in Higher-Order Logics, pp. 41\u201354. Springer, Heidelberg (2003)"},{"key":"20_CR19","unstructured":"Saabas, A., Uustalu, T.: Compositional type systems for stack-based low-level languages. In: Proc. of 12th Computing, Australasian Theory Symp., Australian, pp. 27\u201339 (2006)"},{"key":"20_CR20","unstructured":"Sun Microsystem. Top25 bugs (2009), \n                    \n                      http:\/\/bugs.sun.com\/bugdatabase\/top25_bugs.do\/"},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/11609773_6","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"G. Tan","year":"2006","unstructured":"Tan, G., Appel, A.W.: A compositional logic for control flow. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 80\u201394. Springer, Heidelberg (2006)"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"Vanderwaart, J.C., Crary, K.: A typed interface for garbage collection. In: Types in Lang. Design and Impl (TLDI 2003), pp. 109\u2013122 (2003)","DOI":"10.1145\/604174.604189"},{"key":"20_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/BFb0057785","volume-title":"Languages, Compilers, and Tools for Embedded Systems","author":"M. Weiss","year":"1998","unstructured":"Weiss, M., de Ferrire, F., Delsart, B., Fabre, C., Hirsch, F., Johnson, E.A., Joloboff, V., Roy, F., Siebert, F., Spengler, X.: Turboj, a java bytecode-to-native compiler. In: M\u00fcller, F., Bestavros, A. (eds.) LCTES 1998. LNCS, vol.\u00a01474, pp. 119\u2013130. Springer, Heidelberg (1998)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-10672-9_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T11:37:57Z","timestamp":1619782677000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-10672-9_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642106712","9783642106729"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-10672-9_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}