{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:24:04Z","timestamp":1776317044910,"version":"3.50.1"},"reference-count":80,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"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":[[2024,1,2]]},"abstract":"<jats:p>It is widely known that the precision of a program analyzer is closely related to intensional program properties, namely, properties concerning how the program is written. This explains, for instance, the interest in code obfuscation techniques, namely, tools explicitly designed to degrade the results of program analysis by operating syntactic program transformations. Less is known about a possible relation between what the program extensionally computes, namely, its input-output relation, and the precision of a program analyzer. In this paper we explore this potential connection in an effort to isolate program fragments that can be precisely analyzed by abstract interpretation, namely, programs for which there exists a complete abstract interpretation. In the field of static inference of numeric invariants, this happens for programs, or parts of programs, that manifest a monotone (either non-decreasing or non-increasing) behavior. We first formalize the notion of program monotonicity with respect to a given input and a set of numerical variables of interest. A sound proof system is then introduced with judgments specifying whether a program is monotone relatively to a set of variables and a set of inputs. The interest in monotonicity is justified because we prove that the family of monotone programs admits a complete abstract interpretation over a specific class of non-trivial numerical abstractions and inputs. This class includes all non-relational abstract domains that refine interval analysis (i.e., at least as precise as the intervals abstraction) and that satisfy a topological convexity hypothesis.<\/jats:p>","DOI":"10.1145\/3632897","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"1629-1662","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Monotonicity and the Precision of Program Analysis"],"prefix":"10.1145","volume":"8","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"}]},{"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"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9582-3960","authenticated-orcid":false,"given":"Roberto","family":"Giacobazzi","sequence":"additional","affiliation":[{"name":"University of Arizona, Tucson, USA"}]},{"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"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371106"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158153"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000051"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434329"},{"key":"e_1_3_1_6_1","unstructured":"Peter Alvaro Neil Conway Joseph M. Hellerstein and William R. Marczak. 2011. Consistency Analysis in Bloom: a CALM and Collected Approach. In Fifth Biennial Conference on Innovative Data Systems Research CIDR 2011 Asilomar CA USA January 9-12 2011 Online Proceedings. www.cidrdb.org 249\u2013260. http:\/\/cidrdb.org\/cidr2011\/Papers\/CIDR11_Paper35.pdf"},{"key":"e_1_3_1_7_1","unstructured":"Dario Amodei Chris Olah Jacob Steinhardt Paul F. Christiano John Schulman and Dan Man\u00e9. 2016. Concrete Problems in AI Safety. CoRR abs\/1606.06565 (2016). arXiv:1606.06565 http:\/\/arxiv.org\/abs\/1606.06565"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951948"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30044-8_1"},{"key":"e_1_3_1_10_1","unstructured":"Maximilian Baader Matthew Mirman and Martin T. Vechev. 2020. Universal Approximation with Certified Networks. In 8th International Conference on Learning Representations ICLR 2020 Addis Ababa Ethiopia April 26-30 2020. OpenReview.net. https:\/\/openreview.net\/forum?id=B1gX8kBtPr"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0377-0427(94)90294-1"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-32304-2_22"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629488"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1921532.1921553"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000002"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371096"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","unstructured":"Roberto Bruni Roberto Giacobazzi Roberta Gori and Francesco Ranzato. 2021. A Logic for Locally Complete Abstract Interpretations. In 36th Annual ACM\/IEEE Symposium on Logic in Computer Science LICS 2021 Rome Italy June 29 - July 2 2021. IEEE 1\u201313. https:\/\/doi.org\/10.1109\/LICS52264.2021.9470608 10.1109\/LICS52264.2021.9470608","DOI":"10.1109\/LICS52264.2021.9470608"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523453"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3582267"},{"key":"e_1_3_1_20_1","first-page":"79","volume-title":"Proceedings of the 23rd Italian Conference on Theoretical Computer Science, ICTCS 2022, Rome, Italy, September 7-9, 2022 (CEUR Workshop Proceedings, Vol. 3284)","author":"Campion Marco","year":"2022","unstructured":"Marco Campion, Mila Dalla Preda, and Roberto Giacobazzi. 2022a. On the Properties of Partial Completeness in Abstract Interpretation. In Proceedings of the 23rd Italian Conference on Theoretical Computer Science, ICTCS 2022, Rome, Italy, September 7-9, 2022 (CEUR Workshop Proceedings, Vol. 3284), Ugo Dal Lago and Daniele Gorla (Eds.). CEUR-WS.org, 79\u201385. http:\/\/ceur-ws.org\/Vol-3284\/8665.pdf"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11416-021-00377-z"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498721"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-44245-2_7"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706308"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2025113.2025131"},{"key":"e_1_3_1_26_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."},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2391229.2391230"},{"key":"e_1_3_1_28_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_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/390019.808314"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.4.511"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603165"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_3"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290355"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2005.13"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/_j.tcs.2015.02.024"},{"key":"e_1_3_1_38_1","first-page":"81","volume-title":"Proc. of the 11th Internat. Conf. on Algebraic Methodology and Software Technology (AMAST \u201906) (Lecture Notes in Computer Science, Vol. 4019)","author":"Preda M. Dalla","year":"2006","unstructured":"M. Dalla Preda, M. Madou, K. De Bosschere, and R. Giacobazzi. 2006. Opaque Predicates Detection by Abstract Interpretation. In Proc. of the 11th Internat. Conf. on Algebraic Methodology and Software Technology (AMAST \u201906) (Lecture Notes in Computer Science, Vol. 4019). Springer-Verlag, 81\u201395."},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338112"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(03)00392-X"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.neunet.2017.12.012"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236765"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00058"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2008.41"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676987"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33125-1_11"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-016-0374-2"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/333979.333989"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","unstructured":"Sven Gowal Krishnamurthy Dvijotham Robert Stanforth Rudy Bunel Chongli Qin Jonathan Uesato Relja Arandjelovic Timothy Arthur Mann and Pushmeet Kohli. 2019. Scalable Verified Training for Provably Robust Image Classification. In 2019 IEEE\/CVF International Conference on Computer Vision ICCV 2019 Seoul Korea (South) October 27 - November 2 2019. IEEE 4841\u20134850. https:\/\/doi.org\/10.1109\/ICCV.2019.00494 10.1109\/ICCV.2019.00494","DOI":"10.1109\/ICCV.2019.00494"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1080\/00207168908803778"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/D19-1419"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/WCRE.2012.16"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908096"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-22308-2_16"},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44978-7_10"},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/WCRE.2001.957836"},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000034"},{"key":"e_1_3_1_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACSAC.2007.21"},{"key":"e_1_3_1_60_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_1_61_1","volume-title":"Principles of program analysis","author":"Nielson Flemming","year":"2015","unstructured":"Flemming Nielson, Hanne R Nielson, and Chris Hankin. 2015. Principles of program analysis. springer."},{"key":"e_1_3_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209109"},{"key":"e_1_3_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/1929553.1929565"},{"key":"e_1_3_1_64_1","unstructured":"Prajit Ramachandran Barret Zoph and Quoc V. Le. 2018. Searching for Activation Functions. In 6th International Conference on Learning Representations ICLR 2018 Vancouver BC Canada April 30 - May 3 2018 Workshop Track Proceedings. OpenReview.net. https:\/\/openreview.net\/forum?id=Hkuq2EkPf"},{"key":"e_1_3_1_65_1","doi-asserted-by":"publisher","DOI":"10.2307\/1990888"},{"key":"e_1_3_1_66_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_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/3188720"},{"key":"e_1_3_1_68_1","volume-title":"Toward a mathematical semantics for computer languages","author":"Scott Dana S","year":"1971","unstructured":"Dana S Scott and Christopher Strachey. 1971. Toward a mathematical semantics for computer languages. Vol. 1. Oxford University Computing Laboratory, Programming Research Group Oxford."},{"key":"e_1_3_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158143"},{"key":"e_1_3_1_70_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_3_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439931"},{"key":"e_1_3_1_72_1","first-page":"7","volume-title":"Introduction to real analysis","author":"Trench William F","year":"2013","unstructured":"William F Trench. 2013. Introduction to real analysis. Faculty Authored and Edited Books & CDs. 7."},{"key":"e_1_3_1_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_22"},{"key":"e_1_3_1_74_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10936-7_19"},{"key":"e_1_3_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/1435417.1435432"},{"key":"e_1_3_1_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338503.3357718"},{"key":"e_1_3_1_77_1","first-page":"1599","volume-title":"27th USENIX Security Symposium, USENIX Security 2018, Baltimore, MD, USA, August 15-17, 2018","author":"Wang Shiqi","year":"2018","unstructured":"Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. 2018. Formal Security Analysis of Neural Networks using Symbolic Intervals. In 27th USENIX Security Symposium, USENIX Security 2018, Baltimore, MD, USA, August 15-17, 2018, William Enck and Adrienne Porter Felt (Eds.). USENIX Association, 1599\u20131614. https:\/\/www.usenix.org\/conference\/usenixsecurity18\/presentation\/wang-shiqi"},{"key":"e_1_3_1_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498675"},{"key":"e_1_3_1_79_1","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/3054.001.0001"},{"key":"e_1_3_1_80_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11784-009-0130-9"},{"key":"e_1_3_1_81_1","doi-asserted-by":"publisher","DOI":"10.1109\/BWCCA.2010.85"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632897","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632897","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:04:39Z","timestamp":1751659479000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632897"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":80,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632897"],"URL":"https:\/\/doi.org\/10.1145\/3632897","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}