{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T18:19:04Z","timestamp":1784830744304,"version":"3.55.0"},"reference-count":91,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101055412"],"award-info":[{"award-number":["101055412"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"German Research Foundation","doi-asserted-by":"crossref","award":["389792660"],"award-info":[{"award-number":["389792660"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>\n                    Hyperproperties are system properties that relate multiple execution traces and commonly occur when specifying information-flow and security policies. Logics like HyperLTL utilize explicit quantification over execution traces to express temporal hyperproperties in reactive systems, i.e., hyperproperties that reason about the temporal behavior along infinite executions. An often unwanted side-effect of such logics is that they compare the quantified traces\n                    <jats:italic toggle=\"yes\">synchronously<\/jats:italic>\n                    . This prohibits the logics from expressing properties that compare multiple traces asynchronously, such as Zdancewic and Myers\u2019s\n                    <jats:italic toggle=\"yes\">observational determinism<\/jats:italic>\n                    , McLean\u2019s\n                    <jats:italic toggle=\"yes\">non-inference<\/jats:italic>\n                    , or\n                    <jats:italic toggle=\"yes\">stuttering refinement<\/jats:italic>\n                    . We study the model-checking problem for a variant of\n                    <jats:italic toggle=\"yes\">asynchronous HyperLTL<\/jats:italic>\n                    (A-HLTL), a temporal logic that can express hyperproperties where multiple traces are compared across timesteps. In addition to quantifying over system traces, A-HLTL features secondary quantification over stutterings of these traces. Consequently, A-HLTL allows for a succinct specification of many widely used asynchronous hyperproperties. Model-checking A-HLTL requires finding suitable stutterings, which, thus far, has been only possible for very restricted fragments or\n                    <jats:italic toggle=\"yes\">terminating<\/jats:italic>\n                    systems. In this paper, we propose a novel game-based approach for the verification of arbitrary \u2200\n                    <jats:sup>\u2217<\/jats:sup>\n                    \u2203\n                    <jats:sup>\u2217<\/jats:sup>\n                    A-HLTL formulas in\n                    <jats:italic toggle=\"yes\">reactive<\/jats:italic>\n                    systems. In our method, we consider the verification as a game played between a verifier and a refuter, who challenge each other by controlling parts of the underlying traces and stutterings. A winning strategy for the verifier then corresponds to concrete witnesses for existentially quantified traces and asynchronous alignments for existentially quantified stutterings. We identify fragments for which our game-based interpretation is complete and thus constitutes a finite-state decision procedure. We contribute a prototype implementation for finite-state systems and report on encouraging experimental results.\n                  <\/jats:p>","DOI":"10.1145\/3763130","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:51:31Z","timestamp":1759999891000},"page":"2227-2253","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Verifying Asynchronous Hyperproperties in Reactive Systems"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6234-5651","authenticated-orcid":false,"given":"Raven","family":"Beutner","sequence":"first","affiliation":[{"name":"CISPA Helmholtz Center for Information Security, Saarbr\u00fccken, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4280-8441","authenticated-orcid":false,"given":"Bernd","family":"Finkbeiner","sequence":"additional","affiliation":[{"name":"CISPA Helmholtz Center for Information Security, Saarbr\u00fccken, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","unstructured":"Mart\u00edn Abadi and Leslie Lamport. 1991. The Existence of Refinement Mappings. Theor. Comput. Sci. (1991). doi:10.1016\/0304-3975(91)90224-P","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","unstructured":"Erika \u00c1brah\u00e1m Ezio Bartocci Borzoo Bonakdarpour and Oyendrila Dobe. 2020. Probabilistic Hyperproperties with Nondeterminism. In International Symposium on Automated Technology for Verification and Analysis ATVA 2020s. doi:10.1007\/978-3-030-59152-6_29","DOI":"10.1007\/978-3-030-59152-6_29"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","unstructured":"Erika \u00c1brah\u00e1m and Borzoo Bonakdarpour. 2018. HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties. In International Conference on Quantitative Evaluation of Systems QEST 2018. doi:10.1007\/978-3-319-99154-2_2","DOI":"10.1007\/978-3-319-99154-2_2"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","unstructured":"Timos Antonopoulos Eric Koskinen Ton Chanh Le Ramana Nagasamudram David A. Naumann and Minh Ngo. 2023. An Algebra of Alignment for Relational Verification. Proc. ACM Program. Lang. POPL (2023). doi:10.1145\/3571213","DOI":"10.1145\/3571213"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","unstructured":"Mounir Assaf David A. Naumann Julien Signoles Eric Totel and Fr\u00e9d\u00e9ric Tronel. 2017. Hypercollecting semantics and its application to static analysis of information flow. In Symposium on Principles of Programming Languages POPL 2017. doi:10.1145\/3009837.3009889","DOI":"10.1145\/3009837.3009889"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","unstructured":"Ali Bajwa Minjian Zhang Rohit Chadha and Mahesh Viswanathan. 2023. Stack-Aware Hyperproperties. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS 2023. doi:10.1007\/978-3-031-30823-9_16","DOI":"10.1007\/978-3-031-30823-9_16"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","unstructured":"Gilles Barthe Pedro R. D\u2019Argenio and Tamara Rezk. 2004. Secure Information Flow by Self-Composition. In Computer Security Foundations Workshop CSFW 2004. doi:10.1109\/CSFW.2004.17","DOI":"10.1109\/CSFW.2004.17"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","unstructured":"Ezio Bartocci Thomas Ferr\u00e8re Thomas A. Henzinger Dejan Nickovic and Ana Oliveira da Costa. 2022. Information-flow Interfaces. In International Conference on Fundamental Approaches to Software Engineering FASE 2022. doi:10.1007\/978-3-030-99429-7_1","DOI":"10.1007\/978-3-030-99429-7_1"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","unstructured":"Ezio Bartocci Thomas A. Henzinger Dejan Nickovic and Ana Oliveira da Costa. 2023. Hypernode Automata. In International Conference on Concurrency Theory CONCUR 2023. doi:10.4230\/LIPICS.CONCUR.2023.21","DOI":"10.4230\/LIPICS.CONCUR.2023.21"},{"key":"e_1_3_1_11_1","unstructured":"Jon Barwise. 1977. An introduction to first-order logic. In Studies in Logic and the Foundations of Mathematics."},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","unstructured":"Jan Baumeister Norine Coenen Borzoo Bonakdarpour Bernd Finkbeiner and C\u00e9sar S\u00e1nchez. 2021. A Temporal Logic for Asynchronous Hyperproperties. In International Conference on Computer Aided Verification CAV 2021. doi:10.1007\/978-3-030-81685-8_33","DOI":"10.1007\/978-3-030-81685-8_33"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","unstructured":"Nick Benton. 2004. Simple relational correctness proofs for static analyses and program transformations. In Symposium on Principles of Programming Languages POPL 2004. doi:10.1145\/964001.964003","DOI":"10.1145\/964001.964003"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","unstructured":"Raven Beutner. 2024. Automated Software Verification of Hyperliveness. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS 2024. doi:10.1007\/978-3-031-57249-4_10","DOI":"10.1007\/978-3-031-57249-4_10"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","unstructured":"Raven Beutner and Bernd Finkbeiner. 2022a. Prophecy Variables for Hyperproperty Verification. In Computer Security Foundations Symposium CSF 2022. doi:10.1109\/CSF54842.2022.9919658","DOI":"10.1109\/CSF54842.2022.9919658"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","unstructured":"Raven Beutner and Bernd Finkbeiner. 2022b. Software Verification of Hyperproperties Beyond k-Safety. In International Conference on Computer Aided Verification CAV 2022. doi:10.1007\/978-3-031-13185-1_17","DOI":"10.1007\/978-3-031-13185-1_17"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","unstructured":"Raven Beutner and Bernd Finkbeiner. 2023a. AutoHyper: Explicit-State Model Checking for HyperLTL. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS 2023. doi:10.1007\/978-3-031-30823-9_8","DOI":"10.1007\/978-3-031-30823-9_8"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","unstructured":"Raven Beutner and Bernd Finkbeiner. 2023b. HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems. Log. Methods Comput. Sci. (2023). doi:10.46298\/LMCS-19(2:13)2023","DOI":"10.46298\/LMCS-19(2:13)2023"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","unstructured":"Raven Beutner and Bernd Finkbeiner. 2024. Non-deterministic Planning for Hyperproperty Verification. In International Conference on Automated Planning and Scheduling ICAPS 2024. doi:10.1609\/ICAPS.V34I1.31457","DOI":"10.1609\/ICAPS.V34I1.31457"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","unstructured":"Raven Beutner and Bernd Finkbeiner. 2025a. AutoHyper: leveraging Language Inclusion Checking for Hyperproperty Model-Checking. Int. J. Softw. Tools Technol. Transf. (2025). doi:10.1007\/s10009-025-00801-5","DOI":"10.1007\/s10009-025-00801-5"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","unstructured":"Raven Beutner and Bernd Finkbeiner. 2025b. Multiplayer Games With Incomplete Information for Hyperproperty Verification. In International Conference on Autonomous Agents and Multiagent Systems AAMAS 2025. doi:10.5555\/3709347.3743896","DOI":"10.5555\/3709347.3743896"},{"key":"e_1_3_1_22_1","unstructured":"Raven Beutner and Bernd Finkbeiner. 2025c. On Hyperproperty Verification Quantifier Alternations and Games under Partial Information. In Formal Methods in Computer-Aided Design FMCAD 2025."},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","unstructured":"Raven Beutner Bernd Finkbeiner Hadar Frenkel and Niklas Metzger. 2023. Second-Order Hyperproperties. In International Conference on Computer Aided Verification CAV 2023. doi:10.1007\/978-3-031-37703-7_15","DOI":"10.1007\/978-3-031-37703-7_15"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","unstructured":"Raven Beutner Tzu-Han Hsu Borzoo Bonakdarpour and Bernd Finkbeiner. 2024. Syntax-Guided Automated Program Repair for Hyperproperties. In International Conference on Computer Aided Verification CAV 2024. doi:10.1007\/978-3-031-65633-0_1","DOI":"10.1007\/978-3-031-65633-0_1"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","unstructured":"Tewodros A. Beyene Swarat Chaudhuri Corneliu Popeea and Andrey Rybalchenko. 2014. A constraint-based approach to solving games on infinite graphs. In Symposium on Principles of Programming Languages POPL 2014. doi:10.1145\/2535838.2535860","DOI":"10.1145\/2535838.2535860"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","unstructured":"Sebastian Biewer Rayna Dimitrova Michael Fries Maciej Gazda Thomas Heinze Holger Hermanns and Mohammad Reza Mousavi. 2022. Conformance Relations and Hyperproperties for Doping Detection in Time and Space. Log. Methods Comput. Sci. (2022). doi:10.46298\/LMCS-18(1:14)2022","DOI":"10.46298\/LMCS-18(1:14)2022"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","unstructured":"Laura Bozzelli Bastien Maubert and Sophie Pinchinat. 2015. Unifying Hyper and Epistemic Temporal Logics. In International Conference on Foundations of Software Science and Computation Structures FoSSaCS 2015. doi:10.1007\/978-3-662-46678-0_11","DOI":"10.1007\/978-3-662-46678-0_11"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","unstructured":"Laura Bozzelli Adriano Peron and C\u00e9sar S\u00e1nchez. 2021. Asynchronous Extensions of HyperLTL. In Symposium on Logic in Computer Science LICS 2021. doi:10.1109\/LICS52264.2021.9470583","DOI":"10.1109\/LICS52264.2021.9470583"},{"key":"e_1_3_1_29_1","unstructured":"Laura Bozzelli Adriano Peron and C\u00e9sar S\u00e1nchez. 2022. Expressiveness and Decidability of Temporal Logics for Asynchronous Hyperproperties. In International Conference on Concurrency Theory CONCUR 2022. doi:10.4230\/LIPIcs.CONCUR. 2022.27"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","unstructured":"Swarat Chaudhuri Sumit Gulwani and Roberto Lublinerman. 2012. Continuity and robustness of programs. Commun. ACM (2012). doi:10.1145\/2240236.2240262","DOI":"10.1145\/2240236.2240262"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","unstructured":"Minki Cho Youngju Song Dongjae Lee Lennard G\u00e4her and Derek Dreyer. 2023. Stuttering for Free. Proc. ACM Program. Lang. OOPSLA (2023). doi:10.1145\/3622857","DOI":"10.1145\/3622857"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","unstructured":"Alessandro Cimatti Edmund M. Clarke Enrico Giunchiglia Fausto Giunchiglia Marco Pistore Marco Roveri Roberto Sebastiani and Armando Tacchella. 2002. NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In International Conference on Computer Aided Verification CAV 2002. doi:10.1007\/3-540-45657-0_29","DOI":"10.1007\/3-540-45657-0_29"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","unstructured":"Michael R. Clarkson Bernd Finkbeiner Masoud Koleini Kristopher K. Micinski Markus N. Rabe and C\u00e9sar S\u00e1nchez. 2014. Temporal Logics for Hyperproperties. In International Conference on Principles of Security and Trust POST 2014. doi:10.1007\/978-3-642-54792-8_15","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","unstructured":"Michael R. Clarkson and Fred B. Schneider. 2008. Hyperproperties. In Computer Security Foundations Symposium CSF 2008. doi:10.1109\/CSF.2008.7","DOI":"10.1109\/CSF.2008.7"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","unstructured":"Norine Coenen Bernd Finkbeiner Christopher Hahn and Jana Hofmann. 2019a. The Hierarchy of Hyperlogics. In Symposium on Logic in Computer Science LICS 2019. doi:10.1109\/LICS.2019.8785713","DOI":"10.1109\/LICS.2019.8785713"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","unstructured":"Norine Coenen Bernd Finkbeiner C\u00e9sar S\u00e1nchez and Leander Tentrup. 2019b. Verifying Hyperliveness. In International Conference on Computer Aided Verification CAV 2019. doi:10.1007\/978-3-030-25540-4_7","DOI":"10.1007\/978-3-030-25540-4_7"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","unstructured":"Arthur Correnson and Bernd Finkbeiner. 2025. Coinductive Proofs for Temporal Hyperliveness. Proc. ACM Program. Lang. POPL (2025). doi:10.1145\/3704889","DOI":"10.1145\/3704889"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","unstructured":"Arthur Correnson Tobias Nie\u00dfen Bernd Finkbeiner and Georg Weissenbacher. 2024. Finding \u2200 \u2203 Hyperbugs using Symbolic Execution. Proc. ACM Program. Lang. OOPSLA (2024). doi:10.1145\/3689761","DOI":"10.1145\/3689761"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","unstructured":"Patrick Cousot and Radhia Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Symposium on Principles of Programming Languages POPL 1977. doi:10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","unstructured":"Thibault Dardinier and Peter M\u00fcller. 2024. Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties. Proc. ACM Program. Lang. PLDI (2024). doi:10.1145\/3656437","DOI":"10.1145\/3656437"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","unstructured":"Luca de Alfaro Thomas A. Henzinger and Rupak Majumdar. 2001. Symbolic Algorithms for Infinite-State Games. In International Conference on Concurrency Theory CONCUR 2001. doi:10.1007\/3-540-44685-0_36","DOI":"10.1007\/3-540-44685-0_36"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","unstructured":"Robert Dickerson Qianchuan Ye Michael K. Zhang and Benjamin Delaware. 2022. RHLE: Modular Deductive Verification of Relational \u2200\u2203 Properties. In Asian Symposium on Programming Languages and Systems APLAS 2022. doi:10.1007\/978-3-031-21037-2_4","DOI":"10.1007\/978-3-031-21037-2_4"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","unstructured":"Rayna Dimitrova Bernd Finkbeiner and Hazem Torfah. 2020. Probabilistic Hyperproperties of Markov Decision Processes. In International Symposium on Automated Technology for Verification and Analysis ATVA 2020. doi:10.1007\/978-3-030-59152-6_27","DOI":"10.1007\/978-3-030-59152-6_27"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","unstructured":"Emanuele D\u2019Osualdo Azadeh Farzan and Derek Dreyer. 2022. Proving hypersafety compositionally. Proc. ACM Program. Lang. OOPSLA (2022). doi:10.1145\/3563298","DOI":"10.1145\/3563298"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","unstructured":"Alexandre Duret-Lutz Etienne Renault Maximilien Colange Florian Renkin Alexandre Gbaguidi Aisse Philipp SchlehuberCaissier Thomas Medioni Antoine Martin J\u00e9r\u00f4me Dubois Cl\u00e9ment Gillard and Henrich Lauko. 2022. From Spot 2.0 to Spot 2.10: What\u2019s New?. In International Conference on Computer Aided Verification CAV 2022. doi:10.1007\/978-3-031-13188-2_9","DOI":"10.1007\/978-3-031-13188-2_9"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","unstructured":"Marco Eilers Thibault Dardinier and Peter M\u00fcller. 2023. CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity. Proc. ACM Program. Lang. PLDI (2023). doi:10.1145\/3591289","DOI":"10.1145\/3591289"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","unstructured":"Marco Eilers Peter M\u00fcller and Samuel Hitz. 2020. Modular Product Programs. ACM Trans. Program. Lang. Syst. (2020). doi:10.1145\/3324783","DOI":"10.1145\/3324783"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","unstructured":"Azadeh Farzan and Zachary Kincaid. 2018. Strategy synthesis for linear arithmetic games. Proc. ACM Program. Lang. POPL (2018). doi:10.1145\/3158149","DOI":"10.1145\/3158149"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","unstructured":"Azadeh Farzan Dominik Klumpp and Andreas Podelski. 2022. Sound sequentialization for concurrent program verification. In International Conference on Programming Language Design and Implementation PLDI 2022. doi:10.1145\/3519939.3523727","DOI":"10.1145\/3519939.3523727"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","unstructured":"Azadeh Farzan and Anthony Vandikas. 2020. Reductions for safety proofs. Proc. ACM Program. Lang. POPL (2020). doi:10.1145\/3371081","DOI":"10.1145\/3371081"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","unstructured":"Bernd Finkbeiner Christopher Hahn Jana Hofmann and Leander Tentrup. 2020. Realizing omega-regular Hyperproperties. In International Conference on Computer Aided Verification CAV 2020. doi:10.1007\/978-3-030-53291-8_4","DOI":"10.1007\/978-3-030-53291-8_4"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","unstructured":"Bernd Finkbeiner Markus N. Rabe and C\u00e9sar S\u00e1nchez. 2015. Algorithms for Model Checking HyperLTL and HyperCTL\u22c6. In International Conference on Computer Aided Verification CAV 2015. doi:10.1007\/978-3-319-21690-4_3","DOI":"10.1007\/978-3-319-21690-4_3"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","unstructured":"Giuseppe De Giacomo Paolo Felli Marco Montali and Giuseppe Perelli. 2021. HyperLDLf: a Logic for Checking Properties of Finite Traces Process Logs. In International Joint Conference on Artificial Intelligence IJCAI 2021. doi:10.24963\/IJCAI.2021\/256","DOI":"10.24963\/IJCAI.2021\/256"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","unstructured":"Vladimir Gladshtein Qiyuan Zhao Willow Ahrens Saman P. Amarasinghe and Ilya Sergey. 2024. Mechanised Hypersafety Proofs about Structured Data. Proc. ACM Program. Lang. PLDI (2024). doi:10.1145\/3656403","DOI":"10.1145\/3656403"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","unstructured":"Joseph A. Goguen and Jos\u00e9 Meseguer. 1982. Security Policies and Security Models. In Symposium on Security and Privacy SP 1982. doi:10.1109\/SP.1982.10014","DOI":"10.1109\/SP.1982.10014"},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","unstructured":"Ohad Goudsmid Orna Grumberg and Sarai Sheinvald. 2021. Compositional Model Checking for Multi-properties. In International Conference on Verification Model Checking and Abstract Interpretation VMCAI 2021. doi:10.1007\/978-3-030-67067-2_4","DOI":"10.1007\/978-3-030-67067-2_4"},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","unstructured":"Susanne Graf and Hassen Sa\u00efdi. 1997. Construction of Abstract State Graphs with PVS. In International Conference on Computer Aided Verification CAV 1997. doi:10.1007\/3-540-63166-6_10","DOI":"10.1007\/3-540-63166-6_10"},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","unstructured":"Marco Guarnieri Boris K\u00f6pf Jos\u00e9 F. Morales Jan Reineke and Andr\u00e9s S\u00e1nchez. 2020. Spectector: Principled Detection of Speculative Information Flows. In Symposium on Security and Privacy SP 2020. doi:10.1109\/SP40000.2020.00011","DOI":"10.1109\/SP40000.2020.00011"},{"key":"e_1_3_1_59_1","doi-asserted-by":"publisher","unstructured":"Jens Oliver Gutsfeld Arne Meier Christoph Ohrem and Jonni Virtema. 2022. Temporal Team Semantics Revisited. In Symposium on Logic in Computer Science LICS 2022. doi:10.1145\/3531130.3533360","DOI":"10.1145\/3531130.3533360"},{"key":"e_1_3_1_60_1","doi-asserted-by":"publisher","unstructured":"Jens Oliver Gutsfeld Markus M\u00fcller-Olm and Christoph Ohrem. 2020. Propositional Dynamic Logic for Hyperproperties. In International Conference on Concurrency Theory CONCUR 2020. doi:10.4230\/LIPICS.CONCUR.2020.50","DOI":"10.4230\/LIPICS.CONCUR.2020.50"},{"key":"e_1_3_1_61_1","doi-asserted-by":"publisher","unstructured":"Jens Oliver Gutsfeld Markus M\u00fcller-Olm and Christoph Ohrem. 2021. Automata and fixpoints for asynchronous hyperproperties. Proc. ACM Program. Lang. POPL (2021). doi:10.1145\/3434319","DOI":"10.1145\/3434319"},{"key":"e_1_3_1_62_1","doi-asserted-by":"publisher","unstructured":"Jens Oliver Gutsfeld Markus M\u00fcller-Olm and Christoph Ohrem. 2024. Deciding Asynchronous Hyperproperties for Recursive Programs. Proc. ACM Program. Lang. POPL (2024). doi:10.1145\/3632844","DOI":"10.1145\/3632844"},{"key":"e_1_3_1_63_1","doi-asserted-by":"publisher","unstructured":"Philippe Heim and Rayna Dimitrova. 2024. Solving Infinite-State Games via Acceleration. Proc. ACM Program. Lang. POPL (2024). doi:10.1145\/3632899","DOI":"10.1145\/3632899"},{"key":"e_1_3_1_64_1","doi-asserted-by":"publisher","unstructured":"Maurice Herlihy and Jeannette M. Wing. 1990. Linearizability: A Correctness Condition for Concurrent Objects. ACM Trans. Program. Lang. Syst. (1990). doi:10.1145\/78969.78972","DOI":"10.1145\/78969.78972"},{"key":"e_1_3_1_65_1","doi-asserted-by":"publisher","unstructured":"Tzu-Han Hsu Borzoo Bonakdarpour Bernd Finkbeiner and C\u00e9sar S\u00e1nchez. 2023. Bounded Model Checking for Asynchronous Hyperproperties. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS 2023. doi:10.1007\/978-3-031-30823-9_2","DOI":"10.1007\/978-3-031-30823-9_2"},{"key":"e_1_3_1_66_1","doi-asserted-by":"publisher","unstructured":"Marieke Huisman Pratik Worah and Kim Sunesen. 2006. A Temporal Logic Characterisation of Observational Determinism. In Computer Security Foundations Workshop CSFW 2006). doi:10.1109\/CSFW.2006.6","DOI":"10.1109\/CSFW.2006.6"},{"key":"e_1_3_1_67_1","doi-asserted-by":"publisher","unstructured":"Shachar Itzhaky Sharon Shoham and Yakir Vizel. 2024. Hyperproperty Verification as CHC Satisfiability. In European Symposium on Programming ESOP 2024. doi:10.1007\/978-3-031-57267-8_9","DOI":"10.1007\/978-3-031-57267-8_9"},{"key":"e_1_3_1_68_1","doi-asserted-by":"publisher","unstructured":"Andreas Krebs Arne Meier Jonni Virtema and Martin Zimmermann. 2018. Team Semantics for the Specification and Verification of Hyperproperties. In International Symposium on Mathematical Foundations of Computer Science MFCS 2018. doi:10.4230\/LIPICS.MFCS.2018.10","DOI":"10.4230\/LIPICS.MFCS.2018.10"},{"key":"e_1_3_1_69_1","doi-asserted-by":"publisher","unstructured":"Maurice Laveaux Wieger Wesselink and Tim A. C. Willemse. 2022. On-The-Fly Solving for Symbolic Parity Games. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS 2022. doi:10.1007\/978-3-030-99527-0_8","DOI":"10.1007\/978-3-030-99527-0_8"},{"key":"e_1_3_1_70_1","doi-asserted-by":"publisher","unstructured":"Xavier Leroy. 2006. Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In Symposium on Principles of Programming Languages POPL 2006. doi:10.1145\/1111037.1111042","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_3_1_71_1","doi-asserted-by":"publisher","unstructured":"Kenji Maillard Catalin Hritcu Exequiel Rivas and Antoine Van Muylder. 2020. The next 700 relational program logics. Proc. ACM Program. Lang. POPL (2020). doi:10.1145\/3371072","DOI":"10.1145\/3371072"},{"key":"e_1_3_1_72_1","doi-asserted-by":"crossref","unstructured":"Donald A Martin. 1975. Borel determinacy. Annals of Mathematics 2 (1975).","DOI":"10.2307\/1971035"},{"key":"e_1_3_1_73_1","doi-asserted-by":"publisher","unstructured":"Daryl McCullough. 1988. Noninterference and the composability of security properties. In Symposium on Security and Privacy SP 1997. doi:10.1109\/SECPRI.1988.8110","DOI":"10.1109\/SECPRI.1988.8110"},{"key":"e_1_3_1_74_1","doi-asserted-by":"publisher","unstructured":"John McLean. 1994. A general theory of composition for trace sets closed under selective interleaving functions. In Symposium on Security and Privacy SP 1994. doi:10.1109\/RISP.1994.296590","DOI":"10.1109\/RISP.1994.296590"},{"key":"e_1_3_1_75_1","doi-asserted-by":"publisher","unstructured":"Robert McNaughton. 1993. Infinite Games Played on Finite Graphs. Ann. Pure Appl. Logic (1993). doi:10.1016\/0168-0072(93)90036-D","DOI":"10.1016\/0168-0072(93)90036-D"},{"key":"e_1_3_1_76_1","unstructured":"Robin Milner. 1971. An Algebraic Definition of Simulation Between Programs. In International Joint Conference on Artificial Intelligence IJCAI 1971. http:\/\/ijcai.org\/Proceedings\/71\/Papers\/044.pdf"},{"key":"e_1_3_1_77_1","doi-asserted-by":"publisher","unstructured":"Kedar S. Namjoshi. 1997. A Simple Characterization of Stuttering Bisimulation. In Conference on Foundations of Software Technology and Theoretical Computer Science FSTTCS 1997. doi:10.1007\/BFB0058037","DOI":"10.1007\/BFB0058037"},{"key":"e_1_3_1_78_1","doi-asserted-by":"publisher","unstructured":"Kedar S. Namjoshi and Lucas M. Tabajara. 2020. Witnessing Secure Compilation. In International Conference on Verification Model Checking and Abstract Interpretation VMCAI 2020. doi:10.1007\/978-3-030-39322-9_1","DOI":"10.1007\/978-3-030-39322-9_1"},{"key":"e_1_3_1_79_1","doi-asserted-by":"publisher","unstructured":"Nir Piterman. 2007. From Nondeterministic B\u00fcchi and Streett Automata to Deterministic Parity Automata. Log. Methods Comput. Sci. (2007). doi:10.2168\/LMCS-3(3:5)2007","DOI":"10.2168\/LMCS-3(3:5)2007"},{"key":"e_1_3_1_80_1","doi-asserted-by":"publisher","unstructured":"Amir Pnueli. 1977. The Temporal Logic of Programs. In Symposium on Foundations of Computer Science FOCS 1977. doi:10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_1_81_1","unstructured":"Markus N. Rabe. 2016. A temporal logic approach to information-flow control. Ph. D. Dissertation. Saarland University."},{"key":"e_1_3_1_82_1","doi-asserted-by":"publisher","unstructured":"John H. Reif. 1984. The Complexity of Two-Player Games of Incomplete Information. J. Comput. Syst. Sci. (1984). doi:10.1016\/0022-0000(84)90034-5","DOI":"10.1016\/0022-0000(84)90034-5"},{"key":"e_1_3_1_83_1","doi-asserted-by":"publisher","unstructured":"Stanly Samuel Deepak D\u2019Souza and Raghavan Komondoor. 2021. GenSys: a scalable fixed-point engine for maximal controller synthesis over infinite state spaces. In Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering ESEC\/FSE 2021. doi:10.1145\/3468264.3473126","DOI":"10.1145\/3468264.3473126"},{"key":"e_1_3_1_84_1","doi-asserted-by":"publisher","unstructured":"Anne-Kathrin Schmuck Philippe Heim Rayna Dimitrova and Satya Prakash Nayak. 2024. Localized Attractor Computations for Infinite-State Games. In International Conference on Computer Aided Verification CAV 2024. doi:10.1007\/978-3-031-65633-0_7","DOI":"10.1007\/978-3-031-65633-0_7"},{"key":"e_1_3_1_85_1","doi-asserted-by":"publisher","unstructured":"Ron Shemer Arie Gurfinkel Sharon Shoham and Yakir Vizel. 2019. Property Directed Self Composition. In International Conference on Computer Aided Verification CAV 2019. doi:10.1007\/978-3-030-25540-4_9","DOI":"10.1007\/978-3-030-25540-4_9"},{"key":"e_1_3_1_86_1","doi-asserted-by":"publisher","unstructured":"Marcelo Sousa and Isil Dillig. 2016. Cartesian hoare logic for verifying k-safety properties. In Conference on Programming Language Design and Implementation PLDI 2016. doi:10.1145\/2908080.2908092","DOI":"10.1145\/2908080.2908092"},{"key":"e_1_3_1_87_1","doi-asserted-by":"publisher","unstructured":"Colin Stirling. 1995. Modal and Temporal Logics for Processes. In Logics for Concurrency-Structure versus Automata. doi:10.1007\/3-540-60915-6_5","DOI":"10.1007\/3-540-60915-6_5"},{"key":"e_1_3_1_88_1","doi-asserted-by":"publisher","unstructured":"Tachio Terauchi. 2008. A Type System for Observational Determinism. In Computer Security Foundations Symposium CSF 2008. doi:10.1109\/CSF.2008.9","DOI":"10.1109\/CSF.2008.9"},{"key":"e_1_3_1_89_1","doi-asserted-by":"publisher","unstructured":"Hiroshi Unno Tachio Terauchi and Eric Koskinen. 2021. Constraint-Based Relational Verification. In International Conference on Computer Aided Verification CAV 2021. doi:10.1007\/978-3-030-81685-8_35","DOI":"10.1007\/978-3-030-81685-8_35"},{"key":"e_1_3_1_90_1","doi-asserted-by":"publisher","unstructured":"Tom van Dijk. 2018. 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. doi:10.1007\/978-3-319-89960-2_16","DOI":"10.1007\/978-3-319-89960-2_16"},{"key":"e_1_3_1_91_1","doi-asserted-by":"publisher","unstructured":"Huanyu Wang Domenic Forte Mark M. Tehranipoor and Qihang Shi. 2017. Probing Attacks on Integrated Circuits: Challenges and Research Opportunities. IEEE Des. Test (2017). doi:10.1109\/MDAT.2017.2729398","DOI":"10.1109\/MDAT.2017.2729398"},{"key":"e_1_3_1_92_1","doi-asserted-by":"publisher","unstructured":"Steve Zdancewic and Andrew C. Myers. 2003. Observational Determinism for Concurrent Program Security. In Computer Security Foundations Workshop CSFW 2003. doi:10.1109\/CSFW.2003.1212703","DOI":"10.1109\/CSFW.2003.1212703"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763130","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:13:05Z","timestamp":1784196785000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763130"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":91,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763130"],"URL":"https:\/\/doi.org\/10.1145\/3763130","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-25","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}