{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T07:33:48Z","timestamp":1725521628689},"publisher-location":"Berlin, Heidelberg","reference-count":34,"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_2","type":"book-chapter","created":{"date-parts":[[2008,12,3]],"date-time":"2008-12-03T04:00:21Z","timestamp":1228276821000},"page":"25-51","source":"Crossref","is-referenced-by-count":3,"title":["Certification Using the Mobius Base Logic"],"prefix":"10.1007","author":[{"given":"Lennart","family":"Beringer","sequence":"first","affiliation":[]},{"given":"Martin","family":"Hofmann","sequence":"additional","affiliation":[]},{"given":"Mariela","family":"Pavlova","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"2_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":"2_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 (invited talk, 2001)"},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-540-30142-4_3","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Aspinall","year":"2004","unstructured":"Aspinall, D., Beringer, L., Hofmann, M., Loidl, H.-W., Momigliano, A.: A program logic for resource verification. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 34\u201349. Springer, Heidelberg (2004)"},{"key":"2_CR4","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"255","volume-title":"Bytecode Semantics, Verification, Analysis and Transformation","author":"F.Y. Bannwart","year":"2005","unstructured":"Bannwart, F.Y., M\u00fcller, P.: A program logic for bytecode. In: Spoto, F. (ed.) Bytecode Semantics, Verification, Analysis and Transformation. Electronic Notes in Theoretical Computer Science, vol.\u00a0141, pp. 255\u2013273. Elsevier, Amsterdam (2005)"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"Trustworthy Global Computing, Third Symposium (TGC 2007)","year":"2008","unstructured":"Barthe, G., Fournet, C. (eds.): TGC 2007 and FODO 2008. LNCS, vol.\u00a04912. Springer, Heidelberg (2008)"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","volume-title":"Verification of Object-Oriented Software. The KeY Approach","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS, vol.\u00a04334. Springer, Heidelberg (2007)"},{"key":"2_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/3-540-36578-8_18","volume-title":"Fundamental Approaches to Software Engineering","author":"B. Beckert","year":"2003","unstructured":"Beckert, B., Mostowski, W.: A program logic for handling JAVA cARD\u2019s transaction mechanism. In: Pezz\u00e9, M. (ed.) FASE 2003. LNCS, vol.\u00a02621, pp. 246\u2013260. Springer, Heidelberg (2003)"},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/11924661_24","volume-title":"Programming Languages and Systems","author":"L. Beringer","year":"2006","unstructured":"Beringer, L., Hofmann, M.O.: A bytecode logic for JML and types. In: Kobayashi, N. (ed.) APLAS 2006. LNCS, vol.\u00a04279, pp. 389\u2013405. Springer, Heidelberg (2006)"},{"key":"2_CR9","volume-title":"IEEE Computer Security Foundations Workshop","author":"L. Beringer","year":"2007","unstructured":"Beringer, L., Hofmann, M.: Secure information flow and program logics. In: IEEE Computer Security Foundations Workshop. IEEE Press, Los Alamitos (2007)"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/978-3-540-32275-7_23","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"L. Beringer","year":"2005","unstructured":"Beringer, L., Hofmann, M., Momigliano, A., Shkaravska, O.: Automatic certification of heap consumption. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS, vol.\u00a03452, pp. 347\u2013362. Springer, Heidelberg (2005)"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Besson, F., Jensen, T., Pichardie, D.: Proof-Carrying Code from Certified Abstract Interpretation and Fixpoint Compression.Theoretical Computer Science (2006)","DOI":"10.1016\/j.tcs.2006.08.012"},{"key":"2_CR12","unstructured":"Besson, F., Jensen, T., Pichardie, D., Turpin, T.: Result certification for relational program analysis. Inria Research Report 6333 (2007)"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/11526841_8","volume-title":"FM 2005: Formal Methods","author":"D. Cachera","year":"2005","unstructured":"Cachera, D., Jensen, T.P., Pichardie, D., Schneider, G.: Certified memory usage analysis. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol.\u00a03582, pp. 91\u2013106. Springer, Heidelberg (2005)"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/11609773_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B.-Y.E. Chang","year":"2005","unstructured":"Chang, B., Chlipala, A., Necula, G.: A framework for certified program analysis and its applications to mobile-code safety. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 174\u2013189. Springer, Heidelberg (2005)"},{"key":"2_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1040294.1040295","volume-title":"Proceedings of TLDI 2005: 2005 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation","author":"B. Chang","year":"2005","unstructured":"Chang, B., Chlipala, A., Necula, G., Schneck, R.: The open verifier framework for foundational verifiers. In: Morrisett, J., F\u00e4hndrich, M. (eds.) Proceedings of TLDI 2005: 2005 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, pp. 1\u201312. ACM Press, New York (2005)"},{"key":"2_CR16","unstructured":"MOBIUS Consortium. Deliverable\u00a01.1: Resource and information flow security requirements (2006), http:\/\/mobius.inria.fr"},{"key":"2_CR17","unstructured":"MOBIUS Consortium. Deliverable 3.1: Bytecode specification language and program logic (2006), http:\/\/mobius.inria.fr"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Automatic synthesis of optimal invariant assertions: mathematical foundations. In: ACM Symposium on Artificial Intelligence & Programming Languages, Rochester, NY; ACM SIGPLAN Not 12(8), 1\u201312 (1977)","DOI":"10.1145\/800228.806926"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Conference Record of the Fifth ACM Symposium on Principles of Programming Languages, pp. 84\u201397 (1978)","DOI":"10.1145\/512760.512770"},{"key":"2_CR20","doi-asserted-by":"crossref","unstructured":"Czarnik, P., Schubert, A.: Extending operational semantics of the java bytecode. In: Barthe, Fournet [5], pp. 57\u201372","DOI":"10.1007\/978-3-540-78663-4_6"},{"issue":"3","key":"2_CR21","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D. Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. Journal of the ACM\u00a052(3), 365\u2013473 (2005)","journal-title":"Journal of the ACM"},{"key":"2_CR22","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1145\/1190315.1190325","volume-title":"Proc. 2007 ACM SIGPLAN International Workshop on Types in Language Design and Implementation (TLDI 2007)","author":"X. Feng","year":"2007","unstructured":"Feng, X., Ni, Z., Shao, Z., Guo, Y.: An open framework for foundational proof-carrying code. In: Proc. 2007 ACM SIGPLAN International Workshop on Types in Language Design and Implementation (TLDI 2007), pp. 67\u201378. ACM Press, New York (2007)"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-540-75336-0_8","volume-title":"Trustworthy Global Computing","author":"R. H\u00e4hnle","year":"2007","unstructured":"H\u00e4hnle, R., Pan, J., R\u00fcmmer, P., Walter, D.: Integration of a security type system into a program logic. In: Montanari, U., Sannella, D., Bruni, R. (eds.) TGC 2006. LNCS, vol.\u00a04661, pp. 116\u2013131. Springer, Heidelberg (2007)"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Hofmann, M., Pavlova, M.: Elimination of ghost variables in program logics. In: Barthe, Fournet [5], pp. 1\u201320","DOI":"10.1007\/978-3-540-78663-4_1"},{"key":"2_CR25","unstructured":"Kleymann, T.: Hoare Logic and VDM: Machine-Checked Soundness and Completeness Proofs. PhD thesis, LFCS, University of Edinburgh (1998)"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"M\u00fcller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: Proc. ACM POPL 2004, pp. 330\u2013341 (2004)","DOI":"10.1145\/982962.964029"},{"key":"2_CR27","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":"2_CR28","unstructured":"Nelson, G.: Techniques for program verification. Technical Report CSL-81-10, Xerox PARC Computer Science Laboratory (June 1981)"},{"key":"2_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-45793-3_8","volume-title":"Computer Science Logic","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T.: Hoare logics for recursive procedures and unbounded nondeterminism. In: Bradfield, J. (ed.) CSL 2002 and EACSL 2002. LNCS, vol.\u00a02471, pp. 103\u2013119. Springer, Heidelberg (2002)"},{"key":"2_CR30","unstructured":"Pichardie, D.: Bicolano \u2013 Byte Code Language in Coq. Summary appears in [7] (2006), http:\/\/mobius.inia.fr\/bicolano"},{"key":"2_CR31","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.A., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 41\u201354. Springer, Heidelberg (2003)"},{"key":"2_CR32","unstructured":"Wildmoser, M.: Verified Proof Carrying Code. PhD thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen (2005)"},{"key":"2_CR33","first-page":"333","volume-title":"Theoretical Computer Science","author":"M. Wildmoser","year":"2004","unstructured":"Wildmoser, M., Nipkow, T., Klein, G., Nanz, S.: Prototyping proof carrying code. In: Levy, J.-J., Mayr, E.W., Mitchell, J.C. (eds.) Theoretical Computer Science, pp. 333\u2013347. Kluwer Academic Publishing, Dordrecht (2004)"},{"key":"2_CR34","doi-asserted-by":"crossref","unstructured":"Woo, T.Y., Lam, S.S.: A semantic model for authentication protocols. In: RSP: IEEE Computer Society Symposium on Research in Security and Privacy (1993)","DOI":"10.1109\/RISP.1993.287633"}],"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_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T19:12:23Z","timestamp":1557947543000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-92188-2_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540921875","9783540921882"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-92188-2_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}