{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T09:32:50Z","timestamp":1787563970696,"version":"build-2736575974"},"reference-count":68,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001711","name":"Swiss National Science Foundation","doi-asserted-by":"crossref","award":["197065"],"award-info":[{"award-number":["197065"]}],"id":[{"id":"10.13039\/501100001711","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":[[2024,6,20]]},"abstract":"<jats:p>\n                    Hoare logics are proof systems that allowone to formally establish properties of computer programs. Traditional Hoare logics prove properties of individual program executions (such as functional correctness). Hoare logic has been generalized to prove also properties of multiple executions of a program (so-called hyperproperties, such as determinism or non-interference). These program logics prove the\n                    <jats:italic toggle=\"yes\">absence<\/jats:italic>\n                    of (bad combinations of) executions. On the other hand, program logics similar to Hoare logic have been proposed to\n                    <jats:italic toggle=\"yes\">disprove<\/jats:italic>\n                    program properties (e.g., Incorrectness Logic), by proving the\n                    <jats:italic toggle=\"yes\">existence<\/jats:italic>\n                    of (bad combinations of) executions. All of these logics have in common that they specify program properties using assertions over a fixed number of states, for instance, a single pre- and post-state for functional properties or pairs of pre- and post-states for non-interference.\n                  <\/jats:p>\n                  <jats:p>\n                    In this paper, we present Hyper Hoare Logic, a generalization of Hoare logic that lifts assertions to properties of arbitrary\n                    <jats:italic toggle=\"yes\">sets<\/jats:italic>\n                    of states. The resulting logic is simple yet expressive: its judgments can express arbitrary\n                    <jats:italic toggle=\"yes\">program hyperproperties<\/jats:italic>\n                    , a particular class of hyperproperties over the set of terminating executions of a program (including properties of individual program executions). By allowing assertions to reason about sets of states, Hyper Hoare Logic can reason about both the\n                    <jats:italic toggle=\"yes\">absence<\/jats:italic>\n                    and the\n                    <jats:italic toggle=\"yes\">existence<\/jats:italic>\n                    of (combinations of) executions, and, thereby, supports both proving and disproving program (hyper-)properties within the same logic, including (hyper-)properties that no existing Hoare logic can express. We prove that Hyper Hoare Logic\n\t\t\tis sound and complete, and demonstrate that it captures important proof principles naturally. All our technical results have been proved in Isabelle\/HOL.\n                  <\/jats:p>","DOI":"10.1145\/3656437","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T12:27:20Z","timestamp":1718886440000},"page":"1485-1509","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":27,"title":["Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2719-4856","authenticated-orcid":false,"given":"Thibault","family":"Dardinier","sequence":"first","affiliation":[{"name":"ETH Zurich, Z\u00fcrich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7001-2566","authenticated-orcid":false,"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[{"name":"ETH Zurich, Z\u00fcrich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110265"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111320.1111046"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571213"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009889"},{"key":"e_1_3_1_6_1","doi-asserted-by":"crossref","unstructured":"Gilles Barthe Juan Manuel Crespo C\u00e9sar Kunz. 2011a. Relational Verification Using Product Programs. In International Symposium on Formal Methods 200\u2013214.","DOI":"10.1007\/978-3-642-21437-0_17"},{"key":"e_1_3_1_7_1","doi-asserted-by":"crossref","unstructured":"Gilles Barthe Juan Manuel Crespo C\u00e9sar Kunz. 2013. Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification. In International Symposium on Logical Foundations of Computer Science 29\u201343.","DOI":"10.1007\/978-3-642-35722-0_3"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000193"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2019.8894277"},{"key":"e_1_3_1_10_1","doi-asserted-by":"crossref","unstructured":"Gilles Barthe Thomas Espitau Marco Gaboardi Benjamin Gr\u00e9goire Justin Hsu Pierre-Yves Strub. 2018. An Assertion-Based Program Logic for Probabilistic Programs. In European Symposium on Programming 117\u2013144.","DOI":"10.1007\/978-3-319-89884-1_5"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2014.36"},{"key":"e_1_3_1_12_1","doi-asserted-by":"crossref","unstructured":"Gilles Barthe Benjamin Gr\u00e9goire Santiago Zanella B\u00e9guelin. 2009. Formal Certification of Code-Based Cryptographic Proofs. In Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 90\u2013101.","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371123"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_17"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30823-9_8"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276514"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","unstructured":"Roberto Bruni Roberto Giacobazzi Roberta Gori Francesco Ranzato. 2021. A Logic for Locally Complete Abstract Interpretations. In 2021 36th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS) 1\u201313. https:\/\/doi.org\/10.1109\/LICS52264.2021.9470608 10.1109\/LICS52264.2021.9470608","DOI":"10.1109\/LICS52264.2021.9470608"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3582267"},{"key":"e_1_3_1_20_1","doi-asserted-by":"crossref","unstructured":"Michael R Clarkson Bernd Finkbeiner Masoud Koleini Kristopher K Micinski Markus N Rabe C\u00e9sar S\u00e1nchez. 2014. Temporal Logics for Hyperproperties. In International Conference on Principles of Security and Trust 265\u2013284.","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","unstructured":"Michael R. Clarkson Fred B. Schneider. 2008. Hyperproperties. In 21st IEEE Computer Security Foundations Symposium 51\u201365. https:\/\/doi.org\/10.1109\/CSF.2008.7 10.1109\/CSF.2008.7","DOI":"10.1109\/CSF.2008.7"},{"key":"e_1_3_1_22_1","doi-asserted-by":"crossref","unstructured":"Norine Coenen Bernd Finkbeiner C\u00e9sar S\u00e1nchez Leander Tentrup. 2019. Verifying Hyperliveness. In International Conference on Computer Aided Verification 121\u2013139.","DOI":"10.1007\/978-3-030-25540-4_7"},{"key":"e_1_3_1_23_1","doi-asserted-by":"crossref","unstructured":"Ricardo Corin Jerry Den Hartog. 2006. A Probabilistic Hoare-Style Logic for Game-Based Cryptographic Proofs. In International Colloquium on Automata Languages and Programming 252\u2013263.","DOI":"10.1007\/11787006_22"},{"key":"e_1_3_1_24_1","doi-asserted-by":"crossref","unstructured":"David Costanzo Zhong Shao. 2014. A Separation Logic for Enforcing Declarative Information Flow Control Policies. In Principles of Security and Trust Mart\u00edn Abadi and Steve Kremer (Eds.) 179\u2013198.","DOI":"10.1007\/978-3-642-54792-8_10"},{"key":"e_1_3_1_25_1","doi-asserted-by":"crossref","unstructured":"Patrick Cousot Radhia Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages 238\u2013252.","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_1_26_1","unstructured":"Thibault Dardinier. 2023. Formalization of Hyper Hoare Logic: A Logic to (Dis-)Prove Program Hyperproperties. Archive of Formal Proofs (April 2023). https:\/\/isa-afp.org\/entries\/HyperHoareLogic.html Formal proof development."},{"key":"e_1_3_1_27_1","unstructured":"Thibault Dardinier Peter M\u00fcller. 2023. Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (Extended Version). arXiv:cs.LO\/2301.10037."},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","unstructured":"Thibault Dardinier Peter M\u00fcller. 2024. Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (Artifact). https:\/\/doi.org\/10.5281\/zenodo.10808236 10.5281\/zenodo.10808236.","DOI":"10.5281\/zenodo.10808236"},{"key":"e_1_3_1_29_1","doi-asserted-by":"crossref","unstructured":"Edsko de Vries Vasileios Koutavas. 2011. Reverse Hoare Logic. In Software Engineering and Formal Methods Gilles Barthe Alberto Pardo and Gerardo Schneider (Eds.) 155\u2013171.","DOI":"10.1007\/978-3-642-24690-6_12"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1142\/S012905410200114X"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","unstructured":"Robert Dickerson Qianchuan Ye Michael K. Zhang Benjamin Delaware. 2022. RHLE: Modular Deductive Verification of Relational \u2200\u2203 Properties. In Programming Languages and Systems: 20th Asian Symposium APLAS 2022 Auckland New Zealand December 5 2022 Proceedings (Auckland New Zealand) 67\u201387. https:\/\/doi.org\/10.1007\/978-3-031-21037-2_410.1007\/978-3-031-21037-2_4","DOI":"10.1007\/978-3-031-21037-2_4"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338112"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563298"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591289"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3324783"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_13"},{"key":"e_1_3_1_37_1","doi-asserted-by":"crossref","unstructured":"Robert W. Floyd. 1967. Assigning Meanings to Programs. Proceedings of Symposium in Applied Mathematics 19\u201332.","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00264278"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290370"},{"key":"e_1_3_1_40_1","doi-asserted-by":"crossref","unstructured":"David Harel. 1979. First-Order Dynamic Logic. Springer.","DOI":"10.1007\/3-540-09237-4"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_1_42_1","doi-asserted-by":"crossref","unstructured":"Tzu-Han Hsu S\u00e1nchezC\u00e9sar BonakdarpourBorzoo. 2021. Bounded Model Checking for Hyperproperties. In Tools and Algorithms for the Construction and Analysis of Systems Jan Friso Groote and Kim Guldstrand Larsen (Eds.) 94\u2013112. Springer International Publishing Cham.","DOI":"10.1007\/978-3-030-72016-2_6"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050057"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527325"},{"key":"e_1_3_1_45_1","unstructured":"K. Rustan M. Leino. 2008. This is Boogie 2. June 2008. https:\/\/www.microsoft.com\/en-us\/research\/publication\/this-is-boogie-2-2\/"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371072"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2023.19"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1987.10009"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.481534"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-88701-8_20"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","unstructured":"Toby Murray. 2020. An Under-Approximate Relational Logic: Heralding Logics of Insecurity Incorrect Implementation and More. https:\/\/doi.org\/10.48550\/ARXIV.2003.04791 10.48550\/ARXIV.2003.04791","DOI":"10.48550\/ARXIV.2003.04791"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61470-6_7"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31038-7_3"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","unstructured":"Michele Pasqua. 2019. Hyper Static Analysis of Programs \u2013 An Abstract Interpretation-Based Framework for Hyperproperties Verification. PhD thesis University of Verona. https:\/\/doi.org\/10.5281\/zenodo.6584085 10.5281\/zenodo.6584085","DOI":"10.5281\/zenodo.6584085"},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_14"},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498695"},{"key":"e_1_3_1_59_1","unstructured":"Lyle Harold Ramshaw. 1979. Formalizing the Analysis of Algorithms. PhD thesis Stanford University."},{"key":"e_1_3_1_60_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.021"},{"key":"e_1_3_1_61_1","doi-asserted-by":"publisher","DOI":"10.1002\/j.1538-7305.1948.tb01338.x"},{"key":"e_1_3_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00596-1_21"},{"key":"e_1_3_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908092"},{"key":"e_1_3_1_64_1","doi-asserted-by":"crossref","unstructured":"Tachio Terauchi Alex Aiken. 2005. Secure Information Flow as a Safety Problem. In International Static Analysis Symposium. 352\u2013367.","DOI":"10.1007\/11547662_24"},{"key":"e_1_3_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81685-8_35"},{"key":"e_1_3_1_66_1","doi-asserted-by":"publisher","DOI":"10.5555\/353629.353648"},{"key":"e_1_3_1_67_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.036"},{"key":"e_1_3_1_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15497-3_22"},{"key":"e_1_3_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586045"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656437","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656437","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T16:38:47Z","timestamp":1751647127000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656437"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":68,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656437"],"URL":"https:\/\/doi.org\/10.1145\/3656437","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}