{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:42:58Z","timestamp":1780994578948,"version":"3.54.1"},"reference-count":40,"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\/100000181","name":"AFOSR","doi-asserted-by":"crossref","award":["FA9550-23-1-0544"],"award-info":[{"award-number":["FA9550-23-1-0544"]}],"id":[{"id":"10.13039\/100000181","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,1,7]]},"abstract":"<jats:p>\n                    We study \u201c\n                    <jats:italic toggle=\"yes\">the best of abstract interpretations<\/jats:italic>\n                    \u201d, that is, the best possible abstract interpretations of programs. Abstract interpretations are inductively defined by composing abstract transfer functions for the basic commands, such as assignments and Boolean guards. However, abstract interpretation is not compositional: even if the abstract transfer functions of the basic commands are the best possible ones on a given abstract domain\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mi>A<\/mml:mi>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    this does not imply that the whole inductive abstract interpretation of a program\n                    <jats:monospace>p<\/jats:monospace>\n                    is still the best in\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mi>A<\/mml:mi>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    . When this happens we are in the optimal scenario where the abstract interpretation of\n                    <jats:monospace>p<\/jats:monospace>\n                    coincides with the abstraction of the concrete interpretation of\n                    <jats:monospace>p<\/jats:monospace>\n                    . Our main contributions are threefold. Firstly, we investigate the computability properties of the class of programs having the best possible abstract interpretation on a fixed abstract domain\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mi>A<\/mml:mi>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    . We show that this class is, in general, not straightforward and not recursive. Secondly, we prove the impossibility of achieving the best possible abstract interpretation of any program\n                    <jats:monospace>p<\/jats:monospace>\n                    either by an effective compilation of\n                    <jats:monospace>p<\/jats:monospace>\n                    or by minimally refining or simplifying the abstract domain\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mi>A<\/mml:mi>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    . These results show that the program property of having the best possible abstract interpretation is not trivial and, in general, hard to achieve. We then show how to prove that the abstract interpretation of a program is indeed the best possible one. To this aim, we put forward a program logic parameterized on an abstract domain\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mi>A<\/mml:mi>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    which infers triples\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mrow>\n                          <mml:mfenced close=\"[\" open=\"[\">\n                            <mml:mrow>\n                              <mml:mi>p<\/mml:mi>\n                              <mml:mi>r<\/mml:mi>\n                              <mml:mi>e<\/mml:mi>\n                              <mml:msub>\n                                <mml:mo>]<\/mml:mo>\n                                <mml:mi>A<\/mml:mi>\n                              <\/mml:msub>\n                              <mml:mspace width=\"0.2em\"\/>\n                              <mml:mtext>p<\/mml:mtext>\n                              <mml:mspace width=\"0.2em\"\/>\n                            <\/mml:mrow>\n                          <\/mml:mfenced>\n                          <mml:mi>p<\/mml:mi>\n                          <mml:mi>o<\/mml:mi>\n                          <mml:mi>s<\/mml:mi>\n                          <mml:mi>t<\/mml:mi>\n                          <mml:msub>\n                            <mml:mo>]<\/mml:mo>\n                            <mml:mi>A<\/mml:mi>\n                          <\/mml:msub>\n                        <\/mml:mrow>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    . These triples encode that the inductive abstract interpretation of\n                    <jats:monospace>p<\/jats:monospace>\n                    on\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mi>A<\/mml:mi>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    with abstract input\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mrow>\n                          <mml:mi>p<\/mml:mi>\n                          <mml:mi>r<\/mml:mi>\n                          <mml:mi>e<\/mml:mi>\n                          <mml:mo>\u2208<\/mml:mo>\n                          <mml:mi>A<\/mml:mi>\n                        <\/mml:mrow>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    gives\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mrow>\n                          <mml:mi>p<\/mml:mi>\n                          <mml:mi>o<\/mml:mi>\n                          <mml:mi>s<\/mml:mi>\n                          <mml:mi>t<\/mml:mi>\n                          <mml:mo>\u2208<\/mml:mo>\n                          <mml:mi>A<\/mml:mi>\n                        <\/mml:mrow>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    as abstract output and this is the best possible in\n                    <jats:inline-formula>\n                      <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                        <mml:mi>A<\/mml:mi>\n                      <\/mml:math>\n                    <\/jats:inline-formula>\n                    .\n                  <\/jats:p>","DOI":"10.1145\/3704882","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1355-1385","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["The Best of Abstract Interpretations"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9582-3960","authenticated-orcid":false,"given":"Roberto","family":"Giacobazzi","sequence":"first","affiliation":[{"name":"University of Arizona, Tucson, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0159-0068","authenticated-orcid":false,"given":"Francesco","family":"Ranzato","sequence":"additional","affiliation":[{"name":"University of Padova, Padova, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371096"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470608"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523453"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3582267"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876643"},{"key":"e_1_3_2_8_1","volume-title":"Principles of Abstract Interpretation","author":"Cousot Patrick","year":"2021","unstructured":"Patrick Cousot. 2021. Principles of Abstract Interpretation. MIT Press."},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384633"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_8"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290355"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/234528.234742"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00007-3"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(79)90046-1"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676987"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-47764-0_20"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61055-3_34"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63165-8_230"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14162-1_18"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2014.02.003"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055786"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333989"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1042038.1042040"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_15"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268497"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256195"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8609-1"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000034"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_3"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_21"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_1"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.2307\/1990888"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/28907"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008725524946"},{"key":"e_1_3_2_38_1","volume-title":"Recursively Enumerable Sets and Degrees","author":"Soare Robert I.","year":"1980","unstructured":"Robert I. Soare. 1980. Recursively Enumerable Sets and Degrees. Springer-Verlag."},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_17"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","unstructured":"Mark N. Wegman and F. Kenneth Zadeck. 1991. Constant propagation with conditional branches. ACM Transactions on Programming Languages and Systems 13 2 (1991) 181\u2013210. https:\/\/doi.org\/10.1145\/103135.103136 10.1145\/103135.103136","DOI":"10.1145\/103135.103136"},{"key":"e_1_3_2_41_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\/3704882","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704882","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:14:03Z","timestamp":1770200043000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704882"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":40,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704882"],"URL":"https:\/\/doi.org\/10.1145\/3704882","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-10","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"}}]}}