{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,24]],"date-time":"2026-02-24T13:37:59Z","timestamp":1771940279131,"version":"3.50.1"},"publisher-location":"Cham","reference-count":70,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031131844","type":"print"},{"value":"9783031131851","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,7]],"date-time":"2022-08-07T00:00:00Z","timestamp":1659830400000},"content-version":"vor","delay-in-days":218,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Hyperproperties relate multiple computation traces to each other. Model checkers for hyperproperties thus return, in case a system model violates the specification, a set of traces as a counterexample. Fixing the erroneous relations between traces in the system that led to the counterexample is a difficult manual effort that highly benefits from additional explanations. In this paper, we present an explanation method for counterexamples to hyperproperties described in the specification logic HyperLTL. We extend Halpern and Pearl\u2019s definition of actual causality to sets of traces witnessing the violation of a HyperLTL formula, which allows us to identify the events that caused the violation. We report on the implementation of our method and show that it significantly improves on previous approaches for analyzing counterexamples returned by HyperLTL model checkers.<\/jats:p>","DOI":"10.1007\/978-3-031-13185-1_20","type":"book-chapter","created":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T19:29:09Z","timestamp":1659814149000},"page":"407-429","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Explaining Hyperproperty Violations"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2066-1511","authenticated-orcid":false,"given":"Norine","family":"Coenen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2176-876X","authenticated-orcid":false,"given":"Raimund","family":"Dachselt","sequence":"additional","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\/0000-0002-3566-0338","authenticated-orcid":false,"given":"Hadar","family":"Frenkel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1243-4880","authenticated-orcid":false,"given":"Christopher","family":"Hahn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2896-5886","authenticated-orcid":false,"given":"Tom","family":"Horak","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3184-6335","authenticated-orcid":false,"given":"Niklas","family":"Metzger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0842-0029","authenticated-orcid":false,"given":"Julian","family":"Siber","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,8,7]]},"reference":[{"key":"20_CR1","unstructured":"Log4j vulnerabilities. https:\/\/logging.apache.org\/log4j\/2.x\/security.html"},{"key":"20_CR2","doi-asserted-by":"publisher","unstructured":"Agrawal, S., Bonakdarpour, B.: Runtime verification of k-safety hyperproperties in hyperltl. In: CSF 2016. https:\/\/doi.org\/10.1109\/CSF.2016.24","DOI":"10.1109\/CSF.2016.24"},{"key":"20_CR3","unstructured":"Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: IJCAI 2009. http:\/\/ijcai.org\/Proceedings\/09\/Papers\/074.pdf"},{"key":"20_CR4","doi-asserted-by":"publisher","unstructured":"Baier, C., et al.: From verification to causality-based explications. In: ICALP 2021. https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2021.1","DOI":"10.4230\/LIPIcs.ICALP.2021.1"},{"key":"20_CR5","doi-asserted-by":"publisher","unstructured":"Ball, T., Naik, M., Rajamani, S.K.: From symptom to cause: localizing errors in counterexample traces. In: POPL 2003. https:\/\/doi.org\/10.1145\/604131.604140","DOI":"10.1145\/604131.604140"},{"issue":"6","key":"20_CR6","doi-asserted-by":"publisher","first-page":"1207","DOI":"10.1017\/S0960129511000193","volume":"21","author":"G Barthe","year":"2011","unstructured":"Barthe, G., D\u2019Argenio, P.R., Rezk, T.: Secure information flow by self-composition. Math. Struct. Comput. Sci. 21(6), 1207\u20131252 (2011)","journal-title":"Math. Struct. Comput. Sci."},{"key":"20_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/978-3-642-02658-4_11","volume-title":"Computer Aided Verification","author":"I Beer","year":"2009","unstructured":"Beer, I., Ben-David, S., Chockler, H., Orni, A., Trefler, R.: Explaining counterexamples using causality. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 94\u2013108. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_11"},{"key":"20_CR8","unstructured":"Biere, A.: The AIGER And-Inverter Graph (AIG) format version 20071012. Technical report 07\/1, Inst. f. Form. Model. u. Verifikation, Johannes Kepler University (2007)"},{"key":"20_CR9","doi-asserted-by":"publisher","unstructured":"Bochot, T., Virelizier, P., Waeselynck, H., Wiels, V.: Paths to property violation: a structural approach for analyzing counter-examples. In: HASE 2010. https:\/\/doi.org\/10.1109\/HASE.2010.15","DOI":"10.1109\/HASE.2010.15"},{"key":"20_CR10","doi-asserted-by":"publisher","unstructured":"Bonakdarpour, B., Finkbeiner, B.: The complexity of monitoring hyperproperties. In: CSF 2018. https:\/\/doi.org\/10.1109\/CSF.2018.00019","DOI":"10.1109\/CSF.2018.00019"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/978-3-030-31784-3_25","volume-title":"Automated Technology for Verification and Analysis","author":"B Bonakdarpour","year":"2019","unstructured":"Bonakdarpour, B., Finkbeiner, B.: Program repair for hyperproperties. In: Chen, Y.-F., Cheng, C.-H., Esparza, J. (eds.) ATVA 2019. LNCS, vol. 11781, pp. 423\u2013441. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_25"},{"key":"20_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","volume-title":"Computer Aided Verification","author":"R Brayton","year":"2010","unstructured":"Brayton, R., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 24\u201340. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_5"},{"key":"20_CR13","doi-asserted-by":"publisher","unstructured":"Caltais, G., Guetlein, S.L., Leue, S.: Causality for general LTL-definable properties. In: CREST@ETAPS 2018. https:\/\/doi.org\/10.4204\/EPTCS.286.1","DOI":"10.4204\/EPTCS.286.1"},{"issue":"6","key":"20_CR14","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1109\/TSE.2004.22","volume":"30","author":"S Chaki","year":"2004","unstructured":"Chaki, S., Clarke, E.M., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. IEEE Trans. Softw. Eng. 30(6), 388\u2013402 (2004)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"20_CR15","doi-asserted-by":"publisher","unstructured":"Chaki, S., Groce, A., Strichman, O.: Explaining abstract counterexamples. In: ACM SIGSOFT Foundations of Software Engineering (2004). https:\/\/doi.org\/10.1145\/1029894.1029908","DOI":"10.1145\/1029894.1029908"},{"key":"20_CR16","doi-asserted-by":"publisher","unstructured":"Chockler, H., Halpern, J.Y., Kupferman, O.: What causes a system to satisfy a specification? ACM Trans. Comput. Log. 9(3), 20:1\u201320:26 (2008). https:\/\/doi.org\/10.1145\/1352582.1352588","DOI":"10.1145\/1352582.1352588"},{"issue":"1","key":"20_CR17","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"EM Clarke","year":"2001","unstructured":"Clarke, E.M., Biere, A., Raimi, R., Zhu, Y.: Bounded model checking using satisfiability solving. Formal Methods Syst. Des. 19(1), 7\u201334 (2001)","journal-title":"Formal Methods Syst. Des."},{"key":"20_CR18","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logics of Programs, Workshop, Yorktown Heights, New York, USA, May 1981. https:\/\/doi.org\/10.1007\/BFb0025774","DOI":"10.1007\/BFb0025774"},{"key":"20_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15"},{"key":"20_CR20","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). https:\/\/doi.org\/10.1007\/978-3-642-54792-8_15"},{"key":"20_CR21","doi-asserted-by":"publisher","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157\u20131210 (2010). https:\/\/doi.org\/10.3233\/JCS-2009-0393","DOI":"10.3233\/JCS-2009-0393"},{"key":"20_CR22","doi-asserted-by":"publisher","unstructured":"Coenen, N., et al.: Explaining hyperproperty violations. CoRR (2022). https:\/\/doi.org\/10.48550\/ARXIV.2206.02074, full version with appendix","DOI":"10.48550\/ARXIV.2206.02074"},{"key":"20_CR23","doi-asserted-by":"publisher","unstructured":"Coenen, N., Finkbeiner, B., Hahn, C., Hofmann, J.: The hierarchy of hyperlogics. In: LICS 2019. https:\/\/doi.org\/10.1109\/LICS.2019.8785713","DOI":"10.1109\/LICS.2019.8785713"},{"key":"20_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-030-25540-4_7","volume-title":"Computer Aided Verification","author":"N Coenen","year":"2019","unstructured":"Coenen, N., Finkbeiner, B., S\u00e1nchez, C., Tentrup, L.: Verifying hyperliveness. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 121\u2013139. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_7"},{"key":"20_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-662-54434-1_4","volume-title":"Programming Languages and Systems","author":"PR D\u2019Argenio","year":"2017","unstructured":"D\u2019Argenio, P.R., Barthe, G., Biewer, S., Finkbeiner, B., Hermanns, H.: Is your software on dope? In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 83\u2013110. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_4"},{"key":"20_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-319-63390-9_31","volume-title":"Computer Aided Verification","author":"C Dehnert","year":"2017","unstructured":"Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592\u2013600. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_31"},{"key":"20_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-319-46520-3_8","volume-title":"Automated Technology for Verification and Analysis","author":"A Duret-Lutz","year":"2016","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, \u00c9., Xu, L.: Spot 2.0\u2014a framework for LTL and $$\\omega $$-automata manipulation. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 122\u2013129. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_8"},{"key":"20_CR28","doi-asserted-by":"publisher","unstructured":"Durumeric, Z., et al.: The matter of heartbleed. In: IMC 2014. https:\/\/doi.org\/10.1145\/2663716.2663755","DOI":"10.1145\/2663716.2663755"},{"key":"20_CR29","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Hahn, C.: Deciding hyperproperties. In: CONCUR 2016. https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2016.13","DOI":"10.4230\/LIPIcs.CONCUR.2016.13"},{"key":"20_CR30","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Hahn, C., Lukert, P., Stenger, M., Tentrup, L.: Synthesis from hyperproperties. Acta Informatica 57(1-2), 137\u2013163 (2020). https:\/\/doi.org\/10.1007\/s00236-019-00358-2","DOI":"10.1007\/s00236-019-00358-2"},{"key":"20_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-319-89963-3_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B Finkbeiner","year":"2018","unstructured":"Finkbeiner, B., Hahn, C., Stenger, M., Tentrup, L.: $$\\text{ RVHyper }$$: a runtime verification tool for temporal hyperproperties. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 194\u2013200. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89963-3_11"},{"key":"20_CR32","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Hahn, C., Stenger, M., Tentrup, L.: Monitoring hyperproperties. Formal Methods Syst. Des. 54(3), 336\u2013363 (2019). https:\/\/doi.org\/10.1007\/s10703-019-00334-z","DOI":"10.1007\/s10703-019-00334-z"},{"key":"20_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/978-3-319-96145-3_8","volume-title":"Computer Aided Verification","author":"B Finkbeiner","year":"2018","unstructured":"Finkbeiner, B., Hahn, C., Torfah, H.: Model checking quantitative hyperproperties. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 144\u2013163. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_8"},{"key":"20_CR34","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., M\u00fcller, C., Seidl, H., Zalinescu, E.: Verifying security policies in multi-agent workflows with loops. In: CCS 2017. https:\/\/doi.org\/10.1145\/3133956.3134080","DOI":"10.1145\/3133956.3134080"},{"key":"20_CR35","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$$^*$$. 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":"20_CR36","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Sipma, H.: Checking finite traces using alternating automata. Formal Methods Syst. Des. 24(2), 101\u2013127 (2004). https:\/\/doi.org\/10.1023\/B:FORM.0000017718.28096.48","DOI":"10.1023\/B:FORM.0000017718.28096.48"},{"key":"20_CR37","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Zimmermann, M.: The first-order logic of hyperproperties. In: STACS 2017. https:\/\/doi.org\/10.4230\/LIPIcs.STACS.2017.30","DOI":"10.4230\/LIPIcs.STACS.2017.30"},{"key":"20_CR38","doi-asserted-by":"publisher","unstructured":"Fortin, M., Kuijer, L.B., Totzke, P., Zimmermann, M.: HyperLTL satisfiability is $$\\Sigma _1^1$$-complete, HyperCTL$$^*$$ satisfiability is $$\\Sigma _1^2$$-complete. In: MFCS 2021. https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2021.47","DOI":"10.4230\/LIPIcs.MFCS.2021.47"},{"key":"20_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-319-07602-7_11","volume-title":"Formal Aspects of Component Software","author":"G G\u00f6ssler","year":"2014","unstructured":"G\u00f6ssler, G., Le M\u00e9tayer, D.: A general trace-based framework of logical causality. In: Fiadeiro, J.L., Liu, Z., Xue, J. (eds.) FACS 2013. LNCS, vol. 8348, pp. 157\u2013173. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-07602-7_11"},{"key":"20_CR40","doi-asserted-by":"publisher","unstructured":"G\u00f6ssler, G., Stefani, J.: Causality analysis and fault ascription in component-based systems. Theor. Comput. Sci. 837, 158\u2013180 (2020). https:\/\/doi.org\/10.1016\/j.tcs.2020.06.010","DOI":"10.1016\/j.tcs.2020.06.010"},{"key":"20_CR41","doi-asserted-by":"publisher","unstructured":"Groce, A., Chaki, S., Kroening, D., Strichman, O.: Error explanation with distance metrics. Int. J. Softw. Tools Technol. Transf. 8(3), 229\u2013247 (2006). https:\/\/doi.org\/10.1007\/s10009-005-0202-0","DOI":"10.1007\/s10009-005-0202-0"},{"key":"20_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-540-27813-9_35","volume-title":"Computer Aided Verification","author":"A Groce","year":"2004","unstructured":"Groce, A., Kroening, D., Lerda, F.: Understanding Counterexamples with explain. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 453\u2013456. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_35"},{"key":"20_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/3-540-44829-2_8","volume-title":"Model Checking Software","author":"A Groce","year":"2003","unstructured":"Groce, A., Visser, W.: What went wrong: explaining counterexamples. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 121\u2013136. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-44829-2_8"},{"key":"20_CR44","doi-asserted-by":"crossref","unstructured":"Halpern, J.Y.: A modification of the Halpern-Pearl definition of causality. In: IJCAI 2015. http:\/\/ijcai.org\/Abstract\/15\/427","DOI":"10.7551\/mitpress\/9780262035026.003.0002"},{"key":"20_CR45","doi-asserted-by":"crossref","unstructured":"Halpern, J.Y., Pearl, J.: Causes and explanations: a structural-model approach. Part I: causes. Br. J. Philos. Sci. 56(4), 843\u2013887 (2005). http:\/\/www.jstor.org\/stable\/3541870","DOI":"10.1093\/bjps\/axi147"},{"key":"20_CR46","doi-asserted-by":"crossref","unstructured":"Halpern, J.Y., Pearl, J.: Causes and explanations: a structural-model approach. Part II: explanations. Br. J. Philos. Sci. 56(4), 889\u2013911 (2005). http:\/\/www.jstor.org\/stable\/3541871","DOI":"10.1093\/bjps\/axi148"},{"key":"20_CR47","doi-asserted-by":"publisher","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279\u2013295 (1997). https:\/\/doi.org\/10.1109\/32.588521","DOI":"10.1109\/32.588521"},{"key":"20_CR48","doi-asserted-by":"publisher","unstructured":"Horak, T., et al.: Visual analysis of hyperproperties for understanding model checking results. IEEE Trans. Vis. Comput. Graph. 28(1), 357\u2013367 (2022). https:\/\/doi.org\/10.1109\/TVCG.2021.3114866","DOI":"10.1109\/TVCG.2021.3114866"},{"key":"20_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1007\/978-3-030-72016-2_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T-H Hsu","year":"2021","unstructured":"Hsu, T.-H., S\u00e1nchez, C., Bonakdarpour, B.: Bounded model checking for hyperproperties. In: Groote, J.F., Larsen, K.G. (eds.) TACAS 2021. LNCS, vol. 12651, pp. 94\u2013112. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_6"},{"key":"20_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/978-3-319-94144-8_26","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2018","author":"A Ignatiev","year":"2018","unstructured":"Ignatiev, A., Morgado, A., Marques-Silva, J.: PySAT: a Python toolkit for prototyping with SAT oracles. In: Beyersdorff, O., Wintersteiger, C.M. (eds.) SAT 2018. LNCS, vol. 10929, pp. 428\u2013437. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94144-8_26"},{"issue":"3","key":"20_CR51","first-page":"171","volume":"42","author":"E Jee","year":"2010","unstructured":"Jee, E., et al.: FbdVerifier: interactive and visual analysis of counterexample in formal verification of function block diagram. J. Res. Pract. Inf. Technol. 42(3), 171\u2013188 (2010)","journal-title":"J. Res. Pract. Inf. Technol."},{"key":"20_CR52","doi-asserted-by":"publisher","unstructured":"Kocher, P., et al.: Spectre attacks: exploiting speculative execution. In: SP 2019. https:\/\/doi.org\/10.1109\/SP.2019.00002","DOI":"10.1109\/SP.2019.00002"},{"key":"20_CR53","doi-asserted-by":"publisher","unstructured":"Krebs, A., Meier, A., Virtema, J., Zimmermann, M.: Team semantics for the specification and verification of hyperproperties. In: MFCS 2018. https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2018.10","DOI":"10.4230\/LIPIcs.MFCS.2018.10"},{"key":"20_CR54","unstructured":"Lahtinen, J., Launiainen, T., Heljanko, K., Ropponen, J.: Model checking methodology for large systems, faults and asynchronous behaviour: SARANA 2011 work report. No. 12 in VTT Tech., VTT Tech. Research Centre of Finland (2012)"},{"key":"20_CR55","doi-asserted-by":"publisher","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transf. 1(1\u20132) (1997). https:\/\/doi.org\/10.1007\/s100090050010","DOI":"10.1007\/s100090050010"},{"key":"20_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-642-35873-9_16","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"F Leitner-Fischer","year":"2013","unstructured":"Leitner-Fischer, F., Leue, S.: Causality checking for complex system models. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 248\u2013267. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_16"},{"key":"20_CR57","doi-asserted-by":"publisher","unstructured":"Leitner-Fischer, F., Leue, S.: Probabilistic fault tree synthesis using causality computation. Int. J. Crit. Comput. Based Syst. 4(2), 119\u2013143 (2013). https:\/\/doi.org\/10.1504\/IJCCBS.2013.056492","DOI":"10.1504\/IJCCBS.2013.056492"},{"issue":"17","key":"20_CR58","doi-asserted-by":"publisher","first-page":"556","DOI":"10.2307\/2025310","volume":"70","author":"D Lewis","year":"1973","unstructured":"Lewis, D.: Causation. J. Philos. 70(17), 556\u2013567 (1973)","journal-title":"J. Philos."},{"issue":"6","key":"20_CR59","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1145\/3357033","volume":"63","author":"M Lipp","year":"2020","unstructured":"Lipp, M., et al.: Meltdown: reading kernel memory from user space. Commun. ACM 63(6), 46\u201356 (2020)","journal-title":"Commun. ACM"},{"key":"20_CR60","doi-asserted-by":"publisher","unstructured":"Mascle, C., Zimmermann, M.: The keys to decidable HyperLTL satisfiability: small models or very simple formulas. In: CSL 2020. https:\/\/doi.org\/10.4230\/LIPIcs.CSL.2020.29","DOI":"10.4230\/LIPIcs.CSL.2020.29"},{"key":"20_CR61","doi-asserted-by":"crossref","unstructured":"McCullough, D.: Noninterference and the composability of security properties. In: Proceedings. 1988 IEEE Symposium on Security and Privacy, pp. 177\u2013186 (1988)","DOI":"10.1109\/SECPRI.1988.8110"},{"key":"20_CR62","doi-asserted-by":"crossref","unstructured":"Moore, E.F.: Gedanken-experiments on sequential machines. Aut. stud. 34 (1956)","DOI":"10.1515\/9781400882618-006"},{"key":"20_CR63","doi-asserted-by":"publisher","unstructured":"Pakonen, A., Buzhinsky, I., Vyatkin, V.: Counterexample visualization and explanation for function block diagrams. In: INDIN 2018. https:\/\/doi.org\/10.1109\/INDIN.2018.8472025","DOI":"10.1109\/INDIN.2018.8472025"},{"key":"20_CR64","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS 1977 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"20_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/978-3-540-31980-1_32","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V Schuppan","year":"2005","unstructured":"Schuppan, V., Biere, A.: Shortest counterexamples for symbolic model checking of LTL with past. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 493\u2013509. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31980-1_32"},{"key":"20_CR66","unstructured":"S\u00f6rensson, N.: Minisat 2.2 and minisat++ 1.1. SAT Race 2010"},{"key":"20_CR67","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1007\/978-3-030-30942-8_25","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"S Stucki","year":"2019","unstructured":"Stucki, S., S\u00e1nchez, C., Schneider, G., Bonakdarpour, B.: Gray-box monitoring of hyperproperties. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 406\u2013424. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_25"},{"key":"20_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/3-540-63104-6_19","volume-title":"Automated Deduction\u2014CADE-14","author":"MY Vardi","year":"1997","unstructured":"Vardi, M.Y.: Alternating automata: unifying truth and validity checking for temporal logics. In: McCune, W. (ed.) CADE 1997. LNCS, vol. 1249, pp. 191\u2013206. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63104-6_19"},{"key":"20_CR69","unstructured":"Vazquez-C., M., Rabe, M.: py-aiger. https:\/\/github.com\/mvcisback\/py-aiger"},{"key":"20_CR70","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/11901914_9","volume-title":"Automated Technology for Verification and Analysis","author":"C Wang","year":"2006","unstructured":"Wang, C., Yang, Z., Ivan\u010di\u0107, F., Gupta, A.: Whodunit? Causal analysis for counterexamples. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol. 4218, pp. 82\u201395. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11901914_9"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-13185-1_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,30]],"date-time":"2024-09-30T22:06:33Z","timestamp":1727733993000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-13185-1_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031131844","9783031131851"],"references-count":70,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-13185-1_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"7 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"209","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"40","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.9","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9.7","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}