{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:24:05Z","timestamp":1776317045581,"version":"3.50.1"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"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":[[2022,1,16]]},"abstract":"<jats:p>Imprecision is inherent in any decidable (sound) approximation of undecidable program properties. In abstract interpretation this corresponds to the release of false alarms, e.g., when it is used for program analysis and program verification. As all alarming systems, a program analysis tool is credible when few false alarms are reported. As a consequence, we have to live together with false alarms, but also we need methods to control them. As for all approximation methods, also for abstract interpretation we need to estimate the accumulated imprecision during program analysis. In this paper we introduce a theory for estimating the error propagation in abstract interpretation, and hence in program analysis. We enrich abstract domains with a weakening of a metric distance. This enriched structure keeps coherence between the standard partial order relating approximated objects by their relative precision and the effective error made in this approximation. An abstract interpretation is precise when it is complete. We introduce the notion of partial completeness as a weakening of precision. In partial completeness the abstract interpreter may produce a bounded number of false alarms. We prove the key recursive properties of the class of programs for which an abstract interpreter is partially complete with a given bound of imprecision. Then, we introduce a proof system for estimating an upper bound of the error accumulated by the abstract interpreter during program analysis. Our framework is general enough to be instantiated to most known metrics for abstract domains.<\/jats:p>","DOI":"10.1145\/3498721","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":18,"title":["Partial (In)Completeness in abstract interpretation: limiting the imprecision in program analysis"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1099-3494","authenticated-orcid":false,"given":"Marco","family":"Campion","sequence":"first","affiliation":[{"name":"University of Verona, Italy"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2761-4347","authenticated-orcid":false,"given":"Mila","family":"Dalla Preda","sequence":"additional","affiliation":[{"name":"University of Verona, Italy"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9582-3960","authenticated-orcid":false,"given":"Roberto","family":"Giacobazzi","sequence":"additional","affiliation":[{"name":"University of Verona, Italy"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328455"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/321386.321395"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371096"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470608"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-32304-2_7"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45260-5_4"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-018-9625-6"},{"key":"e_1_2_2_8_1","volume-title":"Surreptitious Software: Obfuscation, Watermarking, and Tamperproofing for Software Protection","author":"Collberg Christian","year":"2009","unstructured":"Christian Collberg and Jasvir Nagra . 2009 . Surreptitious Software: Obfuscation, Watermarking, and Tamperproofing for Software Protection . Addison-Wesley Professional . isbn:0321549252 Christian Collberg and Jasvir Nagra. 2009. Surreptitious Software: Obfuscation, Watermarking, and Tamperproofing for Software Protection. Addison-Wesley Professional. isbn:0321549252"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/MIS.2011.106"},{"key":"e_1_2_2_10_1","volume-title":"Principles of Abstract Interpretation","author":"Cousot Patrick","unstructured":"Patrick Cousot . 2021. Principles of Abstract Interpretation . The MIT Press , Cambridge, Mass .. Patrick Cousot. 2021. Principles of Abstract Interpretation. The MIT Press, Cambridge, Mass.."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/390019.808314"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.4.511"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55844-6_142"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_8"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290355"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_2_2_19_1","volume-title":"1997 Joint Conf. on Declarative Programming, APPIA-GULP-PRODE\u201997","author":"Crazzolara Federico","year":"1997","unstructured":"Federico Crazzolara . 1997 . Quasi-metric Spaces as Domains for Abstract Interpretation . In 1997 Joint Conf. on Declarative Programming, APPIA-GULP-PRODE\u201997 , Grado, Italy , June 16-19, 1997, Moreno Falaschi, Marisa Navarro, and Alberto Policriti (Eds.). 45\u201356. Federico Crazzolara. 1997. Quasi-metric Spaces as Domains for Abstract Interpretation. In 1997 Joint Conf. on Declarative Programming, APPIA-GULP-PRODE\u201997, Grado, Italy, June 16-19, 1997, Moreno Falaschi, Marisa Navarro, and Alberto Policriti (Eds.). 45\u201356."},{"key":"e_1_2_2_20_1","volume-title":"International Workshop on Logic-Based Program Synthesis and Transformation. Springer, 147\u2013164","author":"Pierro Alessandra Di","year":"2000","unstructured":"Alessandra Di Pierro and Herbert Wiklicky . 2000 . Measuring the precision of abstract interpretations . In International Workshop on Logic-Based Program Synthesis and Transformation. Springer, 147\u2013164 . Alessandra Di Pierro and Herbert Wiklicky. 2000. Measuring the precision of abstract interpretations. In International Workshop on Logic-Based Program Synthesis and Transformation. Springer, 147\u2013164."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338112"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2008.41"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676987"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33125-1_11"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-016-0374-2"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333989"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256195"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_24"},{"key":"e_1_2_2_29_1","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\/  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\/"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000034"},{"key":"e_1_2_2_31_1","volume-title":"Theory of recursive functions and effective computability","author":"Rogers Hartley","unstructured":"Hartley Rogers . 1992. Theory of recursive functions and effective computability . The MIT press . Hartley Rogers. 1992. Theory of recursive functions and effective computability. The MIT press."},{"key":"e_1_2_2_32_1","unstructured":"Pascal Sotin. 2010. Quantifying the precision of numerical abstract domains. INRIA. https:\/\/hal.inria.fr\/inria-00457324  Pascal Sotin. 2010. Quantifying the precision of numerical abstract domains. INRIA. https:\/\/hal.inria.fr\/inria-00457324"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.4230\/DagRep.9.8.1"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61739-6_53"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.2307\/2371174"},{"key":"e_1_2_2_36_1","volume-title":"The formal semantics of programming languages: an introduction","author":"Winskel Glynn","unstructured":"Glynn Winskel . 1993. The formal semantics of programming languages: an introduction . MIT press . Glynn Winskel. 1993. The formal semantics of programming languages: an introduction. MIT press."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498721","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498721","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:29Z","timestamp":1750188629000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498721"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":36,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498721"],"URL":"https:\/\/doi.org\/10.1145\/3498721","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}