{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T18:12:28Z","timestamp":1781892748165,"version":"3.54.5"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319675305","type":"print"},{"value":"9783319675312","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-67531-2_12","type":"book-chapter","created":{"date-parts":[[2017,9,5]],"date-time":"2017-09-05T09:33:37Z","timestamp":1504604017000},"page":"190-207","source":"Crossref","is-referenced-by-count":28,"title":["Monitoring Hyperproperties"],"prefix":"10.1007","author":[{"given":"Bernd","family":"Finkbeiner","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Christopher","family":"Hahn","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marvin","family":"Stenger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Leander","family":"Tentrup","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,9,6]]},"reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Agrawal, S., Bonakdarpour, B.: Runtime verification of k-safety hyperproperties in HyperLTL. In: Proceedings of CSF, pp. 239\u2013252. IEEE Computer Society (2016)","DOI":"10.1109\/CSF.2016.24"},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"Askarov, A., Sabelfeld, A.: Tight enforcement of information-release policies for dynamic languages. In: Proceedings of CSF, pp. 43\u201359. IEEE Computer Society (2009)","DOI":"10.1109\/CSF.2009.22"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Austin, T.H., Flanagan, C.: Permissive dynamic information flow analysis. In: Proceedings of PLAS, p. 3. ACM (2010)","DOI":"10.1145\/1814217.1814220"},{"key":"12_CR4","unstructured":"Bauer, A.: Monitorability of omega-regular languages. CoRR abs\/1006.3638 (2010)"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/978-3-642-54792-8_9","volume-title":"Principles of Security and Trust","author":"A Bichhawat","year":"2014","unstructured":"Bichhawat, A., Rajani, V., Garg, D., Hammer, C.: Information flow control in WebKit\u2019s JavaScript bytecode. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 159\u2013178. Springer, Heidelberg (2014). doi:\n10.1007\/978-3-642-54792-8_9"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-319-46982-9_4","volume-title":"Runtime Verification","author":"B Bonakdarpour","year":"2016","unstructured":"Bonakdarpour, B., Finkbeiner, B.: Runtime verification for HyperLTL. In: Falcone, Y., S\u00e1nchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 41\u201345. Springer, Cham (2016). doi:\n10.1007\/978-3-319-46982-9_4"},{"key":"12_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-662-54580-5_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Brett","year":"2017","unstructured":"Brett, N., Siddique, U., Bonakdarpour, B.: Rewriting-based runtime verification for alternation-free HyperLTL. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 77\u201393. Springer, Heidelberg (2017). doi:\n10.1007\/978-3-662-54580-5_5"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Chudnov, A., Kuan, G., Naumann, D.A.: Information flow monitoring as abstract interpretation for relational logic. In: Proceedings of CSF, pp. 48\u201362. IEEE Computer Society (2014)","DOI":"10.1109\/CSF.2014.12"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-642-54792-8_15","volume-title":"Principles of Security and Trust","author":"MR Clarkson","year":"2014","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., S\u00e1nchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 265\u2013284. Springer, Heidelberg (2014). doi:\n10.1007\/978-3-642-54792-8_15"},{"issue":"6","key":"12_CR10","doi-asserted-by":"crossref","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."},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11513988_36","volume-title":"Computer Aided Verification","author":"M d\u2019Amorim","year":"2005","unstructured":"d\u2019Amorim, M., Ro\u015fu, G.: Efficient monitoring of \n            $$\\omega $$\n          -languages. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 364\u2013378. Springer, Heidelberg (2005). doi:\n10.1007\/11513988_36"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Devriese, D., Piessens, F.: Noninterference through secure multi-execution. In: Proceedings of SP, pp. 109\u2013124. IEEE Computer Society (2010)","DOI":"10.1109\/SP.2010.15"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-642-27940-9_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Dimitrova","year":"2012","unstructured":"Dimitrova, R., Finkbeiner, B., Kov\u00e1cs, M., Rabe, M.N., Seidl, H.: Model checking information flow in reactive systems. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 169\u2013185. Springer, Heidelberg (2012). doi:\n10.1007\/978-3-642-27940-9_12"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/978-3-642-34026-0_26","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change","author":"R Dimitrova","year":"2012","unstructured":"Dimitrova, R., Finkbeiner, B., Rabe, M.N.: Monitoring temporal information flow. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7609, pp. 342\u2013357. Springer, Heidelberg (2012). doi:\n10.1007\/978-3-642-34026-0_26"},{"key":"12_CR15","unstructured":"Finkbeiner, B., Hahn, C.: Deciding hyperproperties. In: Proceedings of CONCUR, LIPIcs, vol. 59, pp. 13:1\u201313:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2016)"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_29","volume-title":"Computer Aided Verification","author":"B Finkbeiner","year":"2017","unstructured":"Finkbeiner, B., Hahn, C., Stenger, M.: EAHyper: satisfiability, implication, and equivalence checking of hyperproperties. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427. Springer, Cham (2017). doi:\n10.1007\/978-3-319-63390-9_29"},{"key":"12_CR17","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\n            $$^*$$\n          . In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 30\u201348. Springer, Cham (2015). doi:\n10.1007\/978-3-319-21690-4_3"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/978-3-540-77505-8_7","volume-title":"Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues","author":"G Guernic Le","year":"2007","unstructured":"Le Guernic, G., Banerjee, A., Jensen, T., Schmidt, D.A.: Automata-based confidentiality monitoring. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 75\u201389. Springer, Heidelberg (2007). doi:\n10.1007\/978-3-540-77505-8_7"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-642-28166-2_6","volume-title":"Engineering Secure Software and Systems","author":"M Kov\u00e1cs","year":"2012","unstructured":"Kov\u00e1cs, M., Seidl, H.: Runtime enforcement of information flow security in tree manipulating processes. In: Barthe, G., Livshits, B., Scandariato, R. (eds.) ESSoS 2012. LNCS, vol. 7159, pp. 46\u201359. Springer, Heidelberg (2012). doi:\n10.1007\/978-3-642-28166-2_6"},{"key":"12_CR20","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems - Safety","author":"Z Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems - Safety. Springer, New York (1995)"},{"issue":"1","key":"12_CR21","doi-asserted-by":"crossref","first-page":"37","DOI":"10.3233\/JCS-1992-1103","volume":"1","author":"J McLean","year":"1992","unstructured":"McLean, J.: Proving noninterference and functional correctness using traces. J. Comput. Secur. 1(1), 37\u201358 (1992)","journal-title":"J. Comput. Secur."},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of FOCS, pp. 46\u201357. IEEE Computer Society (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"12_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/11813040_38","volume-title":"FM 2006: Formal Methods","author":"A Pnueli","year":"2006","unstructured":"Pnueli, A., Zaks, A.: PSL model checking and run-time verification via testers. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 573\u2013586. Springer, Heidelberg (2006). doi:\n10.1007\/11813040_38"},{"key":"12_CR24","doi-asserted-by":"crossref","unstructured":"Roscoe, A.W.: CSP and determinism in security modelling. In: Proceedings of SP, pp. 114\u2013127. IEEE Computer Society (1995)","DOI":"10.1109\/SECPRI.1995.398927"},{"issue":"1","key":"12_CR25","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A Sabelfeld","year":"2003","unstructured":"Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE J. Sel. Areas Commun. 21(1), 5\u201319 (2003)","journal-title":"IEEE J. Sel. Areas Commun."},{"key":"12_CR26","doi-asserted-by":"crossref","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. In: Proceedings of STOC, pp. 159\u2013168. ACM (1982)","DOI":"10.1145\/800070.802189"},{"key":"12_CR27","doi-asserted-by":"crossref","unstructured":"Suh, G.E., Lee, J.W., Zhang, D., Devadas, S.: Secure program execution via dynamic information flow tracking. In: Proceedings of ASPLOS, pp. 85\u201396. ACM (2004)","DOI":"10.1145\/1024393.1024404"},{"issue":"3","key":"12_CR28","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1007\/s10703-011-0139-8","volume":"41","author":"D Tabakov","year":"2012","unstructured":"Tabakov, D., Rozier, K.Y., Vardi, M.Y.: Optimized temporal monitors for systemc. Formal Methods Syst. Des. 41(3), 236\u2013268 (2012)","journal-title":"Formal Methods Syst. Des."},{"key":"12_CR29","doi-asserted-by":"crossref","unstructured":"Vanhoef, M., Groef, W.D., Devriese, D., Piessens, F., Rezk, T.: Stateful declassification policies for event-driven programs. In: Proceedings of CSF, pp. 293\u2013307. IEEE Computer Society (2014)","DOI":"10.1109\/CSF.2014.28"},{"key":"12_CR30","doi-asserted-by":"crossref","unstructured":"Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: Proceedings of CSF, p. 29. IEEE Computer Society (2003)","DOI":"10.1109\/CSFW.2003.1212703"}],"container-title":["Lecture Notes in Computer Science","Runtime Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-67531-2_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,9,5]],"date-time":"2017-09-05T09:36:49Z","timestamp":1504604209000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-67531-2_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319675305","9783319675312"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-67531-2_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}