{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,10]],"date-time":"2025-02-10T08:40:17Z","timestamp":1739176817357,"version":"3.37.0"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642026577"},{"type":"electronic","value":"9783642026584"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-02658-4_16","type":"book-chapter","created":{"date-parts":[[2009,6,22]],"date-time":"2009-06-22T11:00:16Z","timestamp":1245668416000},"page":"173-187","source":"Crossref","is-referenced-by-count":4,"title":["Automated Analysis of Java Methods for Confidentiality"],"prefix":"10.1007","author":[{"given":"Pavol","family":"\u010cern\u00fd","sequence":"first","affiliation":[]},{"given":"Rajeev","family":"Alur","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"16_CR1","unstructured":"JavaTM ME Developer\u2019s Library 2.0, http:\/\/www.forum.nokia.com"},{"key":"16_CR2","unstructured":"WALA - Watson libraries for analyses, http:\/\/wala.sourceforge.net"},{"key":"16_CR3","unstructured":"JSR 118 Expert Group. Mobile Information Device Profile for J2ME 2.1 (2007)"},{"key":"16_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"664","DOI":"10.1007\/978-3-540-71209-1_51","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Alur","year":"2007","unstructured":"Alur, R., \u010cern\u00fd, P., Chaudhuri, S.: Model checking on trees with path equivalences. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 664\u2013678. Springer, Heidelberg (2007)"},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/11787006_10","volume-title":"Automata, Languages and Programming","author":"R. Alur","year":"2006","unstructured":"Alur, R., \u010cern\u00fd, P., Zdancewic, S.: Preserving secrecy under refinement. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol.\u00a04052, pp. 107\u2013118. Springer, Heidelberg (2006)"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Amtoft, T., Banerjee, A.: Verification condition generation for conditional information flow. In: Proc. of FMSE 2007, pp. 2\u201311 (2007)","DOI":"10.1145\/1314436.1314438"},{"issue":"1","key":"16_CR7","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/565816.503274","volume":"37","author":"Thomas Ball","year":"2002","unstructured":"Ball, T., Rajamani, S.: The SLAM project: debugging system software via static analysis. In: Proc. POPL 2002, pp. 1\u20133 (2002)","journal-title":"ACM SIGPLAN Notices"},{"issue":"6","key":"16_CR8","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/s10207-008-0058-x","volume":"7","author":"J. Bryans","year":"2008","unstructured":"Bryans, J., Koutny, M., Mazar\u00e9, L., Ryan, P.: Opacity generalised to transition systems. Int. J. Inf. Sec.\u00a07(6), 421\u2013435 (2008)","journal-title":"Int. J. Inf. Sec."},{"key":"16_CR9","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: Proc. of POPL 1977, Los Angeles, California, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proc. of POPL 1978, pp. 84\u201397 (1978)","DOI":"10.1145\/512760.512770"},{"issue":"1","key":"16_CR11","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1145\/1111320.1111044","volume":"41","author":"Mads Dam","year":"2006","unstructured":"Dam, M.: Decidability and proof systems for language-based noninterference relations. In: POPL 2006, pp. 67\u201378 (2006)","journal-title":"ACM SIGPLAN Notices"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Dam, M., Giambiagi, P.: Confidentiality for mobile code: The case of a simple payment protocol. In: Proc. of CSFW 2000, pp. 233\u2013244 (2000)","DOI":"10.1109\/CSFW.2000.856940"},{"issue":"2","key":"16_CR13","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1145\/244795.244800","volume":"19","author":"D. Dams","year":"1997","unstructured":"Dams, D., Gerth, R., Grumberg, O.: Abstract interpretation of reactive systems. ACM Trans. Program. Lang. Syst.\u00a019(2), 253\u2013291 (1997)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"key":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/3-540-44685-0_29","volume-title":"CONCUR 2001 - Concurrency Theory","author":"P. Godefroid","year":"2001","unstructured":"Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based model checking using modal transition systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol.\u00a02154, pp. 426\u2013440. Springer, Heidelberg (2001)"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Gray, J.: Probabilistic interference. In: Proc. of SP 1990, pp. 170\u2013179 (1990)","DOI":"10.1109\/RISP.1990.63848"},{"key":"16_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/11691372_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B. Gulavani","year":"2006","unstructured":"Gulavani, B., Rajamani, S.: Counterexample driven refinement for abstract interpretation. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 474\u2013488. Springer, Heidelberg (2006)"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Halpern, J., O\u2019Neill, K.: Secrecy in multiagent systems. In: Proc. of CSFW 2002, pp. 32\u201346 (2002)","DOI":"10.1109\/CSFW.2002.1021805"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Hammer, C., Krinke, J., Nodes, F.: Intransitive noninterference in dependence graphs. In: Proc. of ISoLA 2006, pp. 136\u2013145 (2006)","DOI":"10.1109\/ISoLA.2006.39"},{"key":"16_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"526","DOI":"10.1007\/3-540-45657-0_45","volume-title":"Computer Aided Verification","author":"T. Henzinger","year":"2002","unstructured":"Henzinger, T., Jhala, R., Majumdar, R., Necula, G., Sutre, G., Weimer, W.: Temporal-safety proofs for systems code. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 526\u2013538. Springer, Heidelberg (2002)"},{"key":"16_CR21","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A. Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. Higher-Order and Symbolic Computation\u00a019, 31\u2013100 (2006)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"16_CR22","doi-asserted-by":"crossref","unstructured":"Myers, A.: JFlow: Practical mostly-static information flow control. In: Proc. of POPL 1999, pp. 228\u2013241 (1999)","DOI":"10.1145\/292540.292561"},{"key":"16_CR23","unstructured":"O\u2019Connor, J.: Attack surface analysis of Blackberry devices. White Paper: Symantec security response (2007)"},{"key":"16_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/978-3-540-77505-8_26","volume-title":"Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues","author":"C. Popeea","year":"2006","unstructured":"Popeea, C., Chin, W.: Inferring disjunctive postconditions. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol.\u00a04435, pp. 331\u2013345. Springer, Heidelberg (2006)"},{"issue":"1","key":"16_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 Communications\u00a021(1), 5\u201319 (2003)","journal-title":"IEEE Journal on Selected Areas in Communications"},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"Sabelfeld, A., Sands, D.: Dimensions and principles of declassification. In: CSFW 2005, pp. 255\u2013269 (2005)","DOI":"10.1109\/CSFW.2005.15"},{"key":"16_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/11823230_2","volume-title":"Static Analysis","author":"S. Sankaranarayanan","year":"2006","unstructured":"Sankaranarayanan, S., Ivancic, F., Shlyakhter, I., Gupta, A.: Static analysis in disjunctive numerical domains. In: Yi, K. (ed.) SAS 2006. LNCS, vol.\u00a04134, pp. 3\u201317. Springer, Heidelberg (2006)"},{"key":"16_CR28","doi-asserted-by":"crossref","unstructured":"Schneider, F. (ed.): Trust in Cyberspace. National Academy Press (1999)","DOI":"10.1016\/S1353-4858(00)80006-9"},{"issue":"4","key":"16_CR29","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1145\/1178625.1178628","volume":"15","author":"G. Snelting","year":"2006","unstructured":"Snelting, G., Robschink, T., Krinke, J.: Efficient path conditions in dependence graphs for software safety analysis. ACM Trans. Softw. Eng. Methodol.\u00a015(4), 410\u2013457 (2006)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"16_CR30","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.entcs.2006.11.002","volume":"168","author":"R. Meyden van der","year":"2007","unstructured":"van der Meyden, R., Zhang, C.: Algorithmic verification of noninterference properties. Electr. Notes Theor. Comput. Sci.\u00a0168, 61\u201375 (2007)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"16_CR31","doi-asserted-by":"crossref","unstructured":"Volpano, D., Smith, G.: Probabilistic noninterference in a concurrent language. Journal of Computer Security\u00a07(1) (1999)","DOI":"10.3233\/JCS-1999-72-305"},{"key":"16_CR32","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The formal semantics of programming languages: An Introduction","author":"G. Winskel","year":"1993","unstructured":"Winskel, G.: The formal semantics of programming languages: An Introduction. MIT Press, Cambridge (1993)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02658-4_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,10]],"date-time":"2025-02-10T07:58:30Z","timestamp":1739174310000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02658-4_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642026577","9783642026584"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02658-4_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}