{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T01:24:39Z","timestamp":1740101079657,"version":"3.37.3"},"reference-count":46,"publisher":"IEEE","license":[{"start":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T00:00:00Z","timestamp":1659312000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-009"},{"start":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T00:00:00Z","timestamp":1659312000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-001"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["2100989,CNS-1801546"],"award-info":[{"award-number":["2100989,CNS-1801546"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022,8]]},"DOI":"10.1109\/csf54842.2022.9919679","type":"proceedings-article","created":{"date-parts":[[2022,11,4]],"date-time":"2022-11-04T01:29:20Z","timestamp":1667525360000},"page":"486-500","source":"Crossref","is-referenced-by-count":1,"title":["Mapping Synthesis for Hyperproperties"],"prefix":"10.1109","author":[{"given":"Tzu-Han","family":"Hsu","sequence":"first","affiliation":[{"name":"Michigan State University,Department of Computer Science and Engineering,USA"}]},{"given":"Borzoo","family":"Bonakdarpour","sequence":"additional","affiliation":[{"name":"Michigan State University,Department of Computer Science and Engineering,USA"}]},{"given":"Eunsuk","family":"Kang","sequence":"additional","affiliation":[{"name":"School of Computer Science, Carnegie Mellon University,USA"}]},{"given":"Stavros","family":"Tripakis","sequence":"additional","affiliation":[{"name":"Khoury College of Computer Sciences, Northeastern University,USA"}]}],"member":"263","reference":[{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54580-5_5"},{"key":"ref35","article-title":"Bounded model checking for hyperproperties","author":"hsu","year":"0","journal-title":"Proceedings of the 27th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS)"},{"key":"ref12","first-page":"8","article-title":"Monitoring hyper-properties by combining static analysis and runtime verification","author":"bonakdarpour","year":"0","journal-title":"Proceedings of the 8th Leveraging Applications of Formal Methods Verification and Validation (ISoLA)"},{"journal-title":"Communicating Sequential Processes","year":"1985","author":"hoare","key":"ref34"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45251-6_8"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/4372.4373"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1109\/SECPRI.1989.36298"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0032063"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1982.10014"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/CSF49147.2020.00033"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1109\/CSFW.2001.930154"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31784-3_25"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17465-1_7"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2016.24"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785713"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1109\/SECPRI.2001.924289"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0393"},{"key":"ref38","first-page":"219","article-title":"Automated synthesis of secure platform mappings","author":"kang","year":"0","journal-title":"Proceedings of the 31st International Conference Computer Aided Verification (CAV) Part I"},{"key":"ref19","first-page":"14","article-title":"Deciding hyperproperties","volume":"13","author":"finkbeiner","year":"0","journal-title":"Proceedings of the 27th International Conference on Concurrency Theory (CONCUR)"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_7"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-019-00334-z"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190121"},{"key":"ref23","first-page":"194","article-title":"RVHyper: A runtime verification tool for temporal hyperproperties","author":"finkbeiner","year":"0","journal-title":"Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)"},{"key":"ref45","first-page":"406","article-title":"Graybox monitoring of hyperproperties","author":"stucki","year":"0","journal-title":"Proceedings of the 23rd International Symposium on Formal Methods (FM)"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134080"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_8"},{"key":"ref20","first-page":"521","article-title":"MGHyper: Checking satisfiability of HyperLTL formulas beyond the \\exists ^*\\forall ^* $\\exists_{\\ast}\\ \\forall_{\\ast}$ fragment","author":"finkbeiner","year":"0","journal-title":"Proceedings of the 16th International Symposium on Automated Technology for Verification and Analysis (ATVA)"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-1996-4103"},{"key":"ref41","first-page":"147","article-title":"A calculus of information flow","author":"o'halloran","year":"0","journal-title":"Proceedings of the First European Symposium on Research in Computer Security (ESORICS)"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_29"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0249-7"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-019-00358-2"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-75227-1_10"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.53"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_3"},{"key":"ref29","first-page":"35","article-title":"On the refinement of non-interference","author":"cumming","year":"0","journal-title":"Proc of the IEEE Computer Security Foundations Workshop (CSFW)"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/CSF51468.2021.00010"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00019"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/11787006_10"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(85)90056-0"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00031"},{"journal-title":"Principles of Model Checking","year":"2008","author":"baier","key":"ref5"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1109\/RISP.1994.296590"}],"event":{"name":"2022 IEEE 35th Computer Security Foundations Symposium (CSF)","start":{"date-parts":[[2022,8,7]]},"location":"Haifa, Israel","end":{"date-parts":[[2022,8,10]]}},"container-title":["2022 IEEE 35th Computer Security Foundations Symposium (CSF)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9919409\/9919636\/09919679.pdf?arnumber=9919679","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,8]],"date-time":"2023-11-08T23:19:26Z","timestamp":1699485566000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9919679\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8]]},"references-count":46,"URL":"https:\/\/doi.org\/10.1109\/csf54842.2022.9919679","relation":{},"subject":[],"published":{"date-parts":[[2022,8]]}}}