{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,20]],"date-time":"2025-09-20T21:33:14Z","timestamp":1758403994629,"version":"3.40.3"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030992521"},{"type":"electronic","value":"9783030992538"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T00:00:00Z","timestamp":1648512000000},"content-version":"vor","delay-in-days":87,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Static analyses are mostly designed to show the <jats:italic>absence of bugs<\/jats:italic>: if the analysis reports no alarms then the program won\u2019t exhibit any unwanted behaviours. To this aim they manipulate over-approximations of program semantics and, inevitably, they often report some <jats:italic>false<\/jats:italic> alarms. Recently, O\u2019Hearn proposed Incorrectness Logic, that is based on under-approximations, as a formal method to <jats:italic>find bugs<\/jats:italic> that only reports <jats:italic>true<\/jats:italic> alarms. In this paper we aim to answer one important question raised by O\u2019Hearn, namely which role can Abstract Interpretation play for the development of under-approximate tools for bug catching. In principle, Abstract Interpretation based static analyses can be defined for computing over-approximations as well as under-approximations, but in practice, most techniques exploited the former while few attempts developed the latter. To show why it is difficult to design effective under-approximation abstract domains, we first propose the new definitions of <jats:italic>non emptying functions<\/jats:italic> and <jats:italic>highly surjective function family<\/jats:italic> and then we formally prove the limits of under-approximation analysis by showing the non existence of abstract domains able to approximate such functions in a non trivial way. Our results outline the limits of under-approximation Abstract Interpretation and clarify, for the first time, why over- and under- approximation analyzers exhibited such a different development.<\/jats:p>","DOI":"10.1007\/978-3-030-99253-8_2","type":"book-chapter","created":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:02:48Z","timestamp":1648497768000},"page":"21-39","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Limits and difficulties in the design of under-approximation abstract domains"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4624-9752","authenticated-orcid":false,"given":"Flavio","family":"Ascari","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7771-4154","authenticated-orcid":false,"given":"Roberto","family":"Bruni","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7424-9576","authenticated-orcid":false,"given":"Roberta","family":"Gori","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,3,29]]},"reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Boulanger, J.L. (ed.): Static Analysis of Software: The Abstract Interpretation. Wiley (2011)","DOI":"10.1002\/9781118602867"},{"key":"2_CR2","doi-asserted-by":"publisher","unstructured":"Bourdoncle, F.: Abstract debugging of higher-order imperative languages. SIGPLAN Not. 28(6), 46\u201355 (Jun 1993). https:\/\/doi.org\/10.1145\/173262.155095","DOI":"10.1145\/173262.155095"},{"key":"2_CR3","doi-asserted-by":"publisher","unstructured":"Calcagno, C., Distefano, D., Dubreil, J., Gabi, D., Hooimeijer, P., Luca, M., O\u2019Hearn, P.W., Papakonstantinou, I., Purbrick, J., Rodriguez, D.: Moving fast with software verification. In: Proc. NFM\u201915. LNCS, vol.\u00a09058, pp. 3\u201311. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-17524-9_1","DOI":"10.1007\/978-3-319-17524-9_1"},{"key":"2_CR4","unstructured":"Cousot, P.: Principles of Abstract Interpretation. MIT Press (2021)"},{"key":"2_CR5","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and per analysis of functional languages). In: Proceedings of 1994 IEEE International Conference on Computer Languages (ICCL\u201994). pp. 95\u2013112 (1994). https:\/\/doi.org\/10.1109\/ICCL.1994.288389","DOI":"10.1109\/ICCL.1994.288389"},{"key":"2_CR6","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. p. 238\u2013252. POPL \u201977, Association for Computing Machinery, New York, NY, USA (1977). https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"2_CR7","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. p. 269\u2013282. POPL \u201979, Association for Computing Machinery, New York, NY, USA (1979). https:\/\/doi.org\/10.1145\/567752.567778","DOI":"10.1145\/567752.567778"},{"key":"2_CR8","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R., F\u00e4hndrich, M., Logozzo, F.: Automatic inference of necessary preconditions. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) Verification, Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013. Proceedings. Lecture Notes in Computer Science, vol.\u00a07737, pp. 128\u2013148. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_10","DOI":"10.1007\/978-3-642-35873-9_10"},{"key":"2_CR9","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R., Logozzo, F.: Precondition inference from intermittent assertions and application to contracts on collections. In: Jhala, R., Schmidt, D.A. (eds.) Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings. Lecture Notes in Computer Science, vol.\u00a06538, pp. 150\u2013168. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-18275-4_12","DOI":"10.1007\/978-3-642-18275-4_12"},{"key":"2_CR10","doi-asserted-by":"publisher","unstructured":"Distefano, D., F\u00e4hndrich, M., Logozzo, F., O\u2019Hearn, P.W.: Scaling static analyses at Facebook. Commun. ACM 62(8), 62\u201370 (2019). https:\/\/doi.org\/10.1145\/3338112","DOI":"10.1145\/3338112"},{"key":"2_CR11","unstructured":"Fil\u00e9, G., Ranzato, F.: Improving abstract interpretations by systematic lifting to the powerset. In: Proceedings of the 1994 International Symposium on Logic Programming. p. 655\u2013669. ILPS \u201994, MIT Press, Cambridge, MA, USA (1994)"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. Proceedings of Symposium on Applied Mathematics 19, 19\u201332 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"2_CR13","doi-asserted-by":"publisher","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (Oct 1969). https:\/\/doi.org\/10.1145\/363235.363259","DOI":"10.1145\/363235.363259"},{"key":"2_CR14","unstructured":"Lev-Ami, T., Sagiv, M., Reps, T., Gulwani, S.: Backward analysis for inferring quantified preconditions. Tr-2007-12-01, Tel Aviv University (2007)"},{"key":"2_CR15","doi-asserted-by":"publisher","unstructured":"Min\u00e9, A.: Backward under-approximations in numeric abstract domains to automatically infer sufficient program conditions. Sci. Comput. Program. 93, 154\u2013182 (Nov 2014). https:\/\/doi.org\/10.1016\/j.scico.2013.09.014","DOI":"10.1016\/j.scico.2013.09.014"},{"key":"2_CR16","doi-asserted-by":"publisher","unstructured":"Min\u00e9, A.: Tutorial on static inference of numeric invariants by abstract interpretation. Found. Trends Program. Lang. 4(3\u20134), 120\u2013372 (Dec 2017). https:\/\/doi.org\/10.1561\/2500000034","DOI":"10.1561\/2500000034"},{"key":"2_CR17","doi-asserted-by":"publisher","unstructured":"Nielson, F., Nielson, H., Hankin, C.: Principles of Program Analysis. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-662-03811-6","DOI":"10.1007\/978-3-662-03811-6"},{"key":"2_CR18","doi-asserted-by":"publisher","unstructured":"O\u2019Hearn, P.W.: Continuous reasoning: Scaling the impact of formal methods. In: Proc. LICS\u201918. p. 13\u201325. ACM (2018). https:\/\/doi.org\/10.1145\/3209108.3209109","DOI":"10.1145\/3209108.3209109"},{"key":"2_CR19","doi-asserted-by":"publisher","unstructured":"O\u2019Hearn, P.W.: Incorrectness logic. Proc. ACM Program. Lang. 4(POPL) (Dec 2019). https:\/\/doi.org\/10.1145\/3371078","DOI":"10.1145\/3371078"},{"key":"2_CR20","doi-asserted-by":"publisher","unstructured":"Raad, A., Berdine, J., Dang, H.H., Dreyer, D., O\u2019Hearn, P.W., Villard, J.: Local reasoning about the presence of bugs: Incorrectness separation logic. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12225, pp. 225\u2013252. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_14","DOI":"10.1007\/978-3-030-53291-8_14"},{"key":"2_CR21","doi-asserted-by":"publisher","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: 17th IEEE Symposium on Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings. pp. 55\u201374. IEEE Computer Society (2002). https:\/\/doi.org\/10.1109\/LICS.2002.1029817","DOI":"10.1109\/LICS.2002.1029817"},{"key":"2_CR22","unstructured":"Rival, X., Yi, K.: Introduction to Static Analysis \u2013 An Abstract Interpretation Perspective. MIT Press (2020)"},{"key":"2_CR23","doi-asserted-by":"publisher","unstructured":"Sadowski, C., Aftandilian, E., Eagle, A., Miller-Cushon, L., Jaspan, C.: Lessons from building static analysis tools at Google. Commun. ACM 61(4), 58\u201366 (Mar 2018). https:\/\/doi.org\/10.1145\/3188720","DOI":"10.1145\/3188720"},{"key":"2_CR24","doi-asserted-by":"publisher","unstructured":"Schmidt, D.A.: A calculus of logical relations for over- and underapproximating static analyses. Sci. Comput. Program. 64(1), 29\u201353 (2007). https:\/\/doi.org\/10.1016\/j.scico.2006.03.008","DOI":"10.1016\/j.scico.2006.03.008"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99253-8_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:03:45Z","timestamp":1648497825000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99253-8_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030992521","9783030992538"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99253-8_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"77","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"23","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}