{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:48:08Z","timestamp":1772164088791,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":45,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,6,14]],"date-time":"2017-06-14T00:00:00Z","timestamp":1497398400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["Core-to-Core Program, A.Advanced Research Networks"],"award-info":[{"award-number":["Core-to-Core Program, A.Advanced Research Networks"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-15-2-0104 and FA8750-16-C-0022"],"award-info":[{"award-number":["FA8750-15-2-0104 and FA8750-16-C-0022"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-1314857"],"award-info":[{"award-number":["CNS-1314857"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"mext","award":["Kakenhi 17H01720"],"award-info":[{"award-number":["Kakenhi 17H01720"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,6,14]]},"DOI":"10.1145\/3062341.3062378","type":"proceedings-article","created":{"date-parts":[[2017,6,14]],"date-time":"2017-06-14T10:01:04Z","timestamp":1497434464000},"page":"362-375","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":59,"title":["Decomposition instead of self-composition for proving the absence of timing channels"],"prefix":"10.1145","author":[{"given":"Timos","family":"Antonopoulos","sequence":"first","affiliation":[{"name":"Yale University, USA"}]},{"given":"Paul","family":"Gazzillo","sequence":"additional","affiliation":[{"name":"Yale University, USA"}]},{"given":"Michael","family":"Hicks","sequence":"additional","affiliation":[{"name":"University of Maryland, USA"}]},{"given":"Eric","family":"Koskinen","sequence":"additional","affiliation":[{"name":"Yale University, USA"}]},{"given":"Tachio","family":"Terauchi","sequence":"additional","affiliation":[{"name":"JAIST, Japan"}]},{"given":"Shiyi","family":"Wei","sequence":"additional","affiliation":[{"name":"University of Maryland, USA"}]}],"member":"320","published-online":{"date-parts":[[2017,6,14]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325702"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2011.10.008"},{"key":"e_1_3_2_1_3_1","volume-title":"USENIX Security Symposium","author":"Almeida J. B.","year":"2016","unstructured":"J. B. Almeida , M. Barbosa , G. Barthe , F. Dupressoir , and M. Emmi . Verifying constant-time implementations . In USENIX Security Symposium , 2016 . J. B. Almeida, M. Barbosa, G. Barthe, F. Dupressoir, and M. Emmi. Verifying constant-time implementations. In USENIX Security Symposium, 2016."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2012.26"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009889"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.08.001"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/1009380.1009669"},{"key":"e_1_3_2_1_8_1","volume-title":"FM","author":"Barthe G.","year":"2011","unstructured":"G. Barthe , J. M. Crespo , and C. Kunz . Relational verification using product programs . In FM , 2011 . G. Barthe, J. M. Crespo, and C. Kunz. Relational verification using product programs. In FM, 2011."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190249"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009858"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32004-3_20"},{"key":"e_1_3_2_1_13_1","unstructured":"dk.brics.automaton. Finite-state automata and regular expressions for Java. http:\/\/www.brics.dk\/automaton\/ 2017.  dk.brics.automaton. Finite-state automata and regular expressions for Java. http:\/\/www.brics.dk\/automaton\/ 2017."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2756550"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44709-3_14"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806630"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542518"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480898"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.02.031"},{"key":"e_1_3_2_1_20_1","volume-title":"Grenoble INP","author":"Henry J.","year":"2011","unstructured":"J. Henry . Static analysis by path focusing. Master\u2019s thesis , Grenoble INP , 2011 . J. Henry. Static analysis by path focusing. Master\u2019s thesis, Grenoble INP, 2011."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2012.11.003"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/646761.706156"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/1971852.1971853"},{"key":"e_1_3_2_1_24_1","volume-title":"The password guessing bug in Tenex. https:\/\/www.sjoerdlangkemper.nl\/2016\/11\/01\/ tenex-password-bug\/","author":"Langkemper S.","year":"2016","unstructured":"S. Langkemper . The password guessing bug in Tenex. https:\/\/www.sjoerdlangkemper.nl\/2016\/11\/01\/ tenex-password-bug\/ , 2016 . S. Langkemper. The password guessing bug in Tenex. https:\/\/www.sjoerdlangkemper.nl\/2016\/11\/01\/ tenex-password-bug\/, 2016."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190251"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_2"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/11863908_18"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_14"},{"key":"e_1_3_2_1_29_1","volume-title":"CSF","author":"Pasareanu C. S.","year":"2016","unstructured":"C. S. Pasareanu , Q. Phan , and P. Malacaria . Multi-run sidechannel analysis using symbolic execution and max-SMT . In CSF , 2016 . C. S. Pasareanu, Q. Phan, and P. Malacaria. Multi-run sidechannel analysis using symbolic execution and max-SMT. In CSF, 2016."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/1018438.1021840"},{"key":"e_1_3_2_1_31_1","volume-title":"The Craft of Programming","author":"Reynolds J. C.","year":"1981","unstructured":"J. C. Reynolds . The Craft of Programming . Prentice Hall International series in computer science. Prentice Hall , 1981 . J. C. Reynolds. The Craft of Programming. Prentice Hall International series in computer science. Prentice Hall, 1981."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00596-1_21"},{"key":"e_1_3_2_1_33_1","volume-title":"Checking probabilistic noninterference using JOANA. it - Information Technology, 56(6)","author":"Snelting G.","year":"2014","unstructured":"G. Snelting , D. Giffhorn , J. Graf , C. Hammer , M. Hecker , M. Mohr , and D. Wasserrab . Checking probabilistic noninterference using JOANA. it - Information Technology, 56(6) , 2014 . G. Snelting, D. Giffhorn, J. Graf, C. Hammer, M. Hecker, M. Mohr, and D. Wasserrab. Checking probabilistic noninterference using JOANA. it - Information Technology, 56(6), 2014."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908092"},{"key":"e_1_3_2_1_35_1","unstructured":"STAC. DARPA space\/time analysis for cybersecurity (STAC) program. http:\/\/www.darpa.mil\/program\/ space-time-analysis-for-cybersecurity 2017.  STAC. DARPA space\/time analysis for cybersecurity (STAC) program. http:\/\/www.darpa.mil\/program\/ space-time-analysis-for-cybersecurity 2017."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_24"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1134744.1134750"},{"issue":"2","key":"e_1_3_2_1_38_1","volume":"4","author":"Volpano D. M.","year":"1996","unstructured":"D. M. Volpano , C. E. Irvine , and G. Smith . A sound type system for secure flow analysis. Journal of Computer Security , 4 ( 2\/3 ), 1996 . D. M. Volpano, C. E. Irvine, and G. Smith. A sound type system for secure flow analysis. Journal of Computer Security, 4 (2\/3), 1996.","journal-title":"Journal of Computer Security"},{"key":"e_1_3_2_1_39_1","unstructured":"WALA. IBM T.J. Watson Libraries for Analysis (WALA). http:\/\/wala.sourceforge.net\/ 2017.  WALA. IBM T.J. Watson Libraries for Analysis (WALA). http:\/\/wala.sourceforge.net\/ 2017."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.036"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2010.9"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/2590708.2590710"},{"key":"e_1_3_2_1_43_1","volume-title":"Quantitative information flow as safety and liveness hyperproperties. Theoretical Computer Science, 538","author":"Yasuoka H.","year":"2014","unstructured":"H. Yasuoka and T. Terauchi . Quantitative information flow as safety and liveness hyperproperties. Theoretical Computer Science, 538 , 2014 . H. Yasuoka and T. Terauchi. Quantitative information flow as safety and liveness hyperproperties. Theoretical Computer Science, 538, 2014."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_5"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254078"}],"event":{"name":"PLDI '17: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Barcelona Spain","acronym":"PLDI '17","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3062341.3062378","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3062341.3062378","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3062341.3062378","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:36:32Z","timestamp":1750203392000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3062341.3062378"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,6,14]]},"references-count":45,"alternative-id":["10.1145\/3062341.3062378","10.1145\/3062341"],"URL":"https:\/\/doi.org\/10.1145\/3062341.3062378","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3140587.3062378","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2017,6,14]]},"assertion":[{"value":"2017-06-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}