{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:27:28Z","timestamp":1761611248437},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642032394"},{"type":"electronic","value":"9783642032400"}],"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-03240-0_16","type":"book-chapter","created":{"date-parts":[[2009,7,27]],"date-time":"2009-07-27T10:27:38Z","timestamp":1248690458000},"page":"182-198","source":"Crossref","is-referenced-by-count":3,"title":["Automated Certification of Non-Interference in Rewriting Logic"],"prefix":"10.1007","author":[{"given":"Mauricio","family":"Alba-Castro","sequence":"first","affiliation":[]},{"given":"Mar\u00eda","family":"Alpuente","sequence":"additional","affiliation":[]},{"given":"Santiago","family":"Escobar","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"16_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)"},{"issue":"22","key":"16_CR2","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., De Francisco, N.: Abstract interpretation of operational semantics for secure information flow. Information Processing Letters\u00a083(22), 101\u2013108 (2002)","journal-title":"Information Processing Letters"},{"key":"16_CR3","first-page":"229","volume-title":"SAC 2002","author":"R. Barbuti","year":"2002","unstructured":"Barbuti, R., Bernardeschi, C., De Francisco, N.: Checking security of Java bytecode by abstract interpretation. In: SAC 2002, pp. 229\u2013236. ACM, New York (2002)"},{"key":"16_CR4","first-page":"100","volume-title":"CSFW 2004","author":"G. Barthe","year":"2004","unstructured":"Barthe, G., D\u2019Argenio, P., Rezk, T.: Secure information flow by self-composition. In: CSFW 2004, pp. 100\u2013114. IEEE, Los Alamitos (2004)"},{"key":"16_CR5","first-page":"230","volume-title":"SSP 2006","author":"G. Barthe","year":"2006","unstructured":"Barthe, G., Naumann, D., Rezk, T.: Deriving an information flow checker and certifying compiler for Java. In: SSP 2006, pp. 230\u2013242. IEEE, Los Alamitos (2006)"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-540-71316-6_10","volume-title":"Programming Languages and Systems","author":"G. Barthe","year":"2007","unstructured":"Barthe, G., Pichardie, D., Rezk, T.: A certified lightweight non-interference Java bytecode verifier. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 125\u2013140. Springer, Heidelberg (2007)"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"Barthe, G., Rezk, T.: Non-interference for a JVM-like language. In: TLDI 2005, pp. 103\u2013112 (2005)","DOI":"10.1145\/1040294.1040304"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Beringer, L., Hofmann, M.: Secure information flow and program logics. In: IEEE CSF 2007, pp. 233\u2013248 (2007)","DOI":"10.1109\/CSF.2007.30"},{"issue":"3","key":"16_CR9","first-page":"212","volume":"7","author":"L. Burdy","year":"2005","unstructured":"Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Rustan, K., Leino, M., Poll, E.: An overview of JML tools and applications. IJSTTT\u00a07(3), 212\u2013232 (2005)","journal-title":"IJSTTT"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude: A High-Performance Logical Framework","author":"M. Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol.\u00a04350. Springer, Heidelberg (2007)"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic Design of Program Analysis Frameworks. In: POPL 1979, pp. 269\u2013282 (1979)","DOI":"10.1145\/567752.567778"},{"issue":"7","key":"16_CR12","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":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/11532231_9","volume-title":"Automated Deduction \u2013 CADE-20","author":"G. Dufay","year":"2005","unstructured":"Dufay, G., Felty, A., Matwin, S.: Privacy-sensitive information flow with JML. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS, vol.\u00a03632, pp. 116\u2013130. Springer, Heidelberg (2005)"},{"key":"16_CR14","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":"16_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1007\/978-3-540-27813-9_46","volume-title":"Computer Aided Verification","author":"A. Farzan","year":"2004","unstructured":"Farzan, A., Chen, F., Meseguer, J., Rosu, G.: Formal analysis of Java programs in JavaFAN. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 501\u2013505. Springer, Heidelberg (2004)"},{"key":"16_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-540-27815-3_14","volume-title":"Algebraic Methodology and Software Technology","author":"A. Farzan","year":"2004","unstructured":"Farzan, A., Meseguer, J., Rosu, G.: Formal JVM code analysis in JavaFAN. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol.\u00a03116, pp. 132\u2013147. Springer, Heidelberg (2004)"},{"issue":"2-3","key":"16_CR17","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/s10207-007-0015-0","volume":"6","author":"N. Francesco De","year":"2007","unstructured":"De Francesco, N., Martini, L.: Instruction-level security typing by abstract interpretation. Int. J. of Inf. Sec.\u00a06(2-3), 85\u2013106 (2007)","journal-title":"Int. J. of Inf. Sec."},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Giacobazzi, R., Mastroeni, I.: Abstract non-interference: Parameterizing non-interference by abstract interpretation. In: POPL 2004, pp. 186\u2013197 (2004)","DOI":"10.1145\/964001.964017"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Hunt, S., Sands, D.: On flow-sensitive security types. In: POPL 2006, pp. 79\u201390 (2006)","DOI":"10.1145\/1111037.1111045"},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"Jacobs, B., Pieters, W., Warnier, M.: Statically checking confidentiality via dynamic labels. In: WITS 2005, pp. 50\u201356 (2005)","DOI":"10.1145\/1045405.1045411"},{"issue":"3","key":"16_CR21","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":"1","key":"16_CR22","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J. Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. TCS\u00a096(1), 73\u2013155 (1992)","journal-title":"TCS"},{"issue":"3","key":"16_CR23","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. TCS\u00a0373(3), 213\u2013237 (2007)","journal-title":"TCS"},{"key":"16_CR24","doi-asserted-by":"crossref","unstructured":"Myers, A.C.: Jflow: Practical mostly-static information flow control. In: POPL 1999, pp. 228\u2013241 (1999)","DOI":"10.1145\/292540.292561"},{"key":"16_CR25","unstructured":"Myers, A.C., Nystrom, N., Zheng, L., Zdancewic, S.: Jif: Java information flow. Software release (2001), http:\/\/www.cs.cornell.edu\/jif"},{"key":"16_CR26","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof carrying code. In: POPL 1997, pp. 106\u2013119 (1997)","DOI":"10.1145\/263699.263712"},{"issue":"3-4","key":"16_CR27","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1023\/B:JARS.0000021015.15794.82","volume":"31","author":"E. Rose","year":"2003","unstructured":"Rose, E.: Lightweight bytecode verification. J. Autom. Reason.\u00a031(3-4), 303\u2013334 (2003)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"16_CR28","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 Areas in Comm.\u00a021(1), 5\u201319 (2003)","journal-title":"IEEE J. on Selected Areas in Comm."},{"volume-title":"Term Rewriting Systems","year":"2003","key":"16_CR29","unstructured":"TeReSe (ed.): Term Rewriting Systems. Cambridge U. Press, Cambridge (2003)"},{"key":"16_CR30","unstructured":"Warnier, M.E.: Language Based Security for Java and JML. PhD thesis, Radboud University Nijmegen (2005)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03240-0_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T14:19:22Z","timestamp":1558448362000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03240-0_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642032394","9783642032400"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03240-0_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}