{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T14:14:24Z","timestamp":1784211264275,"version":"3.55.0"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T00:00:00Z","timestamp":1767830400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","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"}]},{"name":"European Union - NextGenerationEU","award":["PE00000014"],"award-info":[{"award-number":["PE00000014"]}]},{"DOI":"10.13039\/501100001665","name":"French National Research Agency","doi-asserted-by":"crossref","award":["ANR-23-PEIA-0006"],"award-info":[{"award-number":["ANR-23-PEIA-0006"]}],"id":[{"id":"10.13039\/501100001665","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":[[2026,1,8]]},"abstract":"<jats:p>\n                    In numerical analysis, error propagation refers to how small inaccuracies in input data or intermediate computations accumulate and affect the final result, typically governed by the stability and sensitivity of the algorithm with respect to some perturbations. The definition of a similar concept in approximated program analysis is still a challenge. In abstract interpretation, inaccuracy arises from the abstraction itself, and the propagation of this error is dictated by the abstract interpreter. In most cases, such imprecision is inevitable. In this paper we introduce a logic for deriving (upper) bounds on the inaccuracy of an abstract interpretation. We are able to derive a function that bounds the imprecision of the result of an abstract interpreter from the imprecision of its input data. When this holds we have what we call partial local completeness of the abstract interpreter, a weaker form of completeness known in the literature. To this end, we introduce the notion of a\n                    <jats:italic toggle=\"yes\">generator<\/jats:italic>\n                    for a property represented in the abstract domain. Generators allow us to restrict the search space when verifying whether the bounding function holds for a given program and input. We then introduce a program logic, called\n                    <jats:italic toggle=\"yes\">Error Propagation Logic<\/jats:italic>\n                    (EPL), for propagating the error bounds produced by an abstract interpretation. This logic is a combination of correctness and incorrectness logics and a logic for\n                    <jats:italic toggle=\"yes\">program<\/jats:italic>\n                    <jats:italic toggle=\"yes\">\u03c9<\/jats:italic>\n                    -\n                    <jats:italic toggle=\"yes\">continuity<\/jats:italic>\n                    that is also introduced in this paper.\n                  <\/jats:p>","DOI":"10.1145\/3776707","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"1876-1904","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["A Logic for the Imprecision of Abstract Interpretations"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1099-3494","authenticated-orcid":false,"given":"Marco","family":"Campion","sequence":"first","affiliation":[{"name":"Inria - ENS - Universit\u00e9 PSL, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2761-4347","authenticated-orcid":false,"given":"Mila","family":"Dalla Preda","sequence":"additional","affiliation":[{"name":"University of Verona, Verona, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9582-3960","authenticated-orcid":false,"given":"Roberto","family":"Giacobazzi","sequence":"additional","affiliation":[{"name":"University of Arizona, Tucson, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8127-9642","authenticated-orcid":false,"given":"Caterina","family":"Urban","sequence":"additional","affiliation":[{"name":"Inria - ENS- Universit\u00e9 PSL, Paris, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470608"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523453"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3582267"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632897"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-032-07106-4_11"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498721"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-44245-2_7"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45260-5_4"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2025113.2025131"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00313-3"},{"key":"e_1_3_2_12_1","volume-title":"Principles of Abstract Interpretation","author":"Cousot Patrick","year":"2021","unstructured":"Patrick Cousot. 2021. Principles of Abstract Interpretation. The MIT Press, Cambridge, Mass."},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/390019.808314"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498680"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498692"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009890"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04295-9"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45142-0_9"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/234528.234742"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00058"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676987"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-47764-0_20"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61735-3_16"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1006\/INCO.1998.2724"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333989"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31954-2_19"},{"key":"e_1_3_2_30_1","volume-title":"Convex polytopes","author":"Gr\u00fcnbaum Branko","year":"1967","unstructured":"Branko Gr\u00fcnbaum, Victor Klee, Micha A Perles, and Geoffrey Colin Shephard. 1967. Convex polytopes. Vol. 16. Springer."},{"issue":"1969","key":"e_1_3_2_31_1","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","article-title":"An Axiomatic Basis for Computer Programming","volume":"10","author":"Hoare C. A. R.","year":"1969","unstructured":"C. A. R. Hoare. 1969. An Axiomatic Basis for Computer Programming. Commun. ACM 12, 10 (1969), 576-580. doi:10.1145\/ 363235.363259","journal-title":"Commun. ACM 12"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-38828-6_4"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689744"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256195"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689797"},{"key":"e_1_3_2_36_1","article-title":"Towards a Quantitative Estimation of Abstract Interpretations","author":"Logozzo Francesco","year":"2009","unstructured":"Francesco Logozzo. 2009. Towards a Quantitative Estimation of Abstract Interpretations. In Workshop on Quantitative Analysis of Software (workshop on quantitative analysis of software ed.). Microsoft. https:\/\/www.microsoft.com\/en-us\/research\/publication\/towards-a-quantitative-estimation-of-abstract-interpretations\/","journal-title":"Workshop on Quantitative Analysis of Software"},{"key":"e_1_3_2_37_1","first-page":"7469","article-title":"Explanations for Monotonic Classifiers","author":"Marques-Silva Jo\u00e3o","year":"2021","unstructured":"Jo\u00e3o Marques-Silva, Thomas Gerspacher, Martin C.Cooper, Alexey Ignatiev, and Nina Narodytska. 2021. Explanations for Monotonic Classifiers. In Proceedings of the 38th International Conference on Machine Learning, ICML 2021, 18\u201324 July 2021, Virtual Event (Proceedings of Machine Learning Research, Vol. 139), Marina Meila and Tong Zhang (Eds.). PMLR, 7469\u20137479. http:\/\/proceedings.mlr.press\/v139\/marques-silva21a.html","journal-title":"Proceedings of the 38th International Conference on Machine Learning, ICML 2021, 18\u201324 July 2021, Virtual Event (Proceedings of Machine Learning Research, Vol. 139)"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8609-1"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000034"},{"key":"e_1_3_2_40_1","first-page":"807","volume-title":"Proceedings of the 27th International Conference on Machine Learning (ICML-10), June 21-24, 2010, Haifa, Israel","author":"Nair Vinod","year":"2010","unstructured":"Vinod Nair and Geoffrey E. Hinton. 2010. Rectified Linear Units Improve Restricted Boltzmann Machines. In Proceedings of the 27th International Conference on Machine Learning (ICML-10), June 21-24, 2010, Haifa, Israel, Johannes F\u00fcrnkranz and Thorsten Joachims (Eds.). Omnipress, 807\u2013814. https:\/\/icml.cc\/Conferences\/2010\/papers\/432.pdf"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371078"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863568"},{"key":"e_1_3_2_43_1","volume-title":"Introduction to static analysis: an abstract interpretation perspective","author":"Rival Xavier","year":"2020","unstructured":"Xavier Rival and Kwangkeun Yi. 2020. Introduction to static analysis: an abstract interpretation perspective. Mit Press."},{"key":"e_1_3_2_44_1","volume-title":"Principles of Mathematical Analysis","author":"Rudin Walter","year":"1976","unstructured":"Walter Rudin. 1976. Principles of Mathematical Analysis (3rd ed.). McGraw-Hill."},{"key":"e_1_3_2_45_1","volume-title":"Quantifying the precision of numerical abstract domains","author":"Sotin Pascal","year":"2010","unstructured":"Pascal Sotin. 2010. Quantifying the precision of numerical abstract domains. Technical Report HAL Id: inria-00457324. INRIA. https:\/\/hal.inria.fr\/inria-00457324"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.2307\/2371174"},{"key":"e_1_3_2_47_1","volume-title":"Lectures on polytopes","author":"Ziegler G\u00fcnter M","year":"2012","unstructured":"G\u00fcnter M Ziegler. 2012. Lectures on polytopes. Vol. 152. Springer Science & Business Media."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776707","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T13:44:34Z","timestamp":1784209474000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776707"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":46,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776707"],"URL":"https:\/\/doi.org\/10.1145\/3776707","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}