{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,21]],"date-time":"2026-05-21T19:44:51Z","timestamp":1779392691178,"version":"3.53.1"},"reference-count":38,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2019,6,25]],"date-time":"2019-06-25T00:00:00Z","timestamp":1561420800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2019,6,25]],"date-time":"2019-06-25T00:00:00Z","timestamp":1561420800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["683300"],"award-info":[{"award-number":["683300"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["CRC 1223"],"award-info":[{"award-number":["CRC 1223"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["CRC 248"],"award-info":[{"award-number":["CRC 248"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2019,11]]},"DOI":"10.1007\/s10703-019-00334-z","type":"journal-article","created":{"date-parts":[[2019,6,25]],"date-time":"2019-06-25T12:57:01Z","timestamp":1561467421000},"page":"336-363","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":42,"title":["Monitoring hyperproperties"],"prefix":"10.1007","volume":"54","author":[{"given":"Bernd","family":"Finkbeiner","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1243-4880","authenticated-orcid":false,"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":[[2019,6,25]]},"reference":[{"key":"334_CR1","doi-asserted-by":"crossref","unstructured":"Agrawal S, Bonakdarpour B (2016) Runtime verification of k-safety hyperproperties in HyperLTL. In: Proceedings of CSF, IEEE Computer Society, pp 239\u2013252","DOI":"10.1109\/CSF.2016.24"},{"key":"334_CR2","doi-asserted-by":"crossref","unstructured":"Askarov A, Sabelfeld A (2009) Tight enforcement of information-release policies for dynamic languages. In: Proceedings of CSF, IEEE Computer Society, pp 43\u201359","DOI":"10.1109\/CSF.2009.22"},{"key":"334_CR3","doi-asserted-by":"crossref","unstructured":"Austin TH, Flanagan C (2010) Permissive dynamic information flow analysis. In: Proceedings of PLAS, ACM, p 3","DOI":"10.1145\/1814217.1814220"},{"key":"334_CR4","doi-asserted-by":"crossref","unstructured":"Barringer H, Falcone Y, Havelund K, Reger G, Rydeheard DE (2012) Quantified event automata: towards expressive and efficient runtime monitors. In: Proceedings of FM, volume 7436 of LNCS, Springer, pp 68\u201384","DOI":"10.1007\/978-3-642-32759-9_9"},{"key":"334_CR5","unstructured":"Bauer A (2010) Monitorability of omega-regular languages. In: CoRR. \narXiv:1006.3638"},{"key":"334_CR6","doi-asserted-by":"crossref","unstructured":"Bichhawat A, Rajani V, Garg D, Hammer C (2014) Information flow control in WebKit\u2019s javascript bytecode. In: Proceedings of POST, volume 8414 of LNCS, Springer, Berlin, pp 159\u2013178","DOI":"10.1007\/978-3-642-54792-8_9"},{"key":"334_CR7","doi-asserted-by":"crossref","unstructured":"Bonakdarpour B, Finkbeiner B (2018) The complexity of monitoring hyperproperties. In: Proceedings of CSF, IEEE Computer Society, pp 162\u2013174","DOI":"10.1109\/CSF.2018.00019"},{"key":"334_CR8","doi-asserted-by":"crossref","unstructured":"Bonakdarpour B, S\u00e1nchez C, Schneider G (2018) Monitoring hyperproperties by combining static analysis and runtime verification. In: Proceedings of II, volume 11245 of LNCS, Springer, pp 8\u201327","DOI":"10.1007\/978-3-030-03421-4_2"},{"key":"334_CR9","doi-asserted-by":"crossref","unstructured":"Brett N, Siddique U, Bonakdarpour B (2017) Rewriting-based runtime verification for alternation-free HyperLTL. In: Proceedings of TACAS, volume 10206 of LNCS, pp 77\u201393","DOI":"10.1007\/978-3-662-54580-5_5"},{"key":"334_CR10","doi-asserted-by":"crossref","unstructured":"Chen F, Rosu G (2009) Parametric trace slicing and monitoring. In: Proceedings of TACAS, volume 5505 of LNCS, Springer, pp 246\u2013261","DOI":"10.1007\/978-3-642-00768-2_23"},{"key":"334_CR11","doi-asserted-by":"crossref","unstructured":"Chudnov A, Kuan G, Naumann DA (2014) Information flow monitoring as abstract interpretation for relational logic. In: Proceedings of CSF, IEEE Computer Society, pp 48\u201362","DOI":"10.1109\/CSF.2014.12"},{"key":"334_CR12","doi-asserted-by":"crossref","unstructured":"Clarkson MR, Finkbeiner B, Koleini M, Micinski KK, Rabe MN, S\u00e1nchez C (2014) Temporal logics for hyperproperties. In: Proceedings of POST, volume 8414 of LNCS, Springer, pp 265\u2013284","DOI":"10.1007\/978-3-642-54792-8_15"},{"issue":"6","key":"334_CR13","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"MR Clarkson","year":"2010","unstructured":"Clarkson MR, Schneider FB (2010) Hyperproperties. J Comput Secur 18(6):1157\u20131210","journal-title":"J Comput Secur"},{"key":"334_CR14","unstructured":"d\u2019Amorim M, Rosu G (2005) Efficient monitoring of omega-languages. In: Proceedings of CAV, volume 3576 of LNCS, Springer, pp 364\u2013378"},{"key":"334_CR15","unstructured":"Devriese D, Piessens F (2010) Frank noninterference through secure multi-execution. In: Proceedings of SP, IEEE Computer Society, pp 109\u2013124"},{"key":"334_CR16","doi-asserted-by":"crossref","unstructured":"Dimitrova R, Finkbeiner B, Kov\u00e1cs M, Rabe MN, Seidl H (2012) Model checking information flow in reactive systems. In: Proceedings of VMCAI, volume 7148 of LNCS, Springer, pp 169\u2013185","DOI":"10.1007\/978-3-642-27940-9_12"},{"key":"334_CR17","doi-asserted-by":"crossref","unstructured":"Dimitrova R, Finkbeiner B, Rabe MN (2012) Monitoring temporal information flow. In: Proceedings of ISoLA, volume 7609 of LNCS, Springer, pp 342\u2013357","DOI":"10.1007\/978-3-642-34026-0_26"},{"key":"334_CR18","unstructured":"Finkbeiner B, Hahn C (2016) Deciding hyperproperties. In: Proceedings of CONCUR, volume 59 of LIPIcs, Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, pp 13:1\u201313:14"},{"key":"334_CR19","doi-asserted-by":"publisher","first-page":"564","DOI":"10.1007\/978-3-319-63390-9_29","volume-title":"Computer Aided Verification","author":"Bernd Finkbeiner","year":"2017","unstructured":"Finkbeiner B, Hahn C, Stenger M (2017) EAHyper: satisfiability, implication, and equivalence checking of hyperproperties. In: Proceedings of CAV, volume 10427 of LNCS, Springer, Berlin, pp 564\u2013570"},{"key":"334_CR20","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-319-67531-2_12","volume-title":"Runtime Verification","author":"Bernd Finkbeiner","year":"2017","unstructured":"Finkbeiner B, Hahn C, Stenger M, Tentrup L (2017) Monitoring hyperproperties. In: Proceedings of RV, volume 10548 of LNCS, Springer, pp 190\u2013207"},{"key":"334_CR21","unstructured":"Finkbeiner B, Hahn C, Stenger M, Tentrup L (2018) Rvhyper: a runtime verification tool for temporal hyperproperties. In: Proceedings of TACAS, volume 10806 of LNCS, Springer, pp 194\u2013200"},{"key":"334_CR22","doi-asserted-by":"crossref","unstructured":"Finkbeiner B, Rabe MN, S\u00e1nchez C (2015) Algorithms for model checking HyperLTL and HyperCTL*. In: Proceedings of CAV, volume 9206 of LNCS, Springer, pp 30\u201348","DOI":"10.1007\/978-3-319-21690-4_3"},{"issue":"2","key":"334_CR23","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1023\/B:FORM.0000017718.28096.48","volume":"24","author":"B Finkbeiner","year":"2004","unstructured":"Finkbeiner B, Sipma H (2004) Checking finite traces using alternating automata. Form Method Syst Des 24(2):101\u2013127","journal-title":"Form Method Syst Des"},{"key":"334_CR24","unstructured":"Le Guernic G, Banerjee A, Jensen TP, Schmidt DA (2006) Automata-based confidentiality monitoring. In: Proceedings of ASIAN, volume 4435 of LNCS, Springer, pp 75\u201389"},{"key":"334_CR25","doi-asserted-by":"crossref","unstructured":"Kov\u00e1cs M, Seidl H (2012) Runtime enforcement of information flow security in tree manipulating processes. In: Proceedings of ESSoS, volume 7159 of LNCS, Springer, pp 46\u201359","DOI":"10.1007\/978-3-642-28166-2_6"},{"key":"334_CR26","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal verification of reactive systems\u2013safety","author":"Z Manna","year":"1995","unstructured":"Manna Z, Pnueli A (1995) Temporal verification of reactive systems\u2013safety. Springer, Berlin"},{"issue":"1","key":"334_CR27","doi-asserted-by":"publisher","first-page":"37","DOI":"10.3233\/JCS-1992-1103","volume":"1","author":"J McLean","year":"1992","unstructured":"McLean J (1992) Proving noninterference and functional correctness using traces. J Comput Secur 1(1):37\u201358","journal-title":"J Comput Secur"},{"key":"334_CR28","doi-asserted-by":"crossref","unstructured":"McLean J (1994) A general theory of composition for trace sets closed under selective interleaving functions. In: 1994 IEEE computer society symposium on research in security and privacy, Oakland, CA, USA, May 16\u201318, 1994, IEEE Computer Society, pp 79\u201393","DOI":"10.1109\/RISP.1994.296590"},{"key":"334_CR29","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: Proceedings of FOCS, IEEE Computer Society, pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"334_CR30","doi-asserted-by":"crossref","unstructured":"Pnueli A, Zaks A (2006) PSL model checking and run-time verification via testers. In: Proceedings of FM, volume 4085 of LNCS, Springer, pp 573\u2013586","DOI":"10.1007\/11813040_38"},{"key":"334_CR31","doi-asserted-by":"crossref","unstructured":"Roscoe AW (1995) CSP and determinism in security modelling. In: Proceedings of SP, IEEE Computer Society, pp 114\u2013127","DOI":"10.1109\/SECPRI.1995.398927"},{"issue":"1","key":"334_CR32","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1109\/JSAC.2002.806121","volume":"21","author":"A Sabelfeld","year":"2003","unstructured":"Sabelfeld A, Myers AC (2003) Language-based information-flow security. IEEE J Sel Areas Commun 21(1):5\u201319","journal-title":"IEEE J Sel Areas Commun"},{"key":"334_CR33","unstructured":"Sistla AP, Clarke EM (1982) The complexity of propositional linear temporal logics. In: Proceedings of STOC, ACM, pp 159\u2013168"},{"key":"334_CR34","doi-asserted-by":"crossref","unstructured":"Suh GE, Lee JW, Zhang D, Devadas S (2004) Secure program execution via dynamic information flow tracking. In: Proceedings of ASPLOS, ACM, pp 85\u201396","DOI":"10.1145\/1024393.1024404"},{"issue":"3","key":"334_CR35","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/s10703-011-0139-8","volume":"41","author":"D Tabakov","year":"2012","unstructured":"Tabakov D, Rozier KY, Vardi MY (2012) Optimized temporal monitors for system C. Form Methods Syst Des 41(3):236\u2013268","journal-title":"Form Methods Syst Des"},{"key":"334_CR36","doi-asserted-by":"crossref","unstructured":"Vanhoef M, De Groef W, Devriese D, Piessens F, Rezk T (2014) Stateful declassification policies for event-driven programs. In: Proceedings of CSF, IEEE Computer Society, pp 293\u2013307","DOI":"10.1109\/CSF.2014.28"},{"key":"334_CR37","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Logics for Concurrency","author":"Moshe Y. Vardi","year":"1996","unstructured":"Vardi MY (1995) An automata-theoretic approach to linear temporal logic. In: Logics for concurrency \u2013structure versus automata (8th Banff Higher Order Workshop, Banff, Canada, August 27\u2013September 3, 1995, Proceedings), volume 1043 of LNCS, Springer, pp 238\u2013266"},{"key":"334_CR38","doi-asserted-by":"crossref","unstructured":"Zdancewic S, Myers AC (2003) Observational determinism for concurrent program security. In: Proceedings of CSF, IEEE Computer Society, p 29","DOI":"10.1109\/CSFW.2003.1212703"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-019-00334-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-019-00334-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-019-00334-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,23]],"date-time":"2020-06-23T23:12:58Z","timestamp":1592953978000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-019-00334-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6,25]]},"references-count":38,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2019,11]]}},"alternative-id":["334"],"URL":"https:\/\/doi.org\/10.1007\/s10703-019-00334-z","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,6,25]]},"assertion":[{"value":"25 June 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}