{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T09:14:14Z","timestamp":1766135654436,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":30,"publisher":"ACM","license":[{"start":{"date-parts":[[2004,10,29]],"date-time":"2004-10-29T00:00:00Z","timestamp":1099008000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2004,10,29]]},"DOI":"10.1145\/1029133.1029136","type":"proceedings-article","created":{"date-parts":[[2005,1,30]],"date-time":"2005-01-30T17:58:48Z","timestamp":1107107928000},"page":"13-22","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Formally verifying information flow type systems for concurrent and thread systems"],"prefix":"10.1145","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[{"name":"INRIA Sophia-Antipolis, France"}]},{"given":"Leonor Prensa","family":"Nieto","sequence":"additional","affiliation":[{"name":"LORIA, France"}]}],"member":"320","published-online":{"date-parts":[[2004,10,29]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796804005453"},{"key":"e_1_3_2_1_2_1","volume-title":"Proceedings of CSFW'02","author":"Banerjee A.","year":"2002","unstructured":"A. Banerjee and D. A. Naumann . Secure Information Flow and Pointer Confinement in a Java-like Language . In Proceedings of CSFW'02 . IEEE Computer Society Press , 2002 .]] A. Banerjee and D. A. Naumann. Secure Information Flow and Pointer Confinement in a Java-like Language. In Proceedings of CSFW'02. IEEE Computer Society Press, 2002.]]"},{"key":"e_1_3_2_1_3_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/978-3-540-24622-0_2","volume-title":"Proceedings of VMCAI'04","author":"Barthe G.","year":"2004","unstructured":"G. Barthe , A. Basu , and T. Rezk . Security types preserving compilation . In B. Steffen and G. Levi, editors, Proceedings of VMCAI'04 , volume 2934 of Lecture Notes in Computer Science , pages 2 -- 15 . Springer-Verlag , 2004 .]] G. Barthe, A. Basu, and T. Rezk. Security types preserving compilation. In B. Steffen and G. Levi, editors, Proceedings of VMCAI'04, volume 2934 of Lecture Notes in Computer Science, pages 2--15. Springer-Verlag, 2004.]]"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/2780683.2780825"},{"key":"e_1_3_2_1_5_1","volume-title":"February","author":"Team Coq Development","year":"2003","unstructured":"Coq Development Team . The Coq Proof Assistant User's Guide. Version 7.4 , February 2003 .]] Coq Development Team. The Coq Proof Assistant User's Guide. Version 7.4, February 2003.]]"},{"key":"e_1_3_2_1_6_1","volume-title":"Proceedings of F-WAN","volume":"2002","author":"Crafa S.","unstructured":"S. Crafa , M. Bugliesi , and G. Castagna . Information flow security for boxed ambients. In V. Sassone, editor , Proceedings of F-WAN , volume 66(3) of Electronic Notes in Theoretical Computer Science. Elsevier Publishing, 2002 .]] S. Crafa, M. Bugliesi, and G. Castagna. Information flow security for boxed ambients. In V. Sassone, editor, Proceedings of F-WAN, volume 66(3) of Electronic Notes in Theoretical Computer Science. Elsevier Publishing, 2002.]]"},{"key":"e_1_3_2_1_7_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1007\/3-540-45608-2_6","volume-title":"Foundations of Security Analysis and Design","author":"Focardi R.","year":"2001","unstructured":"R. Focardi and R. Gorrieri . Classification of security properties: (part i: Information flow) . In R. Focardi and R. Gorrieri, editors, Foundations of Security Analysis and Design , volume 2171 of Lecture Notes in Computer Science , pages 331 -- 396 . Springer-Verlag , 2001 .]] R. Focardi and R. Gorrieri. Classification of security properties: (part i: Information flow). In R. Focardi and R. Gorrieri, editors, Foundations of Security Analysis and Design, volume 2171 of Lecture Notes in Computer Science, pages 331 --396. Springer-Verlag, 2001.]]"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1982.10014"},{"key":"e_1_3_2_1_9_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1007\/3-540-45022-X_35","volume-title":"Proceedings of ICALP'00","author":"Hennessy M.","year":"2000","unstructured":"M. Hennessy and J. Riely . Information flow vs. resource access in the information asynchronous pi-calculus . In U. Montanari, J. D. P. Rolim, and E. Welzl, editors, Proceedings of ICALP'00 , volume 1853 of Lecture Notes in Computer Science , pages 415 -- 427 . Springer , 2000 .]] M. Hennessy and J. Riely. Information flow vs. resource access in the information asynchronous pi-calculus. In U. Montanari, J. D. P. Rolim, and E. Welzl, editors, Proceedings of ICALP'00, volume 1853 of Lecture Notes in Computer Science, pages 415--427. Springer, 2000.]]"},{"key":"e_1_3_2_1_10_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1007\/978-3-540-45212-6_16","volume-title":"Proceedings of EMSOFT'03","author":"Henzinger T.A.","year":"2003","unstructured":"T.A. Henzinger , C.M. Kirsch , and S. Matic . Schedule-carrying code . In R. Alur and I. Lee, editors, Proceedings of EMSOFT'03 , volume 2855 of Lecture Notes in Computer Science , pages 241 -- 256 , 2003 .]] T.A. Henzinger, C.M. Kirsch, and S. Matic. Schedule-carrying code. In R. Alur and I. Lee, editors, Proceedings of EMSOFT'03, volume 2855 of Lecture Notes in Computer Science, pages 241--256, 2003.]]"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503281"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00869-1"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2003.07.004"},{"key":"e_1_3_2_1_14_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of APLAS'04","author":"Mantel H.","year":"2004","unstructured":"H. Mantel and D. Sands . Controlled Declassification based on Intransitive Noninterference . In Proceedings of APLAS'04 , Lecture Notes in Computer Science . Springer-Verlag , 2004 . To appear.]] H. Mantel and D. Sands. Controlled Declassification based on Intransitive Noninterference. In Proceedings of APLAS'04, Lecture Notes in Computer Science. Springer-Verlag, 2004. To appear.]]"},{"key":"e_1_3_2_1_15_1","volume-title":"Proceedings of FCS'04","author":"Matos A. Almeida","year":"2004","unstructured":"A. Almeida Matos , G. Boudol , and I. Castellani . Typing noninterference for reactive programs. In A. Sabelfeld, editor , Proceedings of FCS'04 , 2004 .]] A. Almeida Matos, G. Boudol, and I. Castellani. Typing noninterference for reactive programs. In A. Sabelfeld, editor, Proceedings of FCS'04, 2004.]]"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1009380.1009673"},{"key":"e_1_3_2_1_18_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"Nipkow T.","year":"2002","unstructured":"T. Nipkow , L. C. Paulson , and M. Wenzel . Isabelle\/HOL: A Proof Assistant for Higher-Order Logic , volume 2283 of Lecture Notes in Computer Science . Springer-Verlag , 2002 .]] T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer-Verlag, 2002.]]"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503302"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004653"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2002.806121"},{"key":"e_1_3_2_1_24_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of ISSS'03","author":"Sabelfeld A.","year":"2004","unstructured":"A. Sabelfeld and A. Myers . A model for delimited information release . In Proceedings of ISSS'03 , Lecture Notes in Computer Science . Springer-Verlag , 2004 .]] A. Sabelfeld and A. Myers. A model for delimited information release. In Proceedings of ISSS'03, Lecture Notes in Computer Science. Springer-Verlag, 2004.]]"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011553200337"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/872752.873517"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268975"},{"key":"e_1_3_2_1_28_1","volume-title":"Technische Universit\u00e4t M\u00fcnchen","author":"Strecker M.","year":"2003","unstructured":"M. Strecker . Formal analysis of an information flow type system for MicroJava (extended version). Technical report , Technische Universit\u00e4t M\u00fcnchen , July 2003 .]] M. Strecker. Formal analysis of an information flow type system for MicroJava (extended version). Technical report, Technische Universit\u00e4t M\u00fcnchen, July 2003.]]"},{"key":"e_1_3_2_1_29_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"607","DOI":"10.1007\/BFb0030629","volume-title":"Proceedings of TAPSOFT'97","author":"Volpano D.","year":"1997","unstructured":"D. Volpano and G. Smith . A Type-Based Approach to Program Security . In M. Bidoit and M. Dauchet, editors, Proceedings of TAPSOFT'97 , volume 1214 of Lecture Notes in Computer Science , pages 607 -- 621 . Springer-Verlag , 1997 .]] D. Volpano and G. Smith. A Type-Based Approach to Program Security. In M. Bidoit and M. Dauchet, editors, Proceedings of TAPSOFT'97, volume 1214 of Lecture Notes in Computer Science, pages 607--621. Springer-Verlag, 1997.]]"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/353594.353608"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/872752.873524"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2003.1212703"},{"key":"e_1_3_2_1_33_1","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Proceedings of MFPS'03","author":"Zwandewic S.","year":"2003","unstructured":"S. Zwandewic . A type system for robust declassification. In S. Brookes and P. Panangaden, editors, Proceedings of MFPS'03 , volume 83 of Electronic Notes in Theoretical Computer Science . Elsevier Publishing , 2003 .]] S. Zwandewic. A type system for robust declassification. In S. Brookes and P. Panangaden, editors, Proceedings of MFPS'03, volume 83 of Electronic Notes in Theoretical Computer Science. Elsevier Publishing, 2003.]]"}],"event":{"name":"CCS04: 11th ACM Conference on Computer and Communications Security 2004","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control","ACM Association for Computing Machinery"],"location":"Washington DC USA","acronym":"CCS04"},"container-title":["Proceedings of the 2004 ACM workshop on Formal methods in security engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1029133.1029136","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1029133.1029136","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:31:07Z","timestamp":1750264267000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1029133.1029136"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,10,29]]},"references-count":30,"alternative-id":["10.1145\/1029133.1029136","10.1145\/1029133"],"URL":"https:\/\/doi.org\/10.1145\/1029133.1029136","relation":{},"subject":[],"published":{"date-parts":[[2004,10,29]]},"assertion":[{"value":"2004-10-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}