{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,2]],"date-time":"2026-04-02T15:54:44Z","timestamp":1775145284380,"version":"3.50.1"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2015,1,20]],"date-time":"2015-01-20T00:00:00Z","timestamp":1421712000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Australian Research Council, under ARC","award":["DP110102579"],"award-info":[{"award-number":["DP110102579"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2015,1,20]]},"abstract":"<jats:p>The most commonly used integer types have fixed bit-width, making it possible for computations to \u201cwrap around,\u201d and many programs depend on this behaviour. Yet much work to date on program analysis and verification of integer computations treats integers as having infinite precision, and most analyses that do respect fixed width lose precision when overflow is possible. We present a novel integer interval abstract domain that correctly handles wrap-around. The analysis is signedness agnostic. By treating integers as strings of bits, only considering signedness for operations that treat them differently, we produce precise, correct results at a modest cost in execution time.<\/jats:p>","DOI":"10.1145\/2651360","type":"journal-article","created":{"date-parts":[[2015,1,28]],"date-time":"2015-01-28T14:05:51Z","timestamp":1422453951000},"page":"1-35","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["Interval Analysis and Machine Arithmetic"],"prefix":"10.1145","volume":"37","author":[{"given":"Graeme","family":"Gange","sequence":"first","affiliation":[{"name":"The University of Melbourne, Australia"}]},{"given":"Jorge A.","family":"Navas","sequence":"additional","affiliation":[{"name":"The University of Melbourne, Australia"}]},{"given":"Peter","family":"Schachte","sequence":"additional","affiliation":[{"name":"The University of Melbourne, Australia"}]},{"given":"Harald","family":"S\u00f8ndergaard","sequence":"additional","affiliation":[{"name":"The University of Melbourne, Australia"}]},{"given":"Peter J.","family":"Stuckey","sequence":"additional","affiliation":[{"name":"The University of Melbourne, Australia"}]}],"member":"320","published-online":{"date-parts":[[2015,1,20]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","unstructured":"Gogul Balakrishnan. 2007. WYSINWYX: What You See Is Not What You Execute. Ph.D. Dissertation. University of Wisconsin at Madison Madison WI.","DOI":"10.5555\/1354261"},{"key":"e_1_2_1_2_1","volume-title":"Compiler Construction: Proceedings of the 13th International Conference","author":"Balakrishnan Gogul","unstructured":"Gogul Balakrishnan and Thomas Reps. 2004. Analyzing memory accesses in x86 executables. In Compiler Construction: Proceedings of the 13th International Conference, E. Duesterwald (Ed.). Lecture Notes in Computer Science, Vol. 2985. Springer, 5--23."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_7"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/860256.860262"},{"key":"e_1_2_1_5_1","series-title":"Lecture Notes in Computer Science","volume-title":"Formal verification of a C value analysis based on abstract interpretation","author":"Blazy Sandrine","unstructured":"Sandrine Blazy, Vincent Laporte, Andre Maroneze, and David Pichardie. 2013. Formal verification of a C value analysis based on abstract interpretation. In Static Analysis, F. Logozzo and M. F\u00e4hndrich (Eds.). Lecture Notes in Computer Science, Vol. 7935. Springer, 324--344."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/1882094.1882105"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/2486788.2486892"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781157"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/646448.692441"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/2337223.2337313"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/1949303.1949305"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27705-4_21"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_48"},{"key":"e_1_2_1_16_1","volume-title":"Stuckey","author":"Gange Graeme","year":"2013","unstructured":"Graeme Gange, Jorge A. Navas, Peter Schachte, Harald S\u00f8ndergaard, and Peter J. Stuckey. 2013a. Abstract interpretation over non-lattice abstract domains. In Static Analysis, F. Logozzo and M. F\u00e4hndrich (Eds.). Lecture Notes in Computer Science, Vol. 7935. Springer, 6--24."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_15"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03456-5_28"},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the Ninth International Workshop on Constraint Modelling and Reformulation (ModRef\u201910)","author":"Gotlieb Arnaud","year":"2010","unstructured":"Arnaud Gotlieb, Michel Leconte, and Bruno Marre. 2010. Constraint solving on modular integers. In Proceedings of the Ninth International Workshop on Constraint Modelling and Reformulation (ModRef\u201910)."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1080\/00207168908803778"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/111310.111320"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11319-2_16"},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the 1st Workshop on Software Testing, Verification and Analysis (CSTVA\u201906)","author":"Leconte Michel","year":"2006","unstructured":"Michel Leconte and Bruno Berstel. 2006. Extending a CP solver with congruences as domains for program verification. In Proceedings of the 1st Workshop on Software Testing, Verification and Analysis (CSTVA\u201906), B. Blanc, A. Gotlieb, and C. Michel (Eds.). 22--33."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/2391451.2391465"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.129.21"},{"key":"e_1_2_1_26_1","volume-title":"Stuckey","author":"Marriott Kim","year":"1998","unstructured":"Kim Marriott and Peter J. Stuckey. 1998. Programming with Constraints: An Introduction. MIT Press, Cambridge, MA."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33558-7_39"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8609-1"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/PACT.1999.807422"},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the 10th Asian Symposium on Programming Languages and Systems (APLAS\u201912)","volume":"7705","author":"Navas Jorge A.","unstructured":"Jorge A. Navas, Peter Schachte, Harald S\u00f8ndergaard, and Peter J. Stuckey. 2012. Signedness-agnostic program analysis: Precise integer bounds for low-level code. In Proceedings of the 10th Asian Symposium on Programming Languages and Systems (APLAS\u201912), R. Jhala and A. Igarashi (Eds.). Lecture Notes in Computer Science, Vol. 7705. Springer, 115--130."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/555142"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1134650.1134657"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111542.1111560"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2013.6494996"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/2422921"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2007.371251"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/2391451.2391461"},{"key":"e_1_2_1_38_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Su Zhendong","unstructured":"Zhendong Su and David Wagner. 2004. A class of polynomially solvable range constraints for interval analysis without widenings and narrowings. In Tools and Algorithms for the Construction and Analysis of Systems, K. Jensen and A. Podelski (Eds.). Lecture Notes in Computer Science, Vol. 2988. Springer, 280--295."},{"key":"e_1_2_1_39_1","volume-title":"Proceedings of the 2011 Brazilian Symposium on Programming Languages.","author":"Douglas D.","unstructured":"Douglas D. C. Teixera and Fernando M. Q. Pereira. 2011. The design and implementation of a non-iterative range analysis algorithm on a production compiler. In Proceedings of the 2011 Brazilian Symposium on Programming Languages."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2522728"},{"key":"e_1_2_1_41_1","unstructured":"Henry S. Warren Jr. 2003. Hacker\u2019s Delight. Addison Wesley New York NY."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/1888881.1888888"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.5555\/2590708.2590711"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2651360","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2651360","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:11:54Z","timestamp":1750227114000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2651360"}},"subtitle":["Why Signedness Ignorance Is Bliss"],"short-title":[],"issued":{"date-parts":[[2015,1,20]]},"references-count":43,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,1,20]]}},"alternative-id":["10.1145\/2651360"],"URL":"https:\/\/doi.org\/10.1145\/2651360","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,1,20]]},"assertion":[{"value":"2013-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-01-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}