{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:36:18Z","timestamp":1750307778491,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":24,"publisher":"ACM","license":[{"start":{"date-parts":[[2007,11,2]],"date-time":"2007-11-02T00:00:00Z","timestamp":1193961600000},"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":[[2007,11,2]]},"DOI":"10.1145\/1314436.1314438","type":"proceedings-article","created":{"date-parts":[[2007,11,15]],"date-time":"2007-11-15T14:30:20Z","timestamp":1195137020000},"page":"2-11","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Verification condition generation for conditional information flow"],"prefix":"10.1145","author":[{"given":"Torben","family":"Amtoft","sequence":"first","affiliation":[{"name":"Kansas State University, Manhattan, KS"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anindya","family":"Banerjee","sequence":"additional","affiliation":[{"name":"Kansas State University, Manhattan, KS"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2007,11,2]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_3_2_1_1_1","DOI":"10.1145\/1111037.1111046"},{"key":"e_1_3_2_1_2_1","series-title":"LNCS","first-page":"100","volume-title":"SAS","author":"Amtoft T.","year":"2004","unstructured":"T. Amtoft and A. Banerjee . Information flow analysis in logical form . In SAS , volume 3148 of LNCS , pages 100 -- 115 , 2004 . T. Amtoft and A. Banerjee. Information flow analysis in logical form. In SAS, volume 3148 of LNCS, pages 100--115, 2004."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_3_1","DOI":"10.1016\/j.scico.2006.03.002"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_5_1","DOI":"10.1017\/S0956796804005453"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_6_1","DOI":"10.1145\/1255329.1255340"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_7_1","DOI":"10.5381\/jot.2004.3.6.a2"},{"key":"e_1_3_2_1_8_1","series-title":"LNCS","first-page":"49","volume-title":"Selected papers of CASSIS","author":"Barnett M.","year":"2004","unstructured":"M. Barnett , K. R. M. Leino , and W. Schulte . The Spec# programming system: An overview . In Selected papers of CASSIS 2004 , volume 3362 of LNCS , pages 49 -- 69 , 2005. 10.1007\/978-3-540-30569-9_3 M. Barnett, K. R. M. Leino, and W. Schulte. The Spec# programming system: An overview. In Selected papers of CASSIS 2004, volume 3362 of LNCS, pages 49--69, 2005. 10.1007\/978-3-540-30569-9_3"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_9_1","DOI":"10.5555\/1009380.1009669"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_11_1","DOI":"10.1145\/2363.2366"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_12_1","DOI":"10.1007\/s10009-004-0167-4"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_13_1","DOI":"10.1145\/1032297.1032305"},{"key":"e_1_3_2_1_14_1","series-title":"LNCS","first-page":"108","volume-title":"Selected papers of CASSIS","author":"Cok D. R.","year":"2004","unstructured":"D. R. Cok and J. Kiniry . ESC\/Java2: Uniting ESC\/Java and JML . In Selected papers of CASSIS 2004 , volume 3362 of LNCS , pages 108 -- 128 , 2005. 10.1007\/978-3-540-30569-9_6 D. R. Cok and J. Kiniry. ESC\/Java2: Uniting ESC\/Java and JML. In Selected papers of CASSIS 2004, volume 3362 of LNCS, pages 108--128, 2005. 10.1007\/978-3-540-30569-9_6"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_15_1","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_16_1","series-title":"LNCS","first-page":"151","volume-title":"SPC","author":"Darvas A.","year":"2005","unstructured":"A. Darvas , R. H\u00e4hnle , and D. Sands . A theorem proving approach to analysis of secure information flow . In SPC , volume 3450 of LNCS , pages 151 -- 171 , 2005 . A. Darvas, R. H\u00e4hnle, and D. Sands. A theorem proving approach to analysis of secure information flow. In SPC, volume 3450 of LNCS, pages 151--171, 2005."},{"key":"e_1_3_2_1_17_1","series-title":"LNAI","first-page":"116","volume-title":"CADE-20","author":"Dufay G.","year":"2005","unstructured":"G. Dufay , A. Felty , and S. Matwin . Privacy-sensitive information flow with JML . In CADE-20 , volume 3632 of LNAI , pages 116 -- 130 , 2005 . 10.1007\/11532231_9 G. Dufay, A. Felty, and S. Matwin. Privacy-sensitive information flow with JML. In CADE-20, volume 3632 of LNAI, pages 116--130, 2005. 10.1007\/11532231_9"},{"key":"e_1_3_2_1_18_1","series-title":"LNCS","first-page":"148","volume-title":"CAV","author":"Dwyer M. B.","year":"2005","unstructured":"M. B. Dwyer , J. Hatcliff , M. Hoosier , and Robby. Building your own software model checker using the Bogor extensible model checking framework . In CAV , volume 3576 of LNCS , pages 148 -- 152 , 2005 . 10.1007\/11513988_15 M. B. Dwyer, J. Hatcliff, M. Hoosier, and Robby. Building your own software model checker using the Bogor extensible model checking framework. In CAV, volume 3576 of LNCS, pages 148--152, 2005. 10.1007\/11513988_15"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_19_1","DOI":"10.1109\/SP.1982.10014"},{"key":"e_1_3_2_1_20_1","first-page":"87","volume-title":"ISSSE","author":"Hammer C.","year":"2006","unstructured":"C. Hammer , J. Krinke , and G. Snelting . Information flow control for Java based on path conditions in dependence graphs . In ISSSE , pages 87 -- 96 , 2006 . C. Hammer, J. Krinke, and G. Snelting. Information flow control for Java based on path conditions in dependence graphs. In ISSSE, pages 87--96, 2006."},{"key":"e_1_3_2_1_21_1","series-title":"LNCS","first-page":"235","volume-title":"SPIN","author":"Henzinger T. A.","year":"2003","unstructured":"T. A. Henzinger , R. Jhala , R. Majumdar , and G. Sutre . Software verification with BLAST . In SPIN , volume 2648 of LNCS , pages 235 -- 239 , 2003 . T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Software verification with BLAST. In SPIN, volume 2648 of LNCS, pages 235--239, 2003."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"crossref","first-page":"228","DOI":"10.1145\/292540.292561","volume-title":"POPL","author":"Myers A. C.","year":"1999","unstructured":"A. C. Myers . JFlow : Practical mostly-static information flow control . In POPL , pages 228 -- 241 . ACM Press , 1999 . 10.1145\/292540.292561 A. C. Myers. JFlow: Practical mostly-static information flow control. In POPL, pages 228--241. ACM Press, 1999. 10.1145\/292540.292561"},{"key":"e_1_3_2_1_23_1","series-title":"LNCS","first-page":"279","volume-title":"ESORICS","author":"Naumann D. A.","year":"2006","unstructured":"D. A. Naumann . From coupling relations to mated invariants for checking information flow . In ESORICS , volume 4189 of LNCS , pages 279 -- 296 , 2006 . 10.1007\/11863908_18 D. A. Naumann. From coupling relations to mated invariants for checking information flow. In ESORICS, volume 4189 of LNCS, pages 279--296, 2006. 10.1007\/11863908_18"},{"key":"e_1_3_2_1_24_1","series-title":"LNCS","first-page":"174","volume-title":"ISSS","author":"Sabelfeld A.","year":"2004","unstructured":"A. Sabelfeld and A. C. Myers . A model for delimited information release . In ISSS , volume 3233 of LNCS , pages 174 -- 191 , 2004 . A. Sabelfeld and A. C. Myers. A model for delimited information release. In ISSS, volume 3233 of LNCS, pages 174--191, 2004."},{"key":"e_1_3_2_1_25_1","series-title":"LNCS","first-page":"352","volume-title":"SAS","author":"Terauchi T.","year":"2005","unstructured":"T. Terauchi and A. Aiken . Secure information flow as a safety problem . In SAS , volume 3672 of LNCS , pages 352 -- 367 , 2005 . 10.1007\/11547662_24 T. Terauchi and A. Aiken. Secure information flow as a safety problem. In SAS, volume 3672 of LNCS, pages 352--367, 2005. 10.1007\/11547662_24"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_26_1","DOI":"10.3233\/JCS-1996-42-304"}],"event":{"sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control","ACM Association for Computing Machinery"],"acronym":"CCS07","name":"CCS07: 14th ACM Conference on Computer and Communications Security 2007","location":"Fairfax Virginia USA"},"container-title":["Proceedings of the 2007 ACM workshop on Formal methods in security engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1314436.1314438","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1314436.1314438","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:56:04Z","timestamp":1750254964000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1314436.1314438"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,11,2]]},"references-count":24,"alternative-id":["10.1145\/1314436.1314438","10.1145\/1314436"],"URL":"https:\/\/doi.org\/10.1145\/1314436.1314438","relation":{},"subject":[],"published":{"date-parts":[[2007,11,2]]},"assertion":[{"value":"2007-11-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}