{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,11]],"date-time":"2026-11-11T07:11:38Z","timestamp":1794381098511,"version":"4.9.0"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540227915","type":"print"},{"value":"9783540278641","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27864-1_10","type":"book-chapter","created":{"date-parts":[[2010,9,16]],"date-time":"2010-09-16T12:35:37Z","timestamp":1284640537000},"page":"100-115","source":"Crossref","is-referenced-by-count":57,"title":["Information Flow Analysis in Logical Form"],"prefix":"10.1007","author":[{"given":"Torben","family":"Amtoft","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Anindya","family":"Banerjee","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Banerjee, A., Heintze, N., Riecke, J.G.: A core calculus of dependency. In: ACM Symposium on Principles of Programming Languages (POPL), pp. 147\u2013160 (1999)","DOI":"10.1145\/292540.292555"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Amtoft, T., Banerjee, A.: Information flow analysis in logical form. Technical Report CIS TR 2004-3, Kansas State University (April 2004)","DOI":"10.1007\/978-3-540-27864-1_10"},{"issue":"1","key":"10_CR3","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1145\/357084.357088","volume":"2","author":"G.R. Andrews","year":"1980","unstructured":"Andrews, G.R., Reitman, R.P.: An axiomatic approach to information flow in programs. ACM Transactions on Programming Languages and Systems\u00a02(1), 56\u201375 (1980)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10_CR4","first-page":"253","volume-title":"IEEE Computer Security Foundations Workshop (CSFW)","author":"A. Banerjee","year":"2002","unstructured":"Banerjee, A., Naumann, D.A.: Secure information flow and pointer confinement in a Java-like language. In: IEEE Computer Security Foundations Workshop (CSFW), pp. 253\u2013270. IEEE Computer Society Press, Los Alamitos (2002)"},{"key":"10_CR5","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: IEEE Computer Security Foundations Workshop, CSFW (2004) (to appear)"},{"issue":"1","key":"10_CR6","first-page":"3","volume":"28","author":"D. Clark","year":"2002","unstructured":"Clark, D., Hankin, C., Hunt, S.: Information flow for Algol-like languages. Computer Languages\u00a028(1), 3\u201328 (2002)","journal-title":"Computer Languages"},{"key":"10_CR7","first-page":"297","volume-title":"Foundations of Secure Computation","author":"E.S. Cohen","year":"1978","unstructured":"Cohen, E.S.: Information transmission in sequential programs. In: DeMillo, R.A., Dobkin, D.P., Jones, A.K., Lipton, R.J. (eds.) Foundations of Secure Computation, pp. 297\u2013335. Academic Press, London (1978)"},{"key":"10_CR8","first-page":"238","volume-title":"ACM Symposium on Principles of Programming Languages (POPL)","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: ACM Symposium on Principles of Programming Languages (POPL), pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"10_CR9","series-title":"SIGPLAN Notices","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/800228.806926","volume-title":"Proceedings of the ACM Symposium on Artificial Intelligence and Programming Languages","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Automatic synthesis of optimal invariant assertions: mathematical foundations. In: Proceedings of the ACM Symposium on Artificial Intelligence and Programming Languages, August 1977. SIGPLAN Notices, vol.\u00a012, pp. 1\u201312. ACM Press, New York (1977)"},{"key":"#cr-split#-10_CR10.1","unstructured":"Darvas, ??., H??hnle, R., Sands, D.: A theorem proving approach to analysis of secure information flow. Technical Report 2004-01, Department of Computing Science, Chalmers University of Technology and G??teborg University (2004);"},{"key":"#cr-split#-10_CR10.2","unstructured":"A fuller version of a paper appearing in Workshop on Issues in the Theory of Security (2003)"},{"issue":"7","key":"10_CR11","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1145\/359636.359712","volume":"20","author":"D. Denning","year":"1977","unstructured":"Denning, D., Denning, P.: Certification of programs for secure information flow. Communications of the ACM\u00a020(7), 504\u2013513 (1977)","journal-title":"Communications of the ACM"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Giacobazzi, R., Mastroeni, I.: Abstract non-interference: Parameterizing non-interference by abstract interpretation. In: ACM Symposium on Principles of Programming Languages (POPL), pp. 186\u2013197 (2004)","DOI":"10.1145\/964001.964017"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Goguen, J., Meseguer, J.: Security policies and security models. In: Proc. IEEE Symp. on Security and Privacy, pp. 11\u201320 (1982)","DOI":"10.1109\/SP.1982.10014"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Heintze, N., Riecke, J.G.: The SLam calculus: programming with secrecy and integrity. In: ACM Symposium on Principles of Programming Languages (POPL), pp. 365\u2013377 (1998)","DOI":"10.1145\/268946.268976"},{"key":"10_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/3-540-44829-2_17","volume-title":"Model Checking Software","author":"T.A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with Blast. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 235\u2013239. Springer, Heidelberg (2003)"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Hunt, S., Sands, D.: Binding time analysis: A new PERspective. In: Partial Evaluation and Semantics-Based Program Manipulation (PEPM 1991). Sigplan Notices, vol.\u00a026(9), pp. 154\u2013165 (1991)","DOI":"10.1145\/115865.115881"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: ACM Symposium on Principles of Programming Languages (POPL), pp. 14\u201326 (2001)","DOI":"10.1145\/373243.375719"},{"key":"10_CR18","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/S0167-6423(99)00024-6","volume":"37","author":"R. Joshi","year":"2000","unstructured":"Joshi, R., Leino, K.R.M.: A semantic approach to secure information flow. Science of Computer Programming\u00a037, 113\u2013138 (2000)","journal-title":"Science of Computer Programming"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"McCullough, D.: Specifications for multi-level security and a hook-up. In: IEEE Symposium on Security and Privacy, April 27-29, pp. 161\u2013166 (1987)","DOI":"10.1109\/SP.1987.10009"},{"key":"10_CR20","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F. Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999), Web page at www.imm.dtu.dk\/~riis\/PPA\/ppa.html"},{"key":"10_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"P. O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol.\u00a02142, pp. 1\u201319. Springer, Heidelberg (2001)"},{"key":"10_CR22","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P., Yang, H., Reynolds, J.: Separation and information hiding. In: ACM Symposium on Principles of Programming Languages (POPL), pp. 268\u2013280 (2004)","DOI":"10.1145\/964001.964024"},{"issue":"6","key":"10_CR23","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1017\/S0956796897002906","volume":"7","author":"P. \u00d8rb\u00e6k","year":"1997","unstructured":"\u00d8rb\u00e6k, P., Palsberg, J.: Trust in the \u03bb-calculus. Journal of Functional Programming\u00a07(6), 557\u2013591 (1997)","journal-title":"Journal of Functional Programming"},{"issue":"1","key":"10_CR24","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1145\/596980.596983","volume":"25","author":"F. Pottier","year":"2003","unstructured":"Pottier, F., Simonet, V.: Information flow inference for ML. ACM Transactions on Programming Languages and Systems\u00a025(1), 117\u2013158 (2003)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"10_CR25","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1109\/LICS.2002.1029817","volume-title":"IEEE Symposium on Logic in Computer Science (LICS)","author":"J.C. Reynolds","year":"2002","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: IEEE Symposium on Logic in Computer Science (LICS), pp. 55\u201374. IEEE Computer Society Press, Los Alamitos (2002)"},{"key":"10_CR26","doi-asserted-by":"crossref","unstructured":"Sabelfeld, A., Myers, A.: A model for delimited information release. In: Proceedings of the International Symposium on Software Security, ISSS 2003 (2004) (to appear)","DOI":"10.1007\/978-3-540-37621-7_9"},{"issue":"1","key":"10_CR27","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.C.: Language-based information-flow security. IEEE J. Selected Areas in Communications\u00a021(1), 5\u201319 (2003)","journal-title":"IEEE J. Selected Areas in Communications"},{"issue":"1","key":"10_CR28","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1023\/A:1011553200337","volume":"14","author":"A. Sabelfeld","year":"2001","unstructured":"Sabelfeld, A., Sands, D.: A Per model of secure information flow in sequential programs. Higher-order and Symbolic Computation\u00a014(1), 59\u201391 (2001)","journal-title":"Higher-order and Symbolic Computation"},{"key":"10_CR29","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)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27864-1_10.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,18]],"date-time":"2020-11-18T23:24:38Z","timestamp":1605741878000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27864-1_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540227915","9783540278641"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27864-1_10","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/b99688","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004]]}}}