{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:17:01Z","timestamp":1725560221027},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540280057"},{"type":"electronic","value":"9783540318644"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11532231_9","type":"book-chapter","created":{"date-parts":[[2010,7,21]],"date-time":"2010-07-21T18:56:52Z","timestamp":1279738612000},"page":"116-130","source":"Crossref","is-referenced-by-count":16,"title":["Privacy-Sensitive Information Flow with JML"],"prefix":"10.1007","author":[{"given":"Guillaume","family":"Dufay","sequence":"first","affiliation":[]},{"given":"Amy","family":"Felty","sequence":"additional","affiliation":[]},{"given":"Stan","family":"Matwin","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","first-page":"253","volume-title":"Proceedings of the 15th IEEE Computer Security Foundations Workshop","author":"A. Banerjee","year":"2002","unstructured":"Banerjee, A., Naumann, D.A.: Secure information flow and pointer confinement in a Java-like language. In: Proceedings of the 15th IEEE Computer Security Foundations Workshop, p. 253. IEEE Computer Society, Los Alamitos (2002)"},{"key":"9_CR2","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1109\/CSFW.2004.1310735","volume-title":"Proceedings of the 17th IEEE Computer Security Foundations Workshop","author":"G. Barthe","year":"2004","unstructured":"Barthe, G., D\u2019Argenio, P., Rezk, T.: Secure information flow by self-composition. In: Proceedings of the 17th IEEE Computer Security Foundations Workshop, pp. 100\u2013114. IEEE Computer Society, Los Alamitos (2004)"},{"key":"9_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/3-540-45681-3_12","volume-title":"Principles of Data Mining and Knowledge Discovery","author":"A. Felty","year":"2002","unstructured":"Felty, A., Matwin, S.: Privacy-oriented data mining by proof checking. In: Elomaa, T., Mannila, H., Toivonen, H. (eds.) PKDD 2002. LNCS (LNAI), vol.\u00a02431, p. 138. Springer, Heidelberg (2002)"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Ferrari, E., Samarati, P., Bertino, E., Jajodia, S.: Providing flexibility in information flow control for object-oriented systems. In: Proceedings of the 1997 IEEE Symposium on Security and Privacy (May 1997)","DOI":"10.1109\/SECPRI.1997.601328"},{"key":"9_CR5","unstructured":"Filli\u00e2tre, J.-C.: Why: A multi-language multi-prover verification tool. Research Report 1366, LRI, Universit\u00e9 Paris Sud (March 2003)"},{"key":"9_CR6","unstructured":"Giambiagi, P., Dam, M.: Verification of confidentiality properties for Java Card applets. Manuscript (2003)"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: Proceedings of 1982 IEEE Symposium on Security and Privacy, pp. 11\u201320 (1982)","DOI":"10.1109\/SP.1982.10014"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/11423409_19","volume-title":"Privacy Enhancing Technologies","author":"K. Hayati","year":"2005","unstructured":"Hayati, K., Abadi, M.: Language-based enforcement of privacy policies. In: Martin, D., Serjantov, A. (eds.) PET 2004. LNCS, vol.\u00a03424, pp. 302\u2013313. Springer, Heidelberg (2005)"},{"issue":"10","key":"9_CR9","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commununications of ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Commununications of ACM"},{"key":"9_CR10","unstructured":"JACK: Java Applet Correctness Kit., \n                  \n                    http:\/\/www-sop.inria.fr\/everest\/soft\/Jack\/jack.html"},{"key":"9_CR11","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/978-1-4615-5229-1_12","volume-title":"Behavioral Specifications of Businesses and Systems","author":"G.T. Leavens","year":"1999","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: JML: A notation for detailed design. In: Behavioral Specifications of Businesses and Systems, pp. 175\u2013188. Kluwer Academic Publishers, Dordrecht (1999), \n                  \n                    http:\/\/www.jmlspecs.org"},{"issue":"1\u20132","key":"9_CR12","first-page":"86","volume":"58","author":"C. March\u00e9","year":"2004","unstructured":"March\u00e9, C., Paulin-Mohring, C., Urbain, X.: The Krakatoa Tool for Certification of Java\/JavaCard Programs annotated in JML. Journal of Logic and Algebraic Programming\u00a058(1\u20132), 86\u2013106 (2004)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"9_CR13","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the Seventh International Conference on Typed Lambda Calculi and Applications","author":"S. Matwin","year":"2005","unstructured":"Matwin, S., Felty, A., Hern\u00e1dv\u00f6lgyi, I., Capretta, V.: Privacy in data mining using formal methods. In: Proceedings of the Seventh International Conference on Typed Lambda Calculi and Applications. LNCS, vol.\u00a02841, Springer, Heidelberg (2005)"},{"key":"9_CR14","unstructured":"Coq Development Team. The Coq Proof Assistant Reference Manual \u2013 Version 8.0 (2004), \n                  \n                    http:\/\/coq.inria.fr\/doc\/"},{"key":"9_CR15","unstructured":"Information and Privacy Commissioner\/Ontario. Data mining: Staking a claim on your privacy (January 1998), \n                  \n                    http:\/\/www.ipc.on.ca\/scripts\/index.asp?action=31&P_ID=11387"},{"key":"9_CR16","volume-title":"Object-Oriented Software Construction","author":"B. Meyer","year":"1997","unstructured":"Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice Hall, Englewood Cliffs (1997)","edition":"2"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Myers, A.C.: JFlow: Practical mostly-static information flow control. In: Symposium on Principles of Programming Languages (POPL), January 1999, pp. 228\u2013241 (1999)","DOI":"10.1145\/292540.292561"},{"key":"9_CR18","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1109\/CSFW.2004.1310740","volume-title":"Proceedings of the 17th IEEE Computer Security Foundations Workshop","author":"A.C. Myers","year":"2004","unstructured":"Myers, A.C., Sabelfeld, A., Zdancewic, S.: Enforcing robust declassification. In: Proceedings of the 17th IEEE Computer Security Foundations Workshop, pp. 172\u2013186. IEEE Computer Society, Los Alamitos (2004)"},{"issue":"1","key":"9_CR19","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"},{"key":"9_CR20","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1109\/CSFW.2001.930141","volume-title":"Proceedings of the 14th IEEE Computer Security Foundations Workshop","author":"G. Smith","year":"2001","unstructured":"Smith, G.: A new type system for secure information flow. In: Proceedings of the 14th IEEE Computer Security Foundations Workshop, p. 115. IEEE Computer Society, Los Alamitos (2001)"},{"key":"9_CR21","unstructured":"The LOOP Project, \n                  \n                    http:\/\/www.cs.kun.nl\/sos\/research\/loop\/"},{"key":"9_CR22","volume-title":"Data Mining","author":"I.H. Witten","year":"2000","unstructured":"Witten, I.H., Frank, E.: Data Mining. Morgan Kaufmann, San Francisco (2000)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-20"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11532231_9.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:09:18Z","timestamp":1605643758000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11532231_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540280057","9783540318644"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/11532231_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}