{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T19:31:22Z","timestamp":1757619082434,"version":"3.44.0"},"reference-count":81,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2025,7,16]],"date-time":"2025-07-16T00:00:00Z","timestamp":1752624000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,16]],"date-time":"2025-07-16T00:00:00Z","timestamp":1752624000000},"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":["101055412","101055412"],"award-info":[{"award-number":["101055412","101055412"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["389792660","389792660"],"award-info":[{"award-number":["389792660","389792660"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"name":"CISPA - Helmholtz-Zentrum f\u00fcr Informationssicherheit gGmbH"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2025,8]]},"abstract":"Abstract<\/jats:title>\n Temporal hyperproperties are system properties that relate multiple execution traces. In finite-state systems, temporal hyperproperties are supported by model-checking algorithms, and tools for general temporal logics like HyperLTL exist. In infinite-state systems, the analysis of temporal hyperproperties has, so far, been limited to k<\/jats:italic>-safety properties, i.e., properties that stipulate the absence of a bad interaction between any k<\/jats:italic> traces. In this paper, we present an automated method for the verification of \n \n $$\\forall ^k\\exists ^l$$<\/jats:tex-math>\n \n \n \n \u2200<\/mml:mo>\n k<\/mml:mi>\n <\/mml:msup>\n \n \u2203<\/mml:mo>\n l<\/mml:mi>\n <\/mml:msup>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>-safety properties in infinite-state systems. A \n \n $$\\forall ^k\\exists ^l$$<\/jats:tex-math>\n \n \n \n \u2200<\/mml:mo>\n k<\/mml:mi>\n <\/mml:msup>\n \n \u2203<\/mml:mo>\n l<\/mml:mi>\n <\/mml:msup>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula>-safety property stipulates that for any k<\/jats:italic> traces, there exist l<\/jats:italic> traces such that the resulting \n \n $$k+l$$<\/jats:tex-math>\n \n \n k<\/mml:mi>\n +<\/mml:mo>\n l<\/mml:mi>\n <\/mml:mrow>\n <\/mml:math>\n <\/jats:alternatives>\n <\/jats:inline-formula> traces do not interact badly. This combination of universal and existential quantification captures many properties beyond k<\/jats:italic>-safety, including hyperliveness properties such as generalized non-interference or program refinement. Our verification method is based on a strategy-based instantiation of existential trace quantification combined with a program reduction, both in the context of a fixed predicate abstraction.<\/jats:p>","DOI":"10.1007\/s10703-025-00482-5","type":"journal-article","created":{"date-parts":[[2025,7,16]],"date-time":"2025-07-16T13:30:48Z","timestamp":1752672648000},"page":"238-277","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Predicate abstraction for hyperliveness verification"],"prefix":"10.1007","volume":"66","author":[{"given":"Raven","family":"Beutner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernd","family":"Finkbeiner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,7,16]]},"reference":[{"issue":"2","key":"482_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 (1991) The existence of refinement mappings. Theor Comput Sci 82(2):253\u2013284","journal-title":"Theor Comput Sci"},{"key":"482_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796819000145","volume":"29","author":"A Aguirre","year":"2019","unstructured":"Aguirre A, Barthe G, Gaboardi M, Garg D, Strub P-Y (2019) A relational logic for higher-order programs. J Funct Program 29:e16","journal-title":"J Funct Program"},{"issue":"4","key":"482_CR3","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 FB (1985) Defining liveness. Inf Process Lett 21(4):181\u2013185","journal-title":"Inf Process Lett"},{"key":"482_CR4","doi-asserted-by":"crossref","unstructured":"Baier C, Coenen N, Finkbeiner B, Funke F, Jantsch S, Siber J (2021) Causality-based game solving. In: International conference on computer aided verification, CAV 2021, volume 12759 of lecture notes in computer science. Springer, pp 894\u2013917","DOI":"10.1007\/978-3-030-81685-8_42"},{"key":"482_CR5","unstructured":"Barrett C, Stump A, Tinelli C et\u00a0al (2010) The smt-lib standard: version 2.0. In: International workshop on satisfiability modulo theories"},{"key":"482_CR6","doi-asserted-by":"crossref","unstructured":"Barrett CW, Fang Y, Goldberg B, Hu Y, Pnueli A, Zuck LD (2005) TVOC: a translation validator for optimizing compilers. In: International conference on computer aided verification, CAV 2005, volume 3576 of lecture notes in computer science. Springer, pp 291\u2013295","DOI":"10.1007\/11513988_29"},{"key":"482_CR7","doi-asserted-by":"crossref","unstructured":"Barthe G, Crespo JM, C Kunz (2013) Beyond 2-safety: Asymmetric product programs for relational program verification. In: International symposium on logical foundations of computer science, LFCS 2013, volume 7734 of lecture notes in computer science. Springer, pp 29\u201343","DOI":"10.1007\/978-3-642-35722-0_3"},{"issue":"6","key":"482_CR8","doi-asserted-by":"publisher","first-page":"1207","DOI":"10.1017\/S0960129511000193","volume":"21","author":"G Barthe","year":"2011","unstructured":"Barthe G, D\u2019Argenio PR, Rezk T (2011) Secure information flow by self-composition. Math Struct Comput Sci 21(6):1207\u20131252","journal-title":"Math Struct Comput Sci"},{"key":"482_CR9","doi-asserted-by":"crossref","unstructured":"Barthe G, Gr\u00e9goire B, SZ B\u00e9guelin (2009) Formal certification of code-based cryptographic proofs. In: Symposium on principles of programming languages, POPL 2009. ACM, pp 90\u2013101","DOI":"10.1145\/1480881.1480894"},{"key":"482_CR10","unstructured":"Bartocci E, Henzinger TA, Nickovic D, da\u00a0Costa AO (2023) Hypernode automata. In: International conference on concurrency theory, CONCUR 2023, volume 279 of LIPIcs, pp 21:1\u201321:16"},{"key":"482_CR11","doi-asserted-by":"crossref","unstructured":"Baumeister J, Coenen N, Bonakdarpour B, Finkbeiner B, S\u00e1nchez C (2021) A temporal logic for asynchronous hyperproperties. In: International conference on computer aided verification, CAV 2021, volume 12759 of lecture notes in computer science. Springer, pp 694\u2013717","DOI":"10.1007\/978-3-030-81685-8_33"},{"key":"482_CR12","doi-asserted-by":"crossref","unstructured":"Benton N (2004) Simple relational correctness proofs for static analyses and program transformations. In: Symposium on principles of programming languages, POPL 2004. ACM, pp 14\u201325","DOI":"10.1145\/964001.964003"},{"issue":"3","key":"482_CR13","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1051\/ita:2002013","volume":"36","author":"J Bernet","year":"2002","unstructured":"Bernet J, Janin D, Walukiewicz I (2002) Permissive strategies: from parity games to safety games. RAIRO Theor Inform Appl 36(3):261\u2013275","journal-title":"RAIRO Theor Inform Appl"},{"key":"482_CR14","doi-asserted-by":"crossref","unstructured":"Beutner R (2024) Automated software verification of hyperliveness. In: International conference tools and algorithms for the construction and analysis of systems, TACAS 2024, volume 14571 of lecture notes in computer science. Springer, pp 196\u2013216","DOI":"10.1007\/978-3-031-57249-4_10"},{"key":"482_CR15","doi-asserted-by":"crossref","unstructured":"Beutner R, Carral D, Finkbeiner B, Hofmann J, Kr\u00f6tzsch M (2022) Deciding hyperproperties combined with functional specifications. In: Symposium on logic in computer science, LICS 2022. ACM, pp 56:1\u201356:13","DOI":"10.1145\/3531130.3533369"},{"key":"482_CR16","unstructured":"Beutner R, Finkbeiner B (2021) A temporal logic for strategic hyperproperties. In: International conference on concurrency theory, CONCUR 2021, volume 203 of LIPIcs. Schloss Dagstuhl, pp 24:1\u201324:19"},{"key":"482_CR17","doi-asserted-by":"crossref","unstructured":"Beutner R, Finkbeiner B (2022) Prophecy variables for hyperproperty verification. In: Computer security foundations symposium, CSF 2022. IEEE, pp 471\u2013485","DOI":"10.1109\/CSF54842.2022.9919658"},{"key":"482_CR18","doi-asserted-by":"crossref","unstructured":"Beutner R, Finkbeiner B (2022) Software verification of hyperproperties beyond k-safety. In: International conference on computer aided verification, CAV 2022, volume 13371 of lecture notes in computer science. Springer, pp 341\u2013362","DOI":"10.1007\/978-3-031-13185-1_17"},{"key":"482_CR19","doi-asserted-by":"crossref","unstructured":"Beutner R, Finkbeiner B (2023) AutoHyper: explicit-state model checking for HyperLTL. In: International conference on tools and algorithms for the construction and analysis of systems, TACAS 2023, volume 13993 of lecture notes in computer science. Springer, pp 145\u2013163","DOI":"10.1007\/978-3-031-30823-9_8"},{"key":"482_CR20","doi-asserted-by":"crossref","unstructured":"Beutner R, Finkbeiner B (2023) HyperATL$$^*$$: a logic for hyperproperties in multi-agent systems. Log Methods Comput Sci 19(2)","DOI":"10.46298\/lmcs-19(2:13)2023"},{"key":"482_CR21","first-page":"189","volume":"2024","author":"R Beutner","year":"2024","unstructured":"Beutner R, Finkbeiner B (2024) Hyper strategy logic. Int Conf Autonomous Agents Multiagent Syst AAMAS 2024:189\u2013197","journal-title":"Int Conf Autonomous Agents Multiagent Syst AAMAS"},{"key":"482_CR22","doi-asserted-by":"crossref","unstructured":"Beutner R, Finkbeiner B (2024) Non-deterministic planning for hyperproperty verification. In: International conference on automated planning and scheduling, ICAPS 2024. AAAI Press, pp 25\u201330","DOI":"10.1609\/icaps.v34i1.31457"},{"key":"482_CR23","first-page":"1","volume":"6","author":"R Beutner","year":"2025","unstructured":"Beutner R, Finkbeiner B (2025) AutoHyper: leveraging language inclusion checking for hyperproperty model-checking. Int J Softw Tools Technol Transf 6:1\u20137","journal-title":"Int J Softw Tools Technol Transf"},{"key":"482_CR24","unstructured":"Beutner R, Finkbeiner B (2025) Multiplayer games with incomplete information for hyperproperty verification. In: International conference on autonomous agents and multiagent systems, AAMAS 2025"},{"key":"482_CR25","doi-asserted-by":"crossref","unstructured":"Beutner R, Finkbeiner B, Frenkel H, Metzger N (2023) Second-order hyperproperties. In: International conference on computer aided verification, CAV 2023, volume 13965 of lecture notes in computer science. Springer, pp 309\u2013332","DOI":"10.1007\/978-3-031-37703-7_15"},{"key":"482_CR26","doi-asserted-by":"crossref","unstructured":"Beutner R, Finkbeiner B, G\u00f6bl A (2024) Visualizing game-based certificates for hyperproperty verification. In: International symposium on formal methods, FM 2024, volume 14934 of lecture notes in computer science. Springer, pp 67\u201375","DOI":"10.1007\/978-3-031-71177-0_5"},{"key":"482_CR27","doi-asserted-by":"crossref","unstructured":"Beutner R, Hsu T-H, Bonakdarpour B, Finkbeiner B (2024) Syntax-guided automated program repair for hyperproperties. In: International conference on computer aided verification, CAV 2024, volume 14683 of lecture notes in computer science. Springer, pp 3\u201326","DOI":"10.1007\/978-3-031-65633-0_1"},{"key":"482_CR28","doi-asserted-by":"crossref","unstructured":"Beyene TA, Chaudhuri S, Popeea C, Rybalchenko A (2014) A constraint-based approach to solving games on infinite graphs. In: Symposium on principles of programming languages, POPL 2014. ACM, pp 221\u2013234","DOI":"10.1145\/2535838.2535860"},{"key":"482_CR29","doi-asserted-by":"crossref","unstructured":"Bozzelli L, Maubert B, Pinchinat S (2015) Unifying hyper and epistemic temporal logics. In: International conference on foundations of software science and computation structures, FoSSaCS 2015, volume 9034 of lecture notes in computer science. Springer, pp 167\u2013182","DOI":"10.1007\/978-3-662-46678-0_11"},{"key":"482_CR30","doi-asserted-by":"crossref","unstructured":"Bozzelli L, Peron A, S\u00e1nchez C (2021) Asynchronous extensions of HyperLTL. In: Symposium on logic in computer science, LICS 2021. IEEE, pp 1\u201313","DOI":"10.1109\/LICS52264.2021.9470583"},{"key":"482_CR31","unstructured":"Bozzelli L, Peron A, S\u00e1nchez C (2022) Expressiveness and decidability of temporal logics for asynchronous hyperproperties. In: International conference on concurrency theory, CONCUR 2022, volume 243 of LIPIcs, pp 27:1\u201327:16"},{"issue":"6","key":"482_CR32","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1109\/TSE.2004.22","volume":"30","author":"S Chaki","year":"2004","unstructured":"Chaki S, Clarke EM, Groce A, Jha S, Veith H (2004) Modular verification of software components in C. IEEE Trans Softw Eng 30(6):388\u2013402","journal-title":"IEEE Trans Softw Eng"},{"issue":"8","key":"482_CR33","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/2240236.2240262","volume":"55","author":"S Chaudhuri","year":"2012","unstructured":"Chaudhuri S, Gulwani S, Lublinerman R (2012) Continuity and robustness of programs. Commun ACM 55(8):107\u2013115","journal-title":"Commun ACM"},{"key":"482_CR34","doi-asserted-by":"crossref","unstructured":"Chen HY, Cook B, Fuhs C, Nimkar K, O\u2019Hearn PW (2014) Proving nontermination via safety. In: International conference on tools and algorithms for the construction and analysis of systems, TACAS 2014, volume 8413 of lecture notes in computer science. Springer, pp 156\u2013171","DOI":"10.1007\/978-3-642-54862-8_11"},{"key":"482_CR35","doi-asserted-by":"crossref","unstructured":"Churchill BR, Padon O, Sharma R, Aiken A (2019) Semantic program alignment for equivalence checking. In: Conference on programming language design and implementation, PLDI 2019. ACM, pp 1027\u20131040","DOI":"10.1145\/3314221.3314596"},{"key":"482_CR36","doi-asserted-by":"crossref","unstructured":"Clarkson MR, Finkbeiner B, Koleini M, Micinski KK, Rabe MN, S\u00e1nchez C (2014) Temporal logics for hyperproperties. In: International conference on principles of security and trust, POST 2014, volume 8414 of lecture notes in computer science. Springer, pp 265\u2013284","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"482_CR37","doi-asserted-by":"crossref","unstructured":"Clarkson MR, Schneider FB (2008) Hyperproperties. In: Computer security foundations symposium, CSF 2008. IEEE Computer Society, pp 51\u201365","DOI":"10.1109\/CSF.2008.7"},{"key":"482_CR38","doi-asserted-by":"crossref","unstructured":"Coenen N, Finkbeiner B, S\u00e1nchez C, Tentrup L (2019) Verifying hyperliveness. In: International conference on computer aided verification, CAV 2019, volume 11561 of lecture notes in computer science. Springer, pp 121\u2013139","DOI":"10.1007\/978-3-030-25540-4_7"},{"key":"482_CR39","doi-asserted-by":"crossref","unstructured":"Cook B, Fuhs C, Nimkar K, O\u2019Hearn PW (2014) Disproving termination with overapproximation. In: Formal methods in computer-aided design, FMCAD 2014. IEEE, pp 67\u201374","DOI":"10.1109\/FMCAD.2014.6987597"},{"issue":"POPL","key":"482_CR40","doi-asserted-by":"publisher","first-page":"1568","DOI":"10.1145\/3704889","volume":"9","author":"A Correnson","year":"2025","unstructured":"Correnson A, Finkbeiner B (2025) Coinductive proofs for temporal hyperliveness. Proc ACM Program Lang 9(POPL):1568\u20131595","journal-title":"Proc ACM Program Lang"},{"issue":"OOPSLA2","key":"482_CR41","doi-asserted-by":"publisher","first-page":"1420","DOI":"10.1145\/3689761","volume":"8","author":"A Correnson","year":"2024","unstructured":"Correnson A, Nie\u00dfen T, Finkbeiner B, Weissenbacher G (2024) Finding $$\\forall \\exists$$ hyperbugs using symbolic execution. Proc ACM Program Lang 8(OOPSLA2):1420\u20131445","journal-title":"Proc ACM Program Lang"},{"issue":"POPL","key":"482_CR42","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1145\/3704852","volume":"9","author":"P Cousot","year":"2025","unstructured":"Cousot P, Wang J (2025) Calculational design of hyperlogics by abstract interpretation. Proc ACM Program Lang 9(POPL):446\u2013478","journal-title":"Proc ACM Program Lang"},{"key":"482_CR43","doi-asserted-by":"crossref","unstructured":"D\u2019Antoni L, Veanes M (2017) The power of symbolic automata and transducers. In: International conference on computer aided verification, CAV 2017, volume 10426 of lecture notes in computer science. Springer, pp 47\u201367","DOI":"10.1007\/978-3-319-63387-9_3"},{"issue":"PLDI","key":"482_CR44","doi-asserted-by":"publisher","first-page":"1485","DOI":"10.1145\/3656437","volume":"8","author":"T Dardinier","year":"2024","unstructured":"Dardinier T, M\u00fcller P (2024) Hyper hoare logic: (dis-)proving program hyperproperties. Proc ACM Program Lang 8(PLDI):1485\u20131509","journal-title":"Proc ACM Program Lang"},{"key":"482_CR45","doi-asserted-by":"crossref","unstructured":"D\u2019Argenio PR, Barthe G, Biewer S, Finkbeiner B, Hermanns H (2017) Is your software on dope? - formal analysis of surreptitiously \"enhanced\" programs. In: European symposium on programming, ESOP 2017, volume 10201 of lecture notes in computer science. Springer, pp 83\u2013110","DOI":"10.1007\/978-3-662-54434-1_4"},{"key":"482_CR46","doi-asserted-by":"crossref","unstructured":"de\u00a0Alfaro L, Godefroid P, Jagadeesan R (2004) Three-valued abstractions of games: uncertainty, but with precision. In: Symposium on logic in computer science, LICS 2004. IEEE Computer Society, pp 170\u2013179","DOI":"10.1109\/LICS.2004.1319611"},{"key":"482_CR47","doi-asserted-by":"crossref","unstructured":"de\u00a0Alfaro L, Roy P (2007) Solving games via three-valued abstraction refinement. In: International Conference on concurrency theory, CONCUR 2007, volume 4703 of lecture notes in computer science. Springer, pp 74\u201389","DOI":"10.1007\/978-3-540-74407-8_6"},{"key":"482_CR48","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura LM, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: International conference on tools and algorithms for the construction and analysis of systems, TACAS 2008, volume 4963 of lecture notes in computer science. Springer, pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"482_CR49","doi-asserted-by":"crossref","unstructured":"Dickerson R, Ye Q, Zhang MK, Delaware B (2022) RHLE: modular deductive verification of relational $$\\forall$$$$\\exists$$ properties. In: Asian symposium on programming languages and systems, APLAS 2022, volume 13658 of lecture notes in computer science. Springer, pp 67\u201387","DOI":"10.1007\/978-3-031-21037-2_4"},{"issue":"OOPSLA2","key":"482_CR50","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1145\/3563298","volume":"6","author":"E D\u2019Osualdo","year":"2022","unstructured":"D\u2019Osualdo E, Farzan A, Dreyer D (2022) Proving hypersafety compositionally. Proc ACM Program Lang 6(OOPSLA2):289\u2013314","journal-title":"Proc ACM Program Lang"},{"issue":"1","key":"482_CR51","doi-asserted-by":"publisher","first-page":"3:1","DOI":"10.1145\/3324783","volume":"42","author":"M Eilers","year":"2020","unstructured":"Eilers M, M\u00fcller P, Hitz S (2020) Modular product programs. ACM Trans Program Lang Syst 42(1):3:1-3:37","journal-title":"ACM Trans Program Lang Syst"},{"key":"482_CR52","doi-asserted-by":"crossref","unstructured":"Faella M, Parlato G (2023) Reachability games modulo theories with a bounded safety player. In: Conference on artificial intelligence, AAAI 2023. AAAI Press, pp 6330\u20136337","DOI":"10.1609\/aaai.v37i5.25779"},{"issue":"POPL","key":"482_CR53","doi-asserted-by":"publisher","first-page":"61:1","DOI":"10.1145\/3158149","volume":"2","author":"A Farzan","year":"2018","unstructured":"Farzan A, Kincaid Z (2018) Strategy synthesis for linear arithmetic games. Proc ACM Program Lang 2(POPL):61:1-61:30","journal-title":"Proc ACM Program Lang"},{"key":"482_CR54","doi-asserted-by":"crossref","unstructured":"Farzan A, Vandikas A (2019) Automated hypersafety verification. In: International conference on computer aided verification, CAV 2019, volume 11561 of lecture notes in computer science. Springer, pp 200\u2013218","DOI":"10.1007\/978-3-030-25540-4_11"},{"issue":"POPL","key":"482_CR55","doi-asserted-by":"publisher","first-page":"13:1","DOI":"10.1145\/3371081","volume":"4","author":"A Farzan","year":"2020","unstructured":"Farzan A, Vandikas A (2020) Reductions for safety proofs. Proc ACM Program Lang 4(POPL):13:1-13:28","journal-title":"Proc ACM Program Lang"},{"key":"482_CR56","doi-asserted-by":"crossref","unstructured":"Finkbeiner B, Rabe M\u00a0N, C S\u00e1nchez (2015) Algorithms for model checking HyperLTL and HyperCTL$$^*$$. In: International conference on computer aided verification, CAV 2015, volume 9206 of lecture notes in computer science. Springer, pp 30\u201348","DOI":"10.1007\/978-3-319-21690-4_3"},{"issue":"1","key":"482_CR57","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s13389-016-0141-6","volume":"8","author":"Q Ge","year":"2018","unstructured":"Ge Q, Yarom Y, Cock D, Heiser G (2018) A survey of microarchitectural timing attacks and countermeasures on contemporary hardware. J Cryptogr Eng 8(1):1\u201327","journal-title":"J Cryptogr Eng"},{"key":"482_CR58","doi-asserted-by":"crossref","unstructured":"Graf S, Sa\u00efdi H (1997) Construction of abstract state graphs with PVS. In: International conference on computer aided verification, CAV 1997, volume 1254 of lecture notes in computer science. Springer, pp 72\u201383","DOI":"10.1007\/3-540-63166-6_10"},{"issue":"POPL","key":"482_CR59","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3434319","volume":"5","author":"JO Gutsfeld","year":"2021","unstructured":"Gutsfeld JO, M\u00fcller-Olm M, Ohrem C (2021) Automata and fixpoints for asynchronous hyperproperties. Proc ACM Program Lang 5(POPL):1\u201329","journal-title":"Proc ACM Program Lang"},{"issue":"POPL","key":"482_CR60","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1145\/3632844","volume":"8","author":"JO Gutsfeld","year":"2024","unstructured":"Gutsfeld JO, M\u00fcller-Olm M, Ohrem C (2024) Deciding asynchronous hyperproperties for recursive programs. Proc ACM Program Lang 8(POPL):33\u201360","journal-title":"Proc ACM Program Lang"},{"key":"482_CR61","doi-asserted-by":"crossref","unstructured":"Heizmann M, Hoenicke J, Podelski A (2009) Refinement of trace abstraction. In: International symposium on static analysis, SAS 2009, vol 5673. Springer, pp 69\u201385","DOI":"10.1007\/978-3-642-03237-0_7"},{"key":"482_CR62","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Jhala R, Majumdar R, Sutre G (2002) Lazy abstraction. In: Symposium on principles of programming languages, POPL 2002. ACM, pp 58\u201370","DOI":"10.1145\/503272.503279"},{"issue":"3","key":"482_CR63","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"M Herlihy","year":"1990","unstructured":"Herlihy M, Wing JM (1990) Linearizability: a correctness condition for concurrent objects. ACM Trans Program Lang Syst 12(3):463\u2013492","journal-title":"ACM Trans Program Lang Syst"},{"key":"482_CR64","doi-asserted-by":"crossref","unstructured":"Hsu T-H, S\u00e1nchez C, Bonakdarpour B (2021) Bounded model checking for hyperproperties. In: international conference on tools and algorithms for the construction and analysis of systems, TACAS 2021, volume 12651 of lecture notes in computer science. Springer, pp 94\u2013112","DOI":"10.1007\/978-3-030-72016-2_6"},{"key":"482_CR65","doi-asserted-by":"crossref","unstructured":"Itzhaky S, Shoham S, Vizel Y (2024) Hyperproperty verification as CHC satisfiability. In: European symposium on programming, ESOP 2024, volume 14577 of lecture notes in computer science. Springer, pp 212\u2013241","DOI":"10.1007\/978-3-031-57267-8_9"},{"key":"482_CR66","doi-asserted-by":"crossref","unstructured":"Jhala R, Podelski A, Rybalchenko A (2018) Predicate abstraction for program verification. In: Handbook of model checking. Springer, pp 447\u2013491","DOI":"10.1007\/978-3-319-10575-8_15"},{"key":"482_CR67","doi-asserted-by":"crossref","unstructured":"Kuwahara T, Sato R, Unno H, Kobayashi N (2015) Predicate abstraction and CEGAR for disproving termination of higher-order functional programs. In: International conference on computer aided verification, CAV 2015, volume 9207 of lecture notes in computer science. Springer, pp 287\u2013303","DOI":"10.1007\/978-3-319-21668-3_17"},{"issue":"12","key":"482_CR68","doi-asserted-by":"publisher","first-page":"717","DOI":"10.1145\/361227.361234","volume":"18","author":"RJ Lipton","year":"1975","unstructured":"Lipton RJ (1975) Reduction: a method of proving properties of parallel programs. Commun ACM 18(12):717\u2013721","journal-title":"Commun ACM"},{"key":"482_CR69","doi-asserted-by":"crossref","unstructured":"McCullough D (1988) Noninterference and the composability of security properties. In: Symposium on security and privacy, SP 1988. IEEE Computer Society, pp 177\u2013186","DOI":"10.1109\/SECPRI.1988.8110"},{"key":"482_CR70","doi-asserted-by":"crossref","unstructured":"McLean J (1994) A general theory of composition for trace sets closed under selective interleaving functions. In: Symposium on security and privacy, SP 1994. IEEE Computer Society, pp 79\u201393","DOI":"10.1109\/RISP.1994.296590"},{"key":"482_CR71","doi-asserted-by":"crossref","unstructured":"Nagasamudram R, Naumann DA (2021) Alignment completeness for relational hoare logics. In: Symposium on logic in computer science, LICS 2021. IEEE, pp 1\u201313","DOI":"10.1109\/LICS52264.2021.9470690"},{"key":"482_CR72","doi-asserted-by":"crossref","unstructured":"Pasareanu CS, Pel\u00e1nek R, Visser W (2007) Predicate abstraction with under-approximation refinement. Log Methods Comput Sci 3(1)","DOI":"10.2168\/LMCS-3(1:5)2007"},{"key":"482_CR73","doi-asserted-by":"crossref","unstructured":"Pnueli A (1977) The temporal logic of programs. In: Symposium on foundations of computer science, FOCS 1997. IEEE Computer Society, pp 46\u201357","DOI":"10.1109\/SFCS.1977.32"},{"key":"482_CR74","doi-asserted-by":"crossref","unstructured":"Pnueli A, Rosner R (1989) On the synthesis of a reactive module. In: Symposium on principles of programming languages, POPL 1989. ACM Press, pp 179\u2013190","DOI":"10.1145\/75277.75293"},{"issue":"3","key":"482_CR75","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1145\/1232420.1232422","volume":"29","author":"A Podelski","year":"2007","unstructured":"Podelski A, Rybalchenko A (2007) Transition predicate abstraction and fair termination. ACM Trans Program Lang Syst 29(3):15","journal-title":"ACM Trans Program Lang Syst"},{"key":"482_CR76","doi-asserted-by":"crossref","unstructured":"Pommellet A, Touili T (2018) Model-checking HyperLTL for pushdown systems. In: International symposium on model checking software, SPIN 2018, volume 10869 of lecture notes in computer science. Springer, pp 133\u2013152","DOI":"10.1007\/978-3-319-94111-0_8"},{"key":"482_CR77","doi-asserted-by":"crossref","unstructured":"Shemer R, Gurfinkel A, Shoham S, Vizel Y (2019) Property directed self composition. In: International conference on computer aided verification, CAV 2019, volume 11561 of lecture notes in computer science. Springer, pp 161\u2013179","DOI":"10.1007\/978-3-030-25540-4_9"},{"key":"482_CR78","doi-asserted-by":"crossref","unstructured":"Sousa M, Dillig I (2016) Cartesian hoare logic for verifying k-safety properties. In: Conference on programming language design and implementation, PLDI 2016. ACM, pp 57\u201369","DOI":"10.1145\/2908080.2908092"},{"key":"482_CR79","doi-asserted-by":"crossref","unstructured":"Unno H, Terauchi T, Koskinen E (2021) Constraint-based relational verification. In: International conference on computer aided verification, CAV 2021, volume 12759 of lecture notes in computer science. Springer, pp 742\u2013766","DOI":"10.1007\/978-3-030-81685-8_35"},{"key":"482_CR80","doi-asserted-by":"crossref","unstructured":"Walker A, Ryzhyk L (2014) Predicate abstraction for reactive synthesis. In: Formal methods in computer-aided design, FMCAD 2014. IEEE, pp 219\u2013226","DOI":"10.1109\/FMCAD.2014.6987617"},{"key":"482_CR81","doi-asserted-by":"crossref","unstructured":"Zdancewic S, Myers AC (2003) Observational determinism for concurrent program security. In: Computer security foundations workshop, CSFW 2003). IEEE Computer Society, pp\u00a029","DOI":"10.1109\/CSFW.2003.1212703"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-025-00482-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-025-00482-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-025-00482-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,7]],"date-time":"2025-09-07T12:18:47Z","timestamp":1757247527000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-025-00482-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,7,16]]},"references-count":81,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,8]]}},"alternative-id":["482"],"URL":"https:\/\/doi.org\/10.1007\/s10703-025-00482-5","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2025,7,16]]},"assertion":[{"value":"27 June 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 May 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 July 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Not applicable.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethical approval"}},{"value":"Not applicable.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}]}}