{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T15:30:33Z","timestamp":1743003033644,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642170706"},{"type":"electronic","value":"9783642170713"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-17071-3_6","type":"book-chapter","created":{"date-parts":[[2010,11,11]],"date-time":"2010-11-11T07:12:58Z","timestamp":1289459578000},"page":"105-124","source":"Crossref","is-referenced-by-count":4,"title":["Abstract Certification of Global Non-interference in Rewriting Logic"],"prefix":"10.1007","author":[{"given":"Mauricio","family":"Alba-Castro","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mar\u00eda","family":"Alpuente","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Santiago","family":"Escobar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-79707-4_15","volume-title":"Formal Methods for Industrial Critical Systems","author":"M. Alba-Castro","year":"2008","unstructured":"Alba-Castro, M., Alpuente, M., Escobar, S.: Automatic certification of Java source code in rewriting logic. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol.\u00a04916, pp. 200\u2013217. Springer, Heidelberg (2008)"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-642-03240-0_16","volume-title":"Formal Methods for Industrial Critical Systems","author":"M. Alba-Castro","year":"2009","unstructured":"Alba-Castro, M., Alpuente, M., Escobar, S.: Automated certification of non-interference in rewriting logic. In: Cofer, D., Fantechi, A. (eds.) FMICS 2008. LNCS, vol.\u00a05596, pp. 182\u2013198. Springer, Heidelberg (2009)"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Amtoft, T., Bandhakavi, S., Banerjee, A.: A logic for information flow in object-oriented programs. In: Conference record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, pp. 91\u2013102 (2006)","DOI":"10.1145\/1111037.1111046"},{"issue":"22","key":"6_CR4","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0020-0190(02)00219-3","volume":"83","author":"R. Barbuti","year":"2002","unstructured":"Barbuti, R., Bernardeschi, C., Francesco, N.D.: Abstract interpretation of operational semantics for secure information flow. Information Processing Letters\u00a083(22), 101\u2013108 (2002)","journal-title":"Information Processing Letters"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Barthe, G., D\u2019Argenio, P., Rezk, T.: Secure information flow by self-composition. In: Proceedings of the 17th IEEE workshop on Computer Security Foundations, CSFW 2004, pp. 100\u2013114 (2004)","DOI":"10.1109\/CSFW.2004.1310735"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Bavera, F., Bonelli, E.: Type-based information flow analysis for bytecode languages with variable object field policies. In: SAC 2008, pp. 347\u2013351 (2008)","DOI":"10.1145\/1363686.1363776"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. In: Proc. IEEE Computer Security Foundations Symposium, CSF 2008 (2008)","DOI":"10.1109\/CSF.2008.7"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude: A High-Performance Logical Framework","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C. (eds.): All About Maude - A High-Performance Logical Framework. LNCS, vol.\u00a04350. Springer, Heidelberg (2007)"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic Design of Program Analysis Frameworks. In: Proc. of Sixth ACM Symp. on Principles of Programming Languages, pp. 269\u2013282 (1979)","DOI":"10.1145\/567752.567778"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-540-32004-3_20","volume-title":"Security in Pervasive Computing","author":"A. Darvas","year":"2005","unstructured":"Darvas, A., Hahnle, R., Sands, D.: A theorem proving approach to analysis of secure information flow. In: Hutter, D., Ullmann, M. (eds.) SPC 2005. LNCS, vol.\u00a03450, pp. 193\u2013209. Springer, Heidelberg (2005)"},{"issue":"7","key":"6_CR11","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.J.: Certification of programs for secure information flow. Commun. ACM\u00a020(7), 504\u2013513 (1977)","journal-title":"Commun. ACM"},{"key":"6_CR12","unstructured":"Farzan, A., Chen, F., Meseguer, J., Rosu, G.: JavaRL: The rewriting logic semantics of Java (2007), http:\/\/fsl.cs.uiuc.edu\/index.php\/Rewriting_Logic_Semantics_of_Java"},{"key":"6_CR13","doi-asserted-by":"publisher","first-page":"5","DOI":"10.3233\/JCS-1994\/1995-3103","volume":"3","author":"R. Focardi","year":"1994","unstructured":"Focardi, R., Gorrieri, R., Focardi, R., Gorrieri, R.: A classification of security properties for process algebras. Journal of Computer Security\u00a03, 5\u201333 (1994)","journal-title":"Journal of Computer Security"},{"issue":"2-3","key":"6_CR14","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/s10207-007-0015-0","volume":"6","author":"N.D. Francesco","year":"2007","unstructured":"Francesco, N.D., Martin, L.: Instruction-level security typing by abstract interpretation. International Journal of Information Security\u00a06(2-3), 85\u2013106 (2007)","journal-title":"International Journal of Information Security"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Research in Security and Privacy, pp. 11\u201320 (1982)","DOI":"10.1109\/SP.1982.10014"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Hunt, S., Sands, D.: On flow-sensitive security types. In: Conference record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles Of Programming Languages, POPL 2006, pp. 79\u201390 (2006)","DOI":"10.1145\/1111037.1111045"},{"issue":"3","key":"6_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1127878.1127884","volume":"31","author":"G. Leavens","year":"2006","unstructured":"Leavens, G., Baker, A., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. ACM SIGSOFT Software Engineering Notes\u00a031(3), 1\u201338 (2006)","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"issue":"3","key":"6_CR18","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1016\/j.tcs.2006.12.018","volume":"373","author":"J. Meseguer","year":"2007","unstructured":"Meseguer, J., Rosu, G.: The rewriting logic semantics project. Theoretical Computer Science\u00a0373(3), 213\u2013237 (2007)","journal-title":"Theoretical Computer Science"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof carrying code. In: Proceedings of the 24th ACM SIGPLAN-SIGACT Annual Symposium on Principles of Programming Languages POPL 1997, Paris, France, pp. 106\u2013119 (1997)","DOI":"10.1145\/263699.263712"},{"issue":"1","key":"6_CR20","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":"6_CR21","first-page":"203","volume-title":"CSF 2007: Proceedings of the 20th IEEE Computer Security Foundations Symposium","author":"P. Shroff","year":"2007","unstructured":"Shroff, P., Smith, S., Thober, M.: Dynamic dependency monitoring to secure information flow. In: CSF 2007: Proceedings of the 20th IEEE Computer Security Foundations Symposium, pp. 203\u2013217. IEEE Computer Society, Los Alamitos (2007)"},{"issue":"4","key":"6_CR22","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. Computer Security\u00a04(4), 167\u2013187 (1996)","journal-title":"Computer Security"},{"key":"6_CR23","unstructured":"Warnier, M.: Language Based Security for Java and JML. PhD thesis, Radboud University Nijmegen (2005)"},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"Wasserrab, D., Lohner, D., Snelting, G.: On pdg-based noninterference and its modular proof. In: Proceedings of the ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security (PLAS 2009), pp. 31\u201344 (2009)","DOI":"10.1145\/1554339.1554345"},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"Zanardini, D.: Analysing non\u2013interference with respect to classes. In: Proc. 10th italian Conference on Theoretical Computer Science (ICTCS 2007), pp. 57\u201369 (2007)","DOI":"10.1142\/9789812770998_0009"},{"key":"6_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","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. 375\u20132002. Springer, Heidelberg (2002)"}],"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-642-17071-3_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,6]],"date-time":"2019-06-06T01:56:49Z","timestamp":1559786209000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-17071-3_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642170706","9783642170713"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-17071-3_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}