{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T07:33:52Z","timestamp":1725521632303},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540921875"},{"type":"electronic","value":"9783540921882"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"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":[[2008]]},"DOI":"10.1007\/978-3-540-92188-2_1","type":"book-chapter","created":{"date-parts":[[2008,12,3]],"date-time":"2008-12-03T04:00:21Z","timestamp":1228276821000},"page":"1-24","source":"Crossref","is-referenced-by-count":17,"title":["The MOBIUS Proof Carrying Code Infrastructure"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[]},{"given":"Pierre","family":"Cr\u00e9gut","sequence":"additional","affiliation":[]},{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Jensen","sequence":"additional","affiliation":[]},{"given":"David","family":"Pichardie","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/978-3-540-32275-7_25","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"E. Albert","year":"2005","unstructured":"Albert, E., Puebla, G., Hermenegildo, M.V.: Abstraction-carrying code. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS, vol.\u00a03452, pp. 380\u2013397. Springer, Heidelberg (2005)"},{"key":"1_CR2","first-page":"247","volume-title":"Logic in Computer Science","author":"A.W. Appel","year":"2001","unstructured":"Appel, A.W.: Foundational proof-carrying code. In: Halpern, J. (ed.) Logic in Computer Science, p. 247. IEEE Press, Los Alamitos (2001)"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1007\/978-3-540-75336-0_2","volume-title":"Trustworthy Global Computing","author":"G. Barthe","year":"2007","unstructured":"Barthe, G., Beringer, L., Cr\u00e9gut, P., Gr\u00e9goire, B., Hofmann, M., M\u00fcller, P., Poll, E., Puebla, G., Stark, I., V\u00e9tillard, E.: MOBIUS: Mobility, ubiquity, security. In: Montanari, U., Sannella, D., Bruni, R. (eds.) TGC 2006. LNCS, vol.\u00a04661, pp. 10\u201329. Springer, Heidelberg (2007)"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-540-71070-7_7","volume-title":"Automated Reasoning","author":"G. Barthe","year":"2008","unstructured":"Barthe, G., Gr\u00e9goire, B., Pavlova, M.: Preservation of proof obligations from java to the java virtual machine. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS, vol.\u00a05195, pp. 83\u201399. Springer, Heidelberg (2008) (to appear, 2008)"},{"key":"1_CR5","volume-title":"Emerging Applications of Abstract Interpretation","author":"F. Besson","year":"2006","unstructured":"Besson, F., Jensen, T., Pichardie, D.: A PCC architecture based on certified abstract interpretation. In: Emerging Applications of Abstract Interpretation. Elsevier, Amsterdam (2006)"},{"issue":"3","key":"1_CR6","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/j.tcs.2006.08.012","volume":"364","author":"F. Besson","year":"2006","unstructured":"Besson, F., Jensen, T., Pichardie, D.: Proof-Carrying Code from Certified Abstract Interpretation and Fixpoint Compression. Theoretical Computer Science\u00a0364(3), 273\u2013291 (2006); Extended version of [BessonP06]","journal-title":"Theoretical Computer Science"},{"key":"1_CR7","unstructured":"Besson, F., Jensen, T., Pichardie, D., Turpin, T.: Result certification for relational program analysis. Research Report 6333, IRISA (September 2007)"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-540-71316-6_10","volume-title":"Programming Languages and Systems","author":"G. Barthe","year":"2007","unstructured":"Barthe, G., Pichardie, D., Rezk, T.: A certified lightweight non-interference java bytecode verifier. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 125\u2013140. Springer, Heidelberg (2007)"},{"key":"1_CR9","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Bytecode Semantics, Verification, Analysis and Transformation","author":"P. Cr\u00e9gut","year":"2005","unstructured":"Cr\u00e9gut, P., Alvarado, C.: Improving the security of downloadable Java applications with static analysis. In: Bytecode Semantics, Verification, Analysis and Transformation. Electronic Notes in Theoretical Computer Science, vol.\u00a0141. Elsevier, Amsterdam (2005)"},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Principles of Programming Languages, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"1_CR11","unstructured":"Chlipala, A.: Modular development of certified program verifiers with a proof assistant. Journal of Functional Programming (to appear)"},{"key":"1_CR12","unstructured":"Coq development team. The Coq proof assistant reference manual V8.0. Technical Report 255, INRIA, France (March 2004), \n                    \n                      http:\/\/coq.inria.fr\/doc\/main.html"},{"key":"1_CR13","unstructured":"Gowdiak, A.: Java 2 Micro Edition (J2ME) security vulnerabilities. In: Hack In The Box Conference, Kuala Lumpur, Malaysia (2004)"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-540-78663-4_4","volume-title":"Trustworthy Global Computing","author":"B. Gr\u00e9goire","year":"2008","unstructured":"Gr\u00e9goire, B., Sacchini, J.: Combining a verification condition generator for a bytecode language with static analyses. In: Barthe, G., Fournet, C. (eds.) TGC 2007 and FODO 2008. LNCS, vol.\u00a04912, pp. 23\u201340. Springer, Heidelberg (2008)"},{"key":"1_CR15","first-page":"194","volume-title":"Principles of Programming Languages","author":"G.A. Kildall","year":"1973","unstructured":"Kildall, G.A.: A unified approach to global program optimization. In: Principles of Programming Languages, pp. 194\u2013206. ACM Press, New York (1973)"},{"issue":"3-4","key":"1_CR16","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1023\/A:1025055424017","volume":"30","author":"X. Leroy","year":"2003","unstructured":"Leroy, X.: Java bytecode verification: algorithms and formalizations. Journal of Automated Reasoning\u00a030(3-4), 235\u2013269 (2003)","journal-title":"Journal of Automated Reasoning"},{"key":"1_CR17","unstructured":"Livshits, V., Lam, M.: Finding security vulnerabilities in java applications with static analysis. In: USENIX Security Symposium (2005)"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Liskov, B., Wing, J.M.: A behavioral notion of subtyping. ACM Transactions on Programming Languages and Systems\u00a016(6) (1994)","DOI":"10.1145\/197320.197383"},{"key":"1_CR19","unstructured":"Lindholm, T., Yellin, F.: The JavaTM Virtual Machine Specification, 2nd edn. Sun Microsystems, Inc. (1999), \n                    \n                      http:\/\/java.sun.com\/docs\/books\/vmspec\/"},{"key":"1_CR20","first-page":"39","volume-title":"SAVCBS 2007: Proceedings of the 2007 conference on Specification and verification of component-based systems","author":"P. M\u00fcller","year":"2007","unstructured":"M\u00fcller, P., Nordio, M.: Proof-transforming compilation of programs with abrupt termination. In: SAVCBS 2007: Proceedings of the 2007 conference on Specification and verification of component-based systems, pp. 39\u201346. ACM, New York (2007)"},{"key":"1_CR21","first-page":"106","volume-title":"Principles of Programming Languages","author":"G.C. Necula","year":"1997","unstructured":"Necula, G.C.: Proof-carrying code. In: Principles of Programming Languages, pp. 106\u2013119. ACM Press, New York (1997)"},{"key":"1_CR22","first-page":"333","volume-title":"Programming Languages Design and Implementation","author":"G.C. Necula","year":"1998","unstructured":"Necula, G.C., Lee, P.: The design and implementation of a certifying compiler. In: Programming Languages Design and Implementation, vol.\u00a033, pp. 333\u2013344. ACM Press, New York (1998)"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Poetzsch-Heffter, A., M\u00fcller, P.: Logical foundations for typed object-oriented languages. In: Gries, D., De Roever, W. (eds.) Programming Concepts and Methods (PROCOMET), pp. 404\u2013423 (1998)","DOI":"10.1007\/978-0-387-35358-6_26"},{"issue":"3-4","key":"1_CR24","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1023\/B:JARS.0000021015.15794.82","volume":"31","author":"E. Rose","year":"2003","unstructured":"Rose, E.: Lightweight bytecode verification. Journal of Automated Reasoning\u00a031(3-4), 303\u2013334 (2003)","journal-title":"Journal of Automated Reasoning"},{"key":"1_CR25","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A. Sabelfeld","year":"2003","unstructured":"Sabelfeld, A., Myers, A.: Language-based information-flow security. IEEE Journal on Selected Areas in Communication\u00a021, 5\u201319 (2003)","journal-title":"IEEE Journal on Selected Areas in Communication"},{"key":"1_CR26","unstructured":"Sun Microsystems Inc., 4150 Network Circle, Santa Clara, California 95054. Connected Limited Device Configuration.Specification Version 1.1. JavaTM\u00a02 Platform, Micro Edition (J2METM) (March 2003)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Components and Objects"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-92188-2_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,4]],"date-time":"2019-03-04T03:18:52Z","timestamp":1551669532000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-92188-2_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540921875","9783540921882"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-92188-2_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}