{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:10:00Z","timestamp":1784844600766,"version":"3.55.0"},"reference-count":86,"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\/"}],"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>We design various logics for proving hyper properties of iterative programs by application of abstract interpretation principles.<\/jats:p>\n                  <jats:p>In part I, we design a generic, structural, fixpoint abstract interpreter parameterized by an algebraic abstract domain describing finite and infinite computations that can be instantiated for various operational, denotational, or relational program semantics. Considering semantics as program properties, we define a post algebraic transformer for execution properties (e.g. sets of traces) and a Post algebraic transformer for semantic (hyper) properties (e.g. sets of sets of traces), we provide corresponding calculuses as instances of the generic abstract interpreter, and we derive under and over approximation hyperlogics.<\/jats:p>\n                  <jats:p>In part II, we define exact and approximate semantic abstractions, and show that they preserve the mathematical structure of the algebraic semantics, the collecting semantics post, the hyper collecting semantics Post, and the hyperlogics.<\/jats:p>\n                  <jats:p>\n                    Since proofs by sound and complete hyperlogics require an exact characterization of the program semantics within the proof, we consider in part III abstractions of the (hyper) semantic properties that yield simplified proof rules. These abstractions include the join, the homomorphic, the elimination, the principal ideal, the order ideal, the frontier order ideal, and the chain limit algebraic abstractions, as well as their combinations, that lead to new algebraic generalizations of hyperlogics, including the\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mrow>\n                          <mml:mo>\u2200<\/mml:mo>\n                          <mml:msup>\n                            <mml:mo>\u2203<\/mml:mo>\n                            <mml:mtext>*<\/mml:mtext>\n                          <\/mml:msup>\n                          <mml:mo>,<\/mml:mo>\n                          <mml:mo>\u2200<\/mml:mo>\n                          <mml:msup>\n                            <mml:mo>\u2200<\/mml:mo>\n                            <mml:mtext>*<\/mml:mtext>\n                          <\/mml:msup>\n                        <\/mml:mrow>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    , and\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mrow>\n                          <mml:mo>\u2203<\/mml:mo>\n                          <mml:msup>\n                            <mml:mo>\u2200<\/mml:mo>\n                            <mml:mtext>*<\/mml:mtext>\n                          <\/mml:msup>\n                        <\/mml:mrow>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    hyperlogics.\n                  <\/jats:p>","DOI":"10.1145\/3704852","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"446-478","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Calculational Design of Hyperlogics by Abstract Interpretation"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0101-9953","authenticated-orcid":false,"given":"Patrick","family":"Cousot","sequence":"first","affiliation":[{"name":"New York University, New York, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-4885-8268","authenticated-orcid":false,"given":"Jeffery","family":"Wang","sequence":"additional","affiliation":[{"name":"New York University, New York, USA"}],"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.1016\/0168-0072(91)90065-T"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71120-0"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571213"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/6490.6494"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009889"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57249-4_10"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_17"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-19(2:13)2023"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37703-7_15"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.5555\/3635637.3662865"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/b139095"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/9758.10501"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54792-8_15"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.3233\/JCS-2009-0393"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_7"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/800214.806556"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-08921-7_53"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00313-3"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45260-5_1"},{"key":"e_1_3_2_21_2","volume-title":"Principles of Abstract Interpretation","author":"Cousot Patrick","year":"2021","unstructured":"Patrick Cousot. 2021. Principles of Abstract Interpretation (1 ed.). MIT Press.","edition":"1"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632849"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632849"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1979.82.43"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143184"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60045-0_58"},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2008.03.025"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103687"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384633"},{"key":"e_1_3_2_30_2","doi-asserted-by":"crossref","unstructured":"Thibault Dardinier. 2024. Formalization of Hyper Hoare Logic: A Logic to (Dis-)Prove Program Hyperproperties. Arch. Formal Proofs 2023. https:\/\/www.isa-afp.org\/entries\/HyperHoareLogic.html","DOI":"10.1145\/3656437"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3656437"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511809088"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24690-6_12"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1142\/S012905410200114X"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4020-1898-5"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-21037-2_4"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0014657"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-11157-3_38"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023555514029"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2023.105077"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CONCUR.2016.13"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.TCS.2004.12.021"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1145\/3175660"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/3649309"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(74)80028-0"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.5555\/547173"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-08353-7_183"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1982.10014"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1984.10019"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1145\/321992.321997"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-08921-7_73"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90182-S"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(90)90018-9"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-8596-5"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(98)00027-6"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1145\/27651.27653"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39698-4_13"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44584-6_1"},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.SCICO.2013.08.012"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.1145\/368924.368930"},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256195"},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","DOI":"10.1145\/343369.343378"},{"key":"e_1_3_2_65_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2007.12.004"},{"key":"e_1_3_2_66_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00288637"},{"key":"e_1_3_2_67_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66706-5_12"},{"key":"e_1_3_2_68_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99725-4_17"},{"key":"e_1_3_2_69_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-44245-2_19"},{"key":"e_1_3_2_70_2","doi-asserted-by":"publisher","DOI":"10.1109\/SP.1987.10009"},{"key":"e_1_3_2_71_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.481534"},{"key":"e_1_3_2_72_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-88701-8_20"},{"key":"e_1_3_2_73_2","volume-title":"Introduction to Set Theory","author":"Monk James Donald","year":"1969","unstructured":"James Donald Monk. 1969. Introduction to Set Theory. McGraw\u2013Hill. http:\/\/euclid.colorado.edu\/~monkd\/monk11.pdf"},{"key":"e_1_3_2_74_2","volume-title":"Abstract interpretation and optimising transformations for applicative programs","author":"Mycroft Alan","year":"1982","unstructured":"Alan Mycroft. 1982. Abstract interpretation and optimising transformations for applicative programs. Ph. D. Dissertation. University of Edinburgh, UK. https:\/\/hdl.handle.net\/1842\/6602"},{"key":"e_1_3_2_75_2","first-page":"17","volume-title":"IFIP Congress","author":"Nivat Maurice","year":"1980","unstructured":"Maurice Nivat. 1980. Non Deterministic Programs: An Algebraic Overview. In IFIP Congress. North-Holland\/IFIP, 17\u201328."},{"key":"e_1_3_2_76_2","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_3_2_77_2","doi-asserted-by":"publisher","DOI":"10.2307\/1968978"},{"key":"e_1_3_2_78_2","unstructured":"David Michael Ritchie Park. 1969. Fixpoint Induction and Proofs of Program Properties. In Machine Intelligence Volume 5 Donald Mitchie and Bernard Meltzer (Eds.). Edinburgh Univ. Press Chapter 3 59\u201378."},{"key":"e_1_3_2_79_2","doi-asserted-by":"publisher","DOI":"10.1137\/0205035"},{"key":"e_1_3_2_80_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.ENTCS.2015.12.021"},{"key":"e_1_3_2_81_2","first-page":"49","volume-title":"Towards a Mathematical Semantics for Computer Languages. Technical Report PRG-6","author":"Scott Dana S.","year":"1971","unstructured":"Dana S. Scott and Christopher Strachey. 1971. Towards a Mathematical Semantics for Computer Languages. Technical Report PRG-6. Oxford University Computer Laboratory. 49 pages. https:\/\/www.cs.ox.ac.uk\/files\/3228\/PRG06.pdf"},{"key":"e_1_3_2_82_2","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_3_2_83_2","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2312.09662"},{"key":"e_1_3_2_84_2","doi-asserted-by":"publisher","DOI":"10.2307\/1968865"},{"key":"e_1_3_2_85_2","doi-asserted-by":"publisher","DOI":"10.1145\/3527316"},{"key":"e_1_3_2_86_2","doi-asserted-by":"publisher","DOI":"10.1145\/2049706.2049708"},{"key":"e_1_3_2_87_2","doi-asserted-by":"publisher","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\/10.1145\/3704852","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704852","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:16:07Z","timestamp":1770200167000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704852"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":86,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704852"],"URL":"https:\/\/doi.org\/10.1145\/3704852","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-08","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"}}]}}