{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T23:26:32Z","timestamp":1759879592616,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540230243"},{"type":"electronic","value":"9783540301240"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30124-0_23","type":"book-chapter","created":{"date-parts":[[2010,3,2]],"date-time":"2010-03-02T12:27:59Z","timestamp":1267532879000},"page":"280-294","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Proving Abstract Non-interference"],"prefix":"10.1007","author":[{"given":"Roberto","family":"Giacobazzi","sequence":"first","affiliation":[]},{"given":"Isabella","family":"Mastroeni","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2004,9,9]]},"reference":[{"issue":"1","key":"23_CR1","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 Trans. Program. Lang. Syst.\u00a02(1), 56\u201376 (1980)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"23_CR2","first-page":"247","volume-title":"Proc. of the 16th IEEE Symp. on Logic in Computer Science LICS 2001","author":"A. Appel","year":"2001","unstructured":"Appel, A.: Foundational proof-carrying code. In: Proc. of the 16th IEEE Symp. on Logic in Computer Science LICS 2001, pp. 247\u2013258. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"23_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-2714-2","volume-title":"Verification of sequential and concurrent programs","author":"K. Apt","year":"1997","unstructured":"Apt, K., Olderog, E.-R.: Verification of sequential and concurrent programs. Springer, Berlin (1997)"},{"key":"23_CR4","unstructured":"Bell, D.E., Burke, E.: A software validation technique for certification: The methodology. Technical Report MTR-2932, MITRE Corp. Badford, MA (1974)"},{"key":"23_CR5","unstructured":"Bell, D.E., LaPadula, L.J.: Secure computer systems: Mathematical foundations and model. Technical Report M74-244, MITRE Corp. Badford, MA (1973)"},{"issue":"1","key":"23_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"},{"issue":"5","key":"23_CR7","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1145\/1067625.806556","volume":"11","author":"E.S. Cohen","year":"1977","unstructured":"Cohen, E.S.: Information transmission in computational systems. ACM SIGOPS Operating System Review\u00a011(5), 133\u2013139 (1977)","journal-title":"ACM SIGOPS Operating System Review"},{"issue":"1-2","key":"23_CR8","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/S0304-3975(00)00313-3","volume":"277","author":"P. Cousot","year":"2002","unstructured":"Cousot, P.: Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theor. Comput. Sci.\u00a0277(1-2), 47, 103 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"23_CR9","first-page":"238","volume-title":"Proc. of Conf. Record of the 4th ACM Symp. on Principles of Programming Languages (POPL 1977)","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: Proc. of Conf. Record of the 4th ACM Symp. on Principles of Programming Languages (POPL 1977), pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"23_CR10","first-page":"269","volume-title":"Proc. Of Conf. Record of the 6th ACM Symp. on Principles of Programming Languages (POPL 1979)","author":"P. Cousot","year":"1979","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proc. Of Conf. Record of the 6th ACM Symp. on Principles of Programming Languages (POPL 1979), pp. 269\u2013282. ACM Press, New York (1979)"},{"key":"23_CR11","first-page":"83","volume-title":"Proc. of Conf. Record of the 19th ACM Symp. on Principles of Programming Languages (POPL 1992)","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Inductive definitions, semantics and abstract interpretation. In: Proc. of Conf. Record of the 19th ACM Symp. on Principles of Programming Languages (POPL 1992), pp. 83\u201394. ACM Press, New York (1992)"},{"key":"23_CR12","unstructured":"Darvas, A., H\u00e4hnle, R., Sands, D.: A theorem proving approach to analysis of secure information flow. In: Gorrieri, R. (ed.) Workshop on Issues in the Theory of Security, WITS. IFIP WG 1.7, ACM SIGPLAN and GI FoMSESS (2003)"},{"issue":"5","key":"23_CR13","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/360051.360056","volume":"19","author":"D.E. Denning","year":"1976","unstructured":"Denning, D.E.: A lattice model of secure information flow. Communications of the ACM\u00a019(5), 236\u2013242 (1976)","journal-title":"Communications of the ACM"},{"issue":"7","key":"23_CR14","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1145\/359636.359712","volume":"20","author":"D.E. Denning","year":"1977","unstructured":"Denning, D.E., 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":"23_CR15","first-page":"191","volume-title":"Proc. of Conf. Record of the 29th ACM Symp. on Principles of Programming Languages (POPL 2002)","author":"C. Flanagan","year":"2002","unstructured":"Flanagan, C., Qadeer, S.: Pedicate abstraction for software verification. In: Proc. of Conf. Record of the 29th ACM Symp. on Principles of Programming Languages (POPL 2002), pp. 191\u2013202. ACM Press, New York (2002)"},{"key":"23_CR16","doi-asserted-by":"crossref","first-page":"186","DOI":"10.1145\/964001.964017","volume-title":"Proc. of the 31st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2004)","author":"R. Giacobazzi","year":"2004","unstructured":"Giacobazzi, R., Mastroeni, I.: Abstract non-interference: Parameterizing non-interference by abstract interpretation. In: Proc. of the 31st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2004), pp. 186\u2013197. ACM Press, New York (2004)"},{"key":"23_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"356","DOI":"10.1007\/3-540-47764-0_20","volume-title":"Static Analysis","author":"R. Giacobazzi","year":"2001","unstructured":"Giacobazzi, R., Quintarelli, E.: Incompleteness, counterexamples, and refinements in abstract model-checking. In: Cousot, P. (ed.) SAS 2001. LNCS, vol.\u00a02126, pp. 356\u2013373. Springer, Heidelberg (2001)"},{"issue":"1-3","key":"23_CR18","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/S0167-6423(97)00034-8","volume":"32","author":"R. Giacobazzi","year":"1998","unstructured":"Giacobazzi, R., Ranzato, F.: Optimal domains for disjunctive abstract interpretation. Sci. Comput. Program\u00a032(1-3), 177\u2013210 (1998)","journal-title":"Sci. Comput. Program"},{"key":"23_CR19","first-page":"11","volume-title":"Proc. IEEE Symp. on Security and Privacy","author":"J.A. Goguen","year":"1982","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: Proc. IEEE Symp. on Security and Privacy, pp. 11\u201320. IEEE Computer Society Press, Los Alamitos (1982)"},{"key":"23_CR20","first-page":"75","volume-title":"Proc. IEEE Symp. On Security and Privacy","author":"J.A. Goguen","year":"1984","unstructured":"Goguen, J.A., Meseguer, J.: Unwinding and inference control. In: Proc. IEEE Symp. On Security and Privacy, pp. 75\u201386. IEEE Computer Society Press, Los Alamitos (1984)"},{"key":"23_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"23_CR22","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":"23_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/3-540-45309-1_6","volume-title":"Programming Languages and Systems","author":"P. Laud","year":"2001","unstructured":"Laud, P.: Semantics and program analysis of computationally secure information flow. In: Sands, D. (ed.) ESOP 2001. LNCS, vol.\u00a02028, pp. 77\u201391. Springer, Heidelberg (2001)"},{"key":"23_CR24","first-page":"106","volume-title":"Proc. of Conf. Record of the 24th ACM Symp. on Principles of Programming Languages (POPL 1997)","author":"G. Necula","year":"1997","unstructured":"Necula, G.: Proof-carrying code. In: Proc. of Conf. Record of the 24th ACM Symp. on Principles of Programming Languages (POPL 1997), pp. 106\u2013119. ACM Press, New York (1997)"},{"key":"23_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/3-540-45789-5_29","volume-title":"Static Analysis","author":"F. Ranzato","year":"2002","unstructured":"Ranzato, F., Tapparo, F.: Making abstract model checking strongly preserving. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol.\u00a02477, pp. 411\u2013427. Springer, Heidelberg (2002)"},{"issue":"1","key":"23_CR26","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. on selected ares in communications\u00a021(1), 5\u201319 (2003)","journal-title":"IEEE J. on selected ares in communications"},{"issue":"1","key":"23_CR27","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":"23_CR28","first-page":"254","volume-title":"ICFP 2000","author":"C. Skalka","year":"2000","unstructured":"Skalka, C., Smith, S.: Static enforcement of security with types. In: ICFP 2000, pp. 254\u2013267. ACM Press, New York (2000)"},{"key":"23_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/3-540-48294-6_20","volume-title":"Static Analysis","author":"D. Volpano","year":"1999","unstructured":"Volpano, D.: Safety versus secrecy. In: Cortesi, A., Fil\u00e9, G. (eds.) SAS 1999. LNCS, vol.\u00a01694, pp. 303\u2013311. Springer, Heidelberg (1999)"},{"issue":"2,3","key":"23_CR30","doi-asserted-by":"publisher","first-page":"167","DOI":"10.3233\/JCS-1996-42-304","volume":"4","author":"D. Volpano","year":"1996","unstructured":"Volpano, D., Smith, G., Irvine, C.: A sound type system for secure flow analysis. Journal of Computer Security\u00a04(2,3), 167\u2013187 (1996)","journal-title":"Journal of Computer Security"},{"key":"23_CR31","doi-asserted-by":"publisher","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)"},{"key":"23_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/3-540-45789-5_26","volume-title":"Static Analysis","author":"M. Zanotti","year":"2002","unstructured":"Zanotti, M.: Security typings by abstract interpretation. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol.\u00a02477, pp. 360\u2013375. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30124-0_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,24]],"date-time":"2021-10-24T03:17:01Z","timestamp":1635045421000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30124-0_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540230243","9783540301240"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30124-0_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]},"assertion":[{"value":"9 September 2004","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}