{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:43:50Z","timestamp":1770288230035,"version":"3.49.0"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319997247","type":"print"},{"value":"9783319997254","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-99725-4_17","type":"book-chapter","created":{"date-parts":[[2018,8,29]],"date-time":"2018-08-29T17:45:50Z","timestamp":1535564750000},"page":"263-283","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Verifying Bounded Subset-Closed Hyperproperties"],"prefix":"10.1007","author":[{"given":"Isabella","family":"Mastroeni","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michele","family":"Pasqua","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,8,29]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Agrawal, S., Bonakdarpour, B.: Runtime verification of k-safety hyperproperties in HyperLTL. In: IEEE 29th Computer Security Foundations Symposium, pp. 239\u2013252 (2016)","DOI":"10.1109\/CSF.2016.24"},{"issue":"4","key":"17_CR2","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B Alpern","year":"1985","unstructured":"Alpern, B., Schneider, F.B.: Defining liveness. Inf. Process. Lett. 21(4), 181\u2013185 (1985)","journal-title":"Inf. Process. Lett."},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Antonopoulos, T., Gazzillo, P., Hicks, M., Koskinen, E., Terauchi, T., Wei, S.: Decomposition instead of self-composition for proving the absence of timing channels. In: Proceedings of PLDI, pp. 362\u2013375 (2017)","DOI":"10.1145\/3062341.3062378"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Assaf, M., Naumann, D.A., Signoles, J., Totel, E., Tronel, F.: Hypercollecting semantics and its application to static analysis of information flow. In: Proceedings of POPL, pp. 874\u2013887 (2017)","DOI":"10.1145\/3009837.3009889"},{"key":"17_CR5","first-page":"47","volume":"173","author":"A Banerjee","year":"2007","unstructured":"Banerjee, A., Giacobazzi, R., Mastroeni, I.: What you lose is what you leak: Information leakage in declassification policies. ENTCS 173, 47\u201366 (2007)","journal-title":"ENTCS"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: Proceedings of 17th IEEE Computer Security Foundations Workshop, pp. 100\u2013114 (2004)","DOI":"10.1109\/CSFW.2004.1310735"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-319-73721-8_6","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S Buro","year":"2018","unstructured":"Buro, S., Mastroeni, I.: Abstract code injection - A semantic approach based on abstract non-interference. In: Dillig, I., Palsberg, J. (eds.) VMCAI 2018. LNCS, vol. 10747, pp. 116\u2013137. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-73721-8_6"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., S\u00e1nchez, C.: Temporal logics for hyperproperties. In: Proceedings of POST (2014)","DOI":"10.1007\/978-3-642-54792-8_15"},{"issue":"6","key":"17_CR9","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"MR Clarkson","year":"2010","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157\u20131210 (2010)","journal-title":"J. Comput. Secur."},{"issue":"5","key":"17_CR10","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1145\/1067625.806556","volume":"11","author":"E Cohen","year":"1977","unstructured":"Cohen, E.: Information transmission in computational systems. SIGOPS Oper. Syst. Rev. 11(5), 133\u2013139 (1977)","journal-title":"SIGOPS Oper. Syst. Rev."},{"issue":"1\u20132","key":"17_CR11","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/S0304-3975(00)00313-3","volume":"277","author":"P Cousot","year":"2002","unstructured":"Cousot, P.: Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theor. Comput. Sci. 277(1\u20132), 47\u2013103 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of POPL, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of POPL, pp. 269\u2013282 (1979)","DOI":"10.1145\/567752.567778"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages). In: Proceedings of ICCL, pp. 95\u2013112 (1994)","DOI":"10.1109\/ICCL.1994.288389"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-319-21690-4_3","volume-title":"Computer Aided Verification","author":"B Finkbeiner","year":"2015","unstructured":"Finkbeiner, B., Rabe, M.N., S\u00e1nchez, C.: Algorithms for model checking HyperLTL and HyperCTL$$^*$$\u2217. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 30\u201348. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_3"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Giacobazzi, R., Logozzo, F., Ranzato, F.: Analyzing program analyses. In: Proceedings of POPL, pp. 261\u2013273 (2015)","DOI":"10.1145\/2676726.2676987"},{"issue":"1\u20133","key":"17_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.tcs.2004.12.021","volume":"337","author":"R Giacobazzi","year":"2005","unstructured":"Giacobazzi, R., Mastroeni, I.: Transforming semantics by abstract interpretation. Theor. Comput. Sci. 337(1\u20133), 1\u201350 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"17_CR18","doi-asserted-by":"crossref","unstructured":"Giacobazzi, R., Mastroeni, I.: Abstract non-interference: parameterizing non-interference by abstract interpretation. In: Proceedings of POPL, pp. 186\u2013197 (2004)","DOI":"10.1145\/964001.964017"},{"issue":"2","key":"17_CR19","doi-asserted-by":"publisher","first-page":"9:1","DOI":"10.1145\/3175660","volume":"21","author":"R Giacobazzi","year":"2018","unstructured":"Giacobazzi, R., Mastroeni, I.: Abstract non-interference: a unifying framework for weakening information-flow. ACM Trans. Priv. Secur 21(2), 9:1\u20139:31 (2018)","journal-title":"ACM Trans. Priv. Secur"},{"key":"17_CR20","unstructured":"Giacobazzi, R., Ranzato, F.: Personal communication (2017)"},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Security and Privacy, pp. 11\u201320 (1982)","DOI":"10.1109\/SP.1982.10014"},{"key":"17_CR22","doi-asserted-by":"crossref","unstructured":"Hunt, S., Mastroeni, I.: The PER model of abstract non-interference. In: Proceedings of 12th International Symposium on Static Analysis, pp. 171\u2013185 (2005)","DOI":"10.1007\/11547662_13"},{"issue":"6","key":"17_CR23","first-page":"1253","volume":"21","author":"I Mastroeni","year":"2011","unstructured":"Mastroeni, I., Banerjee, A.: Modelling declassification policies using abstract domain completeness. MSCS 21(6), 1253\u20131299 (2011)","journal-title":"MSCS"},{"key":"17_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/978-3-642-16901-4_30","volume-title":"Formal Methods and Software Engineering","author":"I Mastroeni","year":"2010","unstructured":"Mastroeni, I., Nikoli\u0107, \u0110.: Abstract program slicing: from theory towards an implementation. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 452\u2013467. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16901-4_30"},{"key":"17_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/978-3-319-66706-5_12","volume-title":"Static Analysis","author":"I Mastroeni","year":"2017","unstructured":"Mastroeni, I., Pasqua, M.: Hyperhierarchy of semantics - A formal framework for hyperproperties verification. In: Ranzato, F. (ed.) SAS 2017. LNCS, vol. 10422, pp. 232\u2013252. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66706-5_12"},{"issue":"1","key":"17_CR26","doi-asserted-by":"publisher","first-page":"7:1","DOI":"10.1145\/3029052","volume":"18","author":"I Mastroeni","year":"2017","unstructured":"Mastroeni, I., Zanardini, D.: Abstract program slicing: An abstract interpretation-based approach to program slicing. ACM TOCL 18(1), 7:1\u20137:58 (2017)","journal-title":"ACM TOCL"},{"key":"17_CR27","doi-asserted-by":"crossref","unstructured":"Naumann, D.A.: From coupling relations to mated invariants for checking information flow. In: Proceedings of ESORICS, pp. 279\u2013296 (2006)","DOI":"10.1007\/11863908_18"},{"key":"17_CR28","unstructured":"Pasqua, M., Mastroeni, I.: On topologies for (hyper)properties. In: Proceedings of ICTCS, pp. 1\u201312 (2017). http:\/\/ceur-ws.org\/Vol-1949\/ICTCSpaper13.pdf"},{"key":"17_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/978-3-540-24725-8_3","volume-title":"Programming Languages and Systems","author":"F Ranzato","year":"2004","unstructured":"Ranzato, F., Tapparo, F.: Strong preservation as completeness in abstract interpretation. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 18\u201332. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24725-8_3"},{"key":"17_CR30","doi-asserted-by":"crossref","unstructured":"Sousa, M., Dillig, I.: Cartesian hoare logic for verifying k-safety properties. In: Proceedings of PLDI, pp. 57\u201369 (2016)","DOI":"10.1145\/2908080.2908092"},{"key":"17_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1007\/11547662_24","volume-title":"Static Analysis","author":"T Terauchi","year":"2005","unstructured":"Terauchi, T., Aiken, A.: Secure information flow as a safety problem. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 352\u2013367. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11547662_24"},{"key":"17_CR32","doi-asserted-by":"crossref","unstructured":"Urban, C., M\u00fcller, P.: An abstract interpretation framework for input data usage. In: ESOP, pp. 683\u2013710 (2018)","DOI":"10.1007\/978-3-319-89884-1_24"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-99725-4_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,6]],"date-time":"2025-07-06T17:25:30Z","timestamp":1751822730000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-99725-4_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319997247","9783319997254"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-99725-4_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}