{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:06:50Z","timestamp":1784844410604,"version":"3.55.0"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"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"],"award-info":[{"award-number":["101055412"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>\n                    Temporal logics for hyperproperties have recently emerged as an expressive specification technique for relational properties of reactive systems. While the model checking problem for such logics has been widely studied, there is a scarcity of deductive proof systems for temporal hyperproperties. In particular, hyperproperties with an alternation of universal and existential quantification over system executions are rarely supported. In this paper, we focus on hyperproperties of the form \u2200\n                    <jats:sup>*<\/jats:sup>\n                    \u2203\n                    <jats:sup>*<\/jats:sup>\n                    <jats:italic toggle=\"yes\">\u03c8<\/jats:italic>\n                    , where\n                    <jats:italic toggle=\"yes\">\u03c8<\/jats:italic>\n                    is a safety relation. We show that hyperproperties of this class - which includes many hyperliveness properties of interest - can always be approximated by coinductive relations. This enables intuitive proofs by coinduction. Based on this observation, we define\n                    <jats:sc>HyCo<\/jats:sc>\n                    (\n                    <jats:bold>Hy<\/jats:bold>\n                    perproperties,\n                    <jats:bold>Co<\/jats:bold>\n                    inductively), a mechanized framework to reason about temporal hyperproperties within the Coq proof assistant. We detail the construction of HyCo, provide a proof of its soundness, and exemplify its use by applying it to the verification of reactive systems modeled as imperative programs with nondeterminism and I\/O.\n                  <\/jats:p>","DOI":"10.1145\/3704889","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1568-1595","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Coinductive Proofs for Temporal Hyperliveness"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2307-2296","authenticated-orcid":false,"given":"Arthur","family":"Correnson","sequence":"first","affiliation":[{"name":"CISPA Helmholtz Center for Information Security, Saarbruecken, 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, Saarbruecken, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796819000145"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062378"},{"key":"e_1_3_2_4_2","first-page":"249","volume-title":"Principles of model checking.","author":"Baier Christel","year":"2008","unstructured":"Christel Baier and Joost-Pieter Katoen . 2008. Principles of model checking. MIT Press, 249\u2013253."},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35722-0_3"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158145"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480894"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371089"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/2492061"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57249-4_10"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF54842.2022.9919658"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_17"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30823-9_8"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/321239.321249"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622857"},{"key":"e_1_3_2_17_2","first-page":"265","article-title":"Temporal Logics for Hyperproperties","author":"Clarkson Michael R.","year":"2014","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 Proc. POST. 265\u2013284.","journal-title":"Proc. POST"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2008.7"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_7"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","unstructured":"Arthur Correnson . 2024. Coinductive Proofs for Temporal Hyperliveness. https:\/\/doi.org\/10.5281\/zenodo.14055009 10.5281\/zenodo.14055009","DOI":"10.5281\/zenodo.14055009"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656437"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-21037-2_4"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","unstructured":"Emanuele D'Osualdo Azadeh Farzan and Derek Dreyer . 2022. Proving hypersafety compositionally. Proc. ACM Program. Lang. 6 OOPSLA2 Article 135 (oct 2022) 26 pages. https:\/\/doi.org\/10.1145\/3563298 10.1145\/3563298","DOI":"10.1145\/3563298"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_31"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_11"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371081"},{"key":"e_1_3_2_27_2","article-title":"Algorithms for Model Checking HyperLTL and HyperCTL*","author":"Finkbeiner Bernd","year":"2015","unstructured":"Bernd Finkbeiner , Markus N. Rabe , and Cesar Sanchez . 2015. Algorithms for Model Checking HyperLTL and HyperCTL*. In Proc. CAV, 2015.","journal-title":"Proc. CAV, 2015"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498689"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72016-2_6"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429093"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF51468.2021.00012"},{"key":"e_1_3_2_33_2","first-page":"79","article-title":"A General Theory of Composition for Trace Sets Closed Under Selective Interleaving Functions","author":"McLean John","year":"1994","unstructured":"John McLean . 1994. A General Theory of Composition for Trace Sets Closed Under Selective Interleaving Functions. In Proc. IEEE Symposium on Security and Privacy. 79\u201393.","journal-title":"Proc. IEEE Symposium on Security and Privacy"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-61470-6_7"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-76637-7_24"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934564"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511792588.007"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","unstructured":"Ron Shemer Arie Gurfinkel Sharon Shoham and Yakir Vizel . 2019. Property Directed Self Composition. In Computer Aided Verification - 31st International Conference CAV 2019 New York City NY USA July 15-18 2019 Proceedings Part I (Lecture Notes in Computer Science Vol. 11561) Isil Dillig and Serdar Tasiran (Eds.). Springer 161\u2013179. https:\/\/doi.org\/10.1007\/978-3-030-25540-4_9 10.1007\/978-3-030-25540-4_9","DOI":"10.1007\/978-3-030-25540-4_9"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/2980983.2908092"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-15579-1_22"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290346"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.036"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373813"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704889","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704889","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:14:58Z","timestamp":1770200098000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704889"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":43,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704889"],"URL":"https:\/\/doi.org\/10.1145\/3704889","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}