{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T21:18:42Z","timestamp":1768339122877,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540326281","type":"print"},{"value":"9783540326298","type":"electronic"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11679219_9","type":"book-chapter","created":{"date-parts":[[2006,2,23]],"date-time":"2006-02-23T02:36:41Z","timestamp":1140662201000},"page":"112-126","source":"Crossref","is-referenced-by-count":20,"title":["Proof Obligations Preserving Compilation"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tamara","family":"Rezk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ando","family":"Saabas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-30569-9_1","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"D. Aspinall","year":"2005","unstructured":"Aspinall, D., Gilmore, S., Hofmann, M., Sannella, D., Stark, I.: Mobile Resource Guarantees for Smart Devices. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 1\u201327. Springer, Heidelberg (2005)"},{"key":"9_CR2","volume-title":"Proceedings of Bytecode 2005, Electronic Notes in Theoretical Computer Science","author":"F. Bannwart","year":"2005","unstructured":"Bannwart, F., M\u2219uller, P.: A program logic for bytecode. In: Spoto, F. (ed.) Proceedings of Bytecode 2005, Electronic Notes in Theoretical Computer Science, Elsevier Publishing, Amsterdam (2005)"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","first-page":"50","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 50\u201371. Springer, Heidelberg (2005)"},{"key":"9_CR4","unstructured":"Benton, N.: A typed logic for stacks and jumps. Manuscript (2004)"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Burdy, L., Pavlova, M.: Java bytecode specification and verification. In: Proceedings of SAC 2006 (2006)(to appear)","DOI":"10.1145\/1141277.1141708"},{"key":"9_CR6","first-page":"100","volume-title":"Proceedings of CSFW 2004","author":"P. D\u2019Argenio","year":"2004","unstructured":"D\u2019Argenio, P., Barthe, G., Rezk, T.: Secure information flow by self-composition. In: Foccardi, R. (ed.) Proceedings of CSFW 2004, pp. 100\u2013114. IEEE Press, Los Alamitos (2004)"},{"key":"9_CR7","unstructured":"Joshua, D.G., Mitchell, W.: Special issue on VLISP. Lisp and Symbolic Computation\u00a08(1\/2) (March 1995)"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-540-30142-4_10","volume-title":"Theorem Proving in Higher Order Logics","author":"N.A. Hamid","year":"2004","unstructured":"Hamid, N.A., Shao, Z.: Interfacing hoare logic and type systems for foundational proof-carrying code. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 118\u2013135. Springer, Heidelberg (2004)"},{"key":"9_CR9","first-page":"106","volume-title":"Proceedings of POPL 1997","author":"G.C. Necula","year":"1997","unstructured":"Necula, G.C.: Proof-Carrying Code. In: Proceedings of POPL 1997, pp. 106\u2013119. ACM Press, New York (1997)"},{"key":"9_CR10","doi-asserted-by":"crossref","unstructured":"Necula, G.C., Lee, P.: The Design and Implementation of a Certifying Compiler. In: Proceedings of PLDI 1998, pp. 333\u2013344 (1998)","DOI":"10.1145\/277650.277752"},{"key":"9_CR11","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., Singerman, E., Siegel, M.: Translation validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 151\u2013166. Springer, Heidelberg (1998)"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/10930755_3","volume-title":"Theorem Proving in Higher Order Logics","author":"C.L. Quigley","year":"2003","unstructured":"Quigley, C.L.: A Programming Logic for Java Bytecode Programs. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 41\u201354. Springer, Heidelberg (2003)"},{"key":"9_CR13","unstructured":"Rinard, M.: Credible compilation. Manuscript (1999)"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/3-540-36384-X_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"X. Rival","year":"2002","unstructured":"Rival, X.: Abstract Interpretation-Based Certification of Assembly Code. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 41\u201355. Springer, Heidelberg (2002)"},{"key":"9_CR15","first-page":"1","volume-title":"Proceedings of POPL 2004","author":"X. Rival","year":"2004","unstructured":"Rival, X.: Symbolic Transfer Functions-based Approaches to Certified Compilation. In: Proceedings of POPL 2004, pp. 1\u201313. ACM Press, New York (2004)"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-540-31987-0_23","volume-title":"Programming Languages and Systems","author":"M. Wildmoser","year":"2005","unstructured":"Wildmoser, M., Nipkow, T.: Asserting bytecode safety. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 326\u2013341. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","Formal Aspects in Security and Trust"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11679219_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,12]],"date-time":"2019-03-12T05:28:34Z","timestamp":1552368514000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11679219_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540326281","9783540326298"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/11679219_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}