{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:10:03Z","timestamp":1763467803057},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540713142"},{"type":"electronic","value":"9783540713166"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-71316-6_10","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T12:58:28Z","timestamp":1184590708000},"page":"125-140","source":"Crossref","is-referenced-by-count":31,"title":["A Certified Lightweight Non-interference Java Bytecode Verifier"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Pichardie","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tamara","family":"Rezk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"10_CR1","first-page":"243","volume-title":"Proceedings of POPL\u201900","author":"A.W. Appel","year":"2000","unstructured":"Appel, A.W., Felty, A.P.: A semantic model of types and machine instuctions for proof-carrying code. In: Proceedings of POPL\u201900, pp. 243\u2013253. ACM Press, New York (2000)"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1007\/11541868_4","volume-title":"Theorem Proving in Higher Order Logics","author":"B.E. Aydemir","year":"2005","unstructured":"Aydemir, B.E., et al.: Mechanized Metatheory for the Masses: The PoplMark Challenge. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 50\u201365. Springer, Heidelberg (2005)"},{"key":"10_CR3","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1017\/S0956796804005453","volume":"15","author":"A. Banerjee","year":"2005","unstructured":"Banerjee, A., Naumann, D.: Stack-based access control for secure information flow. Journal of Functional Programming\u00a015, 131\u2013177 (2005)","journal-title":"Journal of Functional Programming"},{"key":"10_CR4","volume-title":"Symposium on Security and Privacy, 2006","author":"G. Barthe","year":"2006","unstructured":"Barthe, G., Naumann, D., Rezk, T.: Deriving an Information Flow Checker and Certifying Compiler for Java. In: Symposium on Security and Privacy, 2006, IEEE Computer Society Press, Los Alamitos (2006)"},{"key":"10_CR5","unstructured":"Barthe, G., Pichardie, D., Rezk, T.: Non-interference for low level languages. Technical report, INRIA (2006), \n                    \n                      http:\/\/hal.inria.fr\/inria-00106182"},{"key":"10_CR6","first-page":"103","volume-title":"Proceedings of TLDI\u201905","author":"G. Barthe","year":"2005","unstructured":"Barthe, G., Rezk, T.: Non-interference for a JVM-like language. In: F\u00e4hndrich, M. (ed.) Proceedings of TLDI\u201905, pp. 103\u2013112. ACM Press, New York (2005)"},{"issue":"3","key":"10_CR7","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)","journal-title":"Theoretical Computer Science"},{"key":"10_CR8","doi-asserted-by":"crossref","first-page":"369","DOI":"10.3233\/JCS-2002-10404","volume":"10","author":"P. Bieber","year":"2002","unstructured":"Bieber, P., et al.: Checking Secure Interactions of Smart Card Applets: Extended version. Journal of Computer Security\u00a010, 369\u2013398 (2002)","journal-title":"Journal of Computer Security"},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/11741060_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"E. Bonelli","year":"2006","unstructured":"Bonelli, E., Compagnoni, A.B., Medel, R.: Information flow analysis for a typed assembly language with polymorphic stacks. In: Barthe, G., et al. (eds.) CASSIS 2005. LNCS, vol.\u00a03956, pp. 37\u201356. Springer, Heidelberg (2006)"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1007\/978-3-540-30579-8_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Genaim","year":"2005","unstructured":"Genaim, S., Spoto, F.: Information Flow Analysis for Java Bytecode. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 346\u2013362. Springer, Heidelberg (2005)"},{"key":"10_CR11","first-page":"186","volume-title":"Proceedings of POPL\u201904","author":"R. Giacobazzi","year":"2004","unstructured":"Giacobazzi, R., Mastroeni, I.: Abstract non-interference: Parameterizing non-interference by abstract interpretation. In: Proceedings of POPL\u201904, pp. 186\u2013197. ACM Press, New York (2004)"},{"key":"10_CR12","first-page":"255","volume-title":"Proceedings of CSFW\u201906","author":"D. Hedin","year":"2006","unstructured":"Hedin, D., Sands, D.: Noninterference in the presence of non-opaque pointers. In: Proceedings of CSFW\u201906, pp. 255\u2013269. IEEE Computer Society Press, Los Alamitos (2006)"},{"key":"10_CR13","first-page":"79","volume-title":"Proceedings of POPL\u201906","author":"S. Hunt","year":"2006","unstructured":"Hunt, S., Sands, D.: On Flow-Sensitive Security Types. In: Proceedings of POPL\u201906, pp. 79\u201390. ACM Press, New York (2006)"},{"issue":"4","key":"10_CR14","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1002\/spe.438","volume":"32","author":"X. Leroy","year":"2002","unstructured":"Leroy, X.: Bytecode verification on Java smart cards. Software\u2013practice and experience\u00a032(4), 319\u2013340 (2002)","journal-title":"Software\u2013practice and experience"},{"key":"10_CR15","first-page":"228","volume-title":"Proceedings of POPL\u201999","author":"A.C. Myers","year":"1999","unstructured":"Myers, A.C.: Jflow: Practical mostly-static information flow control. In: Proceedings of POPL\u201999, pp. 228\u2013241. ACM Press, New York (1999)"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1007\/11541868_14","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Naumann","year":"2005","unstructured":"Naumann, D.: Verifying a secure information flow analyzer. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 211\u2013226. Springer, Heidelberg (2005)"},{"key":"10_CR17","unstructured":"Rezk, T.: Verification of confidentiality policies for mobile code. PhD thesis, Universit\u00e9 de Nice Sophia-Antipolis (2006)"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Russo, A., Sabelfeld, A.: Securing interaction between threads and the scheduler. In: Proceedings of CSFW\u201906 (2006)","DOI":"10.1109\/CSFW.2006.29"},{"key":"10_CR19","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 Comunications\u00a021, 5\u201319 (2003)","journal-title":"IEEE Journal on Selected Areas in Comunications"},{"key":"10_CR20","volume-title":"Proceedings of CSFW\u201905","author":"A. Sabelfeld","year":"2005","unstructured":"Sabelfeld, A., Sands, D.: Dimensions and principles of declassification. In: Proceedings of CSFW\u201905, IEEE Computer Society Press, Los Alamitos (2005)"},{"key":"10_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1007\/BFb0030629","volume-title":"TAPSOFT\u201997: Theory and Practice of Software Development","author":"D. Volpano","year":"1997","unstructured":"Volpano, D., Smith, G.: A Type-Based Approach to Program Security. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol.\u00a01214, pp. 607\u2013621. Springer, Heidelberg (1997)"},{"key":"10_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/11693024_12","volume-title":"Programming Languages and Systems","author":"D. Yu","year":"2006","unstructured":"Yu, D., Islam, N.: A typed assembly language for confidentiality. In: Sestoft, P. (ed.) ESOP 2006 and ETAPS 2006. LNCS, vol.\u00a03924, pp. 162\u2013179. Springer, Heidelberg (2006)"},{"key":"10_CR23","unstructured":"Zanardini, D.: Certified Abstract Non-Interference: Object-Oriented Code Validation for Information Flow Security. PhD thesis, Universit\u00e0 di Verona (April 2006)"}],"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-540-71316-6_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,17]],"date-time":"2019-02-17T21:46:48Z","timestamp":1550440008000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71316-6_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540713142","9783540713166"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71316-6_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}