{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,20]],"date-time":"2025-07-20T03:54:45Z","timestamp":1752983685254,"version":"3.40.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031711763"},{"type":"electronic","value":"9783031711770"}],"license":[{"start":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T00:00:00Z","timestamp":1726185600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T00:00:00Z","timestamp":1726185600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Hyperproperties relate multiple executions of a system and are commonly used to specify security and information-flow policies. While many verification approaches for hyperproperties exist, providing a convincing <jats:italic>certificate<\/jats:italic> that the system satisfies a given property is still a major challenge. In this paper, we propose <jats:italic>strategies<\/jats:italic> as a suitable form of certificate for hyperproperties specified in a fragment of the temporal logic HyperLTL. Concretely, we interpret the verification of a HyperLTL property as a game between universal and existential quantification, allowing us to leverage strategies for the existential quantifiers as certificates. We present , a browser-based visualization tool that lets users interactively explore an (automatically synthesized) witness strategy by taking control over universally quantified executions.<\/jats:p>","DOI":"10.1007\/978-3-031-71177-0_5","type":"book-chapter","created":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T06:10:51Z","timestamp":1726121451000},"page":"67-75","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Visualizing Game-Based Certificates for\u00a0Hyperproperty Verification"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6234-5651","authenticated-orcid":false,"given":"Raven","family":"Beutner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4280-8441","authenticated-orcid":false,"given":"Bernd","family":"Finkbeiner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-2331-4049","authenticated-orcid":false,"given":"Angelina","family":"G\u00f6bl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,9,13]]},"reference":[{"issue":"2","key":"5_CR1","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M Abadi","year":"1991","unstructured":"Abadi, M., Lamport, L.: The existence of refinement mappings. Theor. Comput. Sci. 82(2), 253\u2013284 (1991). https:\/\/doi.org\/10.1016\/0304-3975(91)90224-P","journal-title":"Theor. Comput. Sci."},{"key":"5_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000193","author":"G Barthe","year":"2011","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure information flow by self-composition. Math. Struct. Comput. Sci. (2011). https:\/\/doi.org\/10.1017\/S0960129511000193","journal-title":"Math. Struct. Comput. Sci."},{"key":"5_CR3","doi-asserted-by":"publisher","unstructured":"Bartocci, E., Henzinger, T.A., Nickovic, D., da\u00a0Costa, A.O.: Hypernode automata. In: International Conference on Concurrency Theory, CONCUR 2023 (2023). https:\/\/doi.org\/10.4230\/LIPICS.CONCUR.2023.21","DOI":"10.4230\/LIPICS.CONCUR.2023.21"},{"key":"5_CR4","doi-asserted-by":"publisher","unstructured":"Beer, I., Ben-David, S., Chockler, H., Orni, A., Trefler, R.J.: Explaining counterexamples using causality. In: International Conference on Computer Aided Verification, CAV 2009 (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_11","DOI":"10.1007\/978-3-642-02658-4_11"},{"key":"5_CR5","doi-asserted-by":"publisher","DOI":"10.1145\/3375633","author":"I Beschastnikh","year":"2020","unstructured":"Beschastnikh, I., Liu, P., Xing, A., Wang, P., Brun, Y., Ernst, M.D.: Visualizing distributed system executions. ACM Trans. Softw. Eng. Methodol. (2020). https:\/\/doi.org\/10.1145\/3375633","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"5_CR6","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B.: Prophecy variables for hyperproperty verification. In: Computer Security Foundations Symposium, CSF 2022 (2022). https:\/\/doi.org\/10.1109\/CSF54842.2022.9919658","DOI":"10.1109\/CSF54842.2022.9919658"},{"key":"5_CR7","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B.: Software verification of hyperproperties beyond k-safety. In: International Conference on Computer Aided Verification, CAV 2022 (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_17","DOI":"10.1007\/978-3-031-13185-1_17"},{"key":"5_CR8","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B.: AutoHyper: explicit-state model checking for HyperLTL. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2023 (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_8","DOI":"10.1007\/978-3-031-30823-9_8"},{"key":"5_CR9","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B.: Non-deterministic planning for hyperproperty verification. In: International Conference on Automated Planning and Scheduling, ICAPS 2024 (2024). https:\/\/doi.org\/10.1609\/ICAPS.V34I1.31457","DOI":"10.1609\/ICAPS.V34I1.31457"},{"key":"5_CR10","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B., Frenkel, H., Metzger, N.: Second-order hyperproperties. In: International Conference on Computer Aided Verification, CAV 2023 (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_15","DOI":"10.1007\/978-3-031-37703-7_15"},{"key":"5_CR11","doi-asserted-by":"publisher","unstructured":"Beutner, R., Finkbeiner, B., G\u00f6bl, A.: HyGaViz: visualizing game-based certificates for hyperproperty verification (2024). https:\/\/doi.org\/10.5281\/zenodo.12206584","DOI":"10.5281\/zenodo.12206584"},{"key":"5_CR12","doi-asserted-by":"publisher","unstructured":"Biewer, S., et al.: Conformance relations and hyperproperties for doping detection in time and space. Log. Methods Comput. Sci. 18, 14 (2022). https:\/\/doi.org\/10.46298\/lmcs-18(1:14)2022","DOI":"10.46298\/lmcs-18(1:14)2022"},{"key":"5_CR13","doi-asserted-by":"publisher","unstructured":"Bolton, M.L., Bass, E.J.: Using task analytic models to visualize model checker counterexamples. In: International Conference on Systems, Man and Cybernetics, SMC 2010 (2010). https:\/\/doi.org\/10.1109\/ICSMC.2010.5641711","DOI":"10.1109\/ICSMC.2010.5641711"},{"key":"5_CR14","doi-asserted-by":"publisher","unstructured":"Bozzelli, L., Maubert, B., Pinchinat, S.: Unifying hyper and epistemic temporal logics. In: International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2015 (2015). https:\/\/doi.org\/10.1007\/978-3-662-46678-0_11","DOI":"10.1007\/978-3-662-46678-0_11"},{"key":"5_CR15","doi-asserted-by":"publisher","DOI":"10.1145\/2240236.2240262","author":"S Chaudhuri","year":"2012","unstructured":"Chaudhuri, S., Gulwani, S., Lublinerman, R.: Continuity and robustness of programs. Commun. ACM (2012). https:\/\/doi.org\/10.1145\/2240236.2240262","journal-title":"Commun. ACM"},{"key":"5_CR16","doi-asserted-by":"publisher","unstructured":"Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., S\u00e1nchez, C.: Temporal logics for hyperproperties. In: International Conference om Principles of Security and Trust, POST 2014 (2014). https:\/\/doi.org\/10.1007\/978-3-642-54792-8_15","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"5_CR17","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0393","author":"MR Clarkson","year":"2010","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. (2010). https:\/\/doi.org\/10.3233\/JCS-2009-0393","journal-title":"J. Comput. Secur."},{"key":"5_CR18","doi-asserted-by":"publisher","unstructured":"Coenen, N., et al.: Explaining hyperproperty violations. In: International Conference on Computer Aided Verification, CAV 2022 (2022). https:\/\/doi.org\/10.1007\/978-3-031-13185-1_20","DOI":"10.1007\/978-3-031-13185-1_20"},{"key":"5_CR19","doi-asserted-by":"publisher","unstructured":"Coenen, N., Finkbeiner, B., Frenkel, H., Hahn, C., Metzger, N., Siber, J.: Temporal causality in reactive systems. In: International Symposium on Automated Technology for Verification and Analysis, ATVA 2022 (2022). https:\/\/doi.org\/10.1007\/978-3-031-19992-9_13","DOI":"10.1007\/978-3-031-19992-9_13"},{"key":"5_CR20","doi-asserted-by":"publisher","unstructured":"Coenen, N., Finkbeiner, B., S\u00e1nchez, C., Tentrup, L.: Verifying hyperliveness. In: International Conference on Computer Aided Verification, CAV 2019 (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_7","DOI":"10.1007\/978-3-030-25540-4_7"},{"key":"5_CR21","doi-asserted-by":"publisher","unstructured":"van Dijk, T.: Oink: an implementation and evaluation of modern parity game solvers. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2018 (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_16","DOI":"10.1007\/978-3-319-89960-2_16"},{"key":"5_CR22","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., et al.: From spot 2.0 to spot 2.10: what\u2019s new? In: International Conference on Computer Aided Verification, CAV 2022 (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_9","DOI":"10.1007\/978-3-031-13188-2_9"},{"key":"5_CR23","doi-asserted-by":"publisher","DOI":"10.1145\/3610392.3610394","author":"B Finkbeiner","year":"2023","unstructured":"Finkbeiner, B.: Logics and algorithms for hyperproperties. ACM SIGLOG News (2023). https:\/\/doi.org\/10.1145\/3610392.3610394","journal-title":"ACM SIGLOG News"},{"key":"5_CR24","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Rabe, M.N., S\u00e1nchez, C.: Algorithms for model checking HyperLTL and HyperCTL$$^*$$. In: International Conference on Computer Aided Verification, CAV 2015 (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_3","DOI":"10.1007\/978-3-319-21690-4_3"},{"key":"5_CR25","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Siber, J.: Counterfactuals modulo temporal logics. In: International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR 2023 (2023). https:\/\/doi.org\/10.29007\/QTW7","DOI":"10.29007\/QTW7"},{"key":"5_CR26","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1093\/BIOINFORMATICS\/BTV557","volume":"32","author":"M Franz","year":"2016","unstructured":"Franz, M., Lopes, C.T., Huck, G., Dong, Y., S\u00fcmer, S.O., Bader, G.D.: Cytoscape.js: a graph theory library for visualisation and analysis. Bioinformatics 32, 309\u2013311 (2016). https:\/\/doi.org\/10.1093\/BIOINFORMATICS\/BTV557","journal-title":"Bioinformatics"},{"key":"5_CR27","doi-asserted-by":"publisher","unstructured":"Griggio, A., Roveri, M., Tonetta, S.: Certifying proofs for LTL model checking. In: Formal Methods in Computer Aided Design, FMCAD 2018 (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8603022","DOI":"10.23919\/FMCAD.2018.8603022"},{"key":"5_CR28","doi-asserted-by":"publisher","unstructured":"Groce, A., Kroening, D., Lerda, F.: Understanding counterexamples with explain. In: International Conference on Computer Aided Verification, CAV 2004 (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_35","DOI":"10.1007\/978-3-540-27813-9_35"},{"key":"5_CR29","doi-asserted-by":"publisher","DOI":"10.1109\/TVCG.2021.3114866","author":"T Horak","year":"2022","unstructured":"Horak, T., et al.: Visual analysis of hyperproperties for understanding model checking results. IEEE Trans. Vis. Comput. Graph. (2022). https:\/\/doi.org\/10.1109\/TVCG.2021.3114866","journal-title":"IEEE Trans. Vis. Comput. Graph."},{"key":"5_CR30","doi-asserted-by":"publisher","unstructured":"Hsu, T., S\u00e1nchez, C., Bonakdarpour, B.: Bounded model checking for hyperproperties. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2021 (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_6","DOI":"10.1007\/978-3-030-72016-2_6"},{"key":"5_CR31","doi-asserted-by":"publisher","unstructured":"Jerding, D.F., Stasko, J.T., Ball, T.: Visualizing interactions in program executions. In: International Conference on Software Engineering, ICSE 1997 (1997). https:\/\/doi.org\/10.1145\/253228.253356","DOI":"10.1145\/253228.253356"},{"key":"5_CR32","doi-asserted-by":"publisher","unstructured":"Kasenberg, D., Thielstrom, R., Scheutz, M.: Generating explanations for temporal logic planner decisions. In: International Conference on Automated Planning and Scheduling, ICAPS 2020 (2020). https:\/\/doi.org\/10.1609\/icaps.v30i1.6740","DOI":"10.1609\/icaps.v30i1.6740"},{"key":"5_CR33","doi-asserted-by":"publisher","unstructured":"McLean, J.: A general theory of composition for trace sets closed under selective interleaving functions. In: Symposium on Security and Privacy, SP 1994 (1994). https:\/\/doi.org\/10.1109\/RISP.1994.296590","DOI":"10.1109\/RISP.1994.296590"},{"key":"5_CR34","doi-asserted-by":"publisher","unstructured":"Moreno, A., Myller, N., Sutinen, E., Ben-Ari, M.: Visualizing programs with Jeliot 3. In: Conference on Advanced Visual Interfaces, AVI 2004 (2004). https:\/\/doi.org\/10.1145\/989863.989928","DOI":"10.1145\/989863.989928"},{"key":"5_CR35","unstructured":"Rabe, M.N.: A temporal logic approach to information-flow control. Ph. D. thesis, Saarland University (2016)"},{"key":"5_CR36","first-page":"15","volume":"7","author":"T Rajala","year":"2008","unstructured":"Rajala, T., Laakso, M., Kaila, E., Salakoski, T.: Effectiveness of program visualization: a case study with the ViLLE tool. J. Inf. Technol. Educ. Innov. Pract. 7, 15 (2008)","journal-title":"J. Inf. Technol. Educ. Innov. Pract."},{"key":"5_CR37","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1109\/MIC.2010.145","volume":"14","author":"S Tilkov","year":"2010","unstructured":"Tilkov, S., Vinoski, S.: Node.js: using javascript to build high-performance network programs. IEEE Internet Comput. 14, 80\u201383 (2010). https:\/\/doi.org\/10.1109\/MIC.2010.145","journal-title":"IEEE Internet Comput."},{"key":"5_CR38","doi-asserted-by":"publisher","unstructured":"Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: Computer Security Foundations Workshop CSFW 2003 (2003). https:\/\/doi.org\/10.1109\/CSFW.2003.1212703","DOI":"10.1109\/CSFW.2003.1212703"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71177-0_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T06:11:45Z","timestamp":1726121505000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71177-0_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,13]]},"ISBN":["9783031711763","9783031711770"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71177-0_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,9,13]]},"assertion":[{"value":"13 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}