{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T01:15:14Z","timestamp":1742951714424,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642214608"},{"type":"electronic","value":"9783642214615"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-21461-5_10","type":"book-chapter","created":{"date-parts":[[2011,6,10]],"date-time":"2011-06-10T09:25:36Z","timestamp":1307697936000},"page":"153-167","source":"Crossref","is-referenced-by-count":0,"title":["An Accurate Type System for Information Flow in Presence of Arrays"],"prefix":"10.1007","author":[{"given":"S\u00e9verine","family":"Fratani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Marc","family":"Talbot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-11957-6_4","volume-title":"Programming Languages and Systems","author":"T. Amtoft","year":"2010","unstructured":"Amtoft, T., Hatcliff, J., Rodr\u00edguez, E.: Precise and automated contract-based reasoning for verification and certification of information flow properties of programs with arrays. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 43\u201363. Springer, Heidelberg (2010)"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/3-540-44585-4_34","volume-title":"Computer Aided Verification","author":"A. Annichini","year":"2001","unstructured":"Annichini, A., Bouajjani, A., Sighireanu, M.: Trex: A tool for reachability analysis of complex systems. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 368\u2013372. Springer, Heidelberg (2001)"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-540-45069-6_12","volume-title":"Computer Aided Verification","author":"S. Bardin","year":"2003","unstructured":"Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: Fast: Fast acceleration of symbolikc transition systems. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 118\u2013121. Springer, Heidelberg (2003)"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/11741060_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"E. Bonelli","year":"2006","unstructured":"Bonelli, E., Compagnoni, A., Medel, R.: Information flow analysis for a typed assembly language with polymorphic stacks. In: Barthe, G., Gr\u00e9goire, B., Huisman, M., Lanet, J.-L. (eds.) CASSIS 2005. LNCS, vol.\u00a03956, pp. 37\u201356. Springer, Heidelberg (2006)"},{"key":"10_CR5","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1109\/CSFW.2004.1310736","volume-title":"17th IEEE Computer Security Foundations Workshop, (CSFW-17 2004)","author":"Z. Deng","year":"2004","unstructured":"Deng, Z., Smith, G.: Lenient array operations for practical secure information flow. In: 17th IEEE Computer Security Foundations Workshop (CSFW-17 2004), p. 115. IEEE Computer Society Press, Los Alamitos (2004)"},{"issue":"5","key":"10_CR6","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/360051.360056","volume":"19","author":"D. Denning","year":"1976","unstructured":"Denning, D.: A lattice model of secure information flow. Commun. ACM\u00a019(5), 236\u2013243 (1976)","journal-title":"Commun. ACM"},{"issue":"7","key":"10_CR7","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. Commun. ACM\u00a020(7), 504\u2013513 (1977)","journal-title":"Commun. ACM"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-540-30579-8_23","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Genaim","year":"2005","unstructured":"Genaim, S., Spoto, F.: Information flow analysis for java bytecode. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 346\u2013362. Springer, Heidelberg (2005)"},{"key":"10_CR9","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1145\/1375581.1375623","volume-title":"Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation","author":"N. Halbwachs","year":"2008","unstructured":"Halbwachs, N., P\u00e9ron, M.: Discovering properties about arrays in simple programs. In: Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, pp. 339\u2013348. ACM Press, New York (2008)"},{"key":"10_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-540-89439-1_24","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"T. Henzinger","year":"2008","unstructured":"Henzinger, T., Hottelier, T., Kov\u00e1cs, L.: Valigator: A verification tool with bound and invariant generation. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol.\u00a05330, pp. 333\u2013342. Springer, Heidelberg (2008)"},{"key":"10_CR11","first-page":"79","volume-title":"Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL 2006","author":"S. Hunt","year":"2006","unstructured":"Hunt, S., Sands, D.: On flow-sensitive security types. In: Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL 2006, pp. 79\u201390. ACM Press, New York (2006)"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Myers, A.: Jflow: Practical mostly-static information flow control. In: POPL, pp. 228\u2013241 (1999)","DOI":"10.1145\/292540.292561"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-642-11319-2_21","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"V. Perrelle","year":"2010","unstructured":"Perrelle, V., Halbwachs, N.: An analysis of permutations in arrays. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol.\u00a05944, pp. 279\u2013294. Springer, Heidelberg (2010)"},{"issue":"1","key":"10_CR14","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 Trans. Program. Lang. Syst.\u00a025(1), 117\u2013158 (2003)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10_CR15","doi-asserted-by":"publisher","first-page":"2003","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 (2003)","journal-title":"IEEE Journal on Selected Areas in Communications"},{"issue":"2\/3","key":"10_CR16","doi-asserted-by":"publisher","first-page":"167","DOI":"10.3233\/JCS-1996-42-304","volume":"4","author":"D. Volpano","year":"1996","unstructured":"Volpano, D., Irvine, C., Smith, G.: A sound type system for secure flow analysis. Journal of Computer Security\u00a04(2\/3), 167\u2013188 (1996)","journal-title":"Journal of Computer Security"},{"issue":"2","key":"10_CR17","first-page":"67","volume":"1","author":"J. Yao","year":"2007","unstructured":"Yao, J., Li, J.: Discretional array operations for secure information flow. Journal of Information and Computing Science\u00a01(2), 67\u201377 (2007)","journal-title":"Journal of Information and Computing Science"}],"container-title":["Lecture Notes in Computer Science","Formal Techniques for Distributed Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21461-5_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T20:07:59Z","timestamp":1558296479000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21461-5_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642214608","9783642214615"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21461-5_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}