{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,2]],"date-time":"2026-04-02T15:54:33Z","timestamp":1775145273298,"version":"3.50.1"},"reference-count":23,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2007,8,2]],"date-time":"2007-08-02T00:00:00Z","timestamp":1186012800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2007,8,2]]},"abstract":"<jats:p>\n            We consider integer arithmetic modulo a power of 2 as provided\nby mainstream programming languages like Java or standard\nimplementations of C. The difficulty here is that, for\n            <jats:italic>w<\/jats:italic>\n            &gt; 1, the ring\n            <jats:bold>Z<\/jats:bold>\n            <jats:sub>\n              <jats:italic>m<\/jats:italic>\n            <\/jats:sub>\n            of integers modulo\n            <jats:italic>m<\/jats:italic>\n            = 2\n            <jats:sup>\n              <jats:italic>w<\/jats:italic>\n            <\/jats:sup>\n            has zero divisors and thus cannot\nbe embedded into a field. Not withstanding that, we present intra-\nand interprocedural algorithms for inferring for every program\npoint\n            <jats:italic>u<\/jats:italic>\n            affine relations between program variables valid at\n            <jats:italic>u<\/jats:italic>\n            . If conditional branching is replaced with\nnondeterministic branching, our algorithms are not only sound but\nalso\n            <jats:italic>complete<\/jats:italic>\n            in that they detect\n            <jats:italic>all<\/jats:italic>\n            valid affine\nrelations in a natural class of programs. Moreover, they run in\ntime linear in the program size and polynomial in the number of\nprogram variables and can be implemented by using the same modular\ninteger arithmetic as the target language to be analyzed. We also\nindicate how our analysis can be extended to deal with equality\nguards, even in an interprocedural setting.\n          <\/jats:p>","DOI":"10.1145\/1275497.1275504","type":"journal-article","created":{"date-parts":[[2007,9,14]],"date-time":"2007-09-14T13:44:55Z","timestamp":1189777495000},"page":"29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":45,"title":["Analysis of modular arithmetic"],"prefix":"10.1145","volume":"29","author":[{"given":"Markus","family":"M\u00fcller-Olm","sequence":"first","affiliation":[{"name":"Westf\u00e4lische Wilhelms-Universit\u00e4t M\u00fcnster, M\u00fcnster, Germany"}]},{"given":"Helmut","family":"Seidl","sequence":"additional","affiliation":[{"name":"TU M\u00fcnchen, M\u00fcnchen, Germany"}]}],"member":"320","published-online":{"date-parts":[[2007,8,2]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the 13th International Conference on Compiler Construction (CC). Lecture Notes in Computer Science","volume":"2985","author":"Balakrishnan G.","unstructured":"Balakrishnan , G. and Reps , T. W . 2004. Analyzing memory accesses in x86 executables . In Proceedings of the 13th International Conference on Compiler Construction (CC). Lecture Notes in Computer Science , vol. 2985 . Springer, 5--23. Balakrishnan, G. and Reps, T. W. 2004. Analyzing memory accesses in x86 executables. In Proceedings of the 13th International Conference on Compiler Construction (CC). Lecture Notes in Computer Science, vol. 2985. Springer, 5--23."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(87)90004-5"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/322234.322243"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_2_1_5_1","first-page":"304","article-title":"Propagating differences: An efficient new fixpoint algorithm for distributive constraint systems","volume":"5","author":"Fecht C.","year":"1998","unstructured":"Fecht , C. and Seidl , H. 1998 . Propagating differences: An efficient new fixpoint algorithm for distributive constraint systems . Nordic J. Comput. 5 , 4, 304 -- 329 . Fecht, C. and Seidl, H. 1998. Propagating differences: An efficient new fixpoint algorithm for distributive constraint systems. Nordic J. Comput. 5, 4, 304--329.","journal-title":"Nordic J. Comput."},{"key":"e_1_2_1_6_1","unstructured":"Gosling J. Joy B. and Steele G. 1996. The Java Language Specification. Addison-Wesley.   Gosling J. Joy B. and Steele G. 1996. The Java Language Specification. Addison-Wesley."},{"key":"e_1_2_1_7_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the International Joint Conference on Theory and Practice of Software Development (TAPSOFT)","author":"Granger P.","unstructured":"Granger , P. 1991. Static analysis of linear congruence equalities among variables of a program . In Proceedings of the International Joint Conference on Theory and Practice of Software Development (TAPSOFT) . Lecture Notes in Computer Science , vol. 493 , Springer , 169--192. Granger, P. 1991. Static analysis of linear congruence equalities among variables of a program. In Proceedings of the International Joint Conference on Theory and Practice of Software Development (TAPSOFT). Lecture Notes in Computer Science, vol. 493, Springer, 169--192."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604138"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1137\/0220067"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268497"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_17"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_5"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_4"},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the 31st International Colloquium on Automata, Languages and Programming (ICALP). Lecture Notes in Computer Science","volume":"3142","author":"M\u00fcller-Olm M.","unstructured":"M\u00fcller-Olm , M. and Seidl , H . 2004a. A note on Karr's algorithm . In Proceedings of the 31st International Colloquium on Automata, Languages and Programming (ICALP). Lecture Notes in Computer Science , vol. 3142 . Springer, 1016--1028. M\u00fcller-Olm, M. and Seidl, H. 2004a. A note on Karr's algorithm. In Proceedings of the 31st International Colloquium on Automata, Languages and Programming (ICALP). Lecture Notes in Computer Science, vol. 3142. Springer, 1016--1028."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2004.05.004"},{"key":"e_1_2_1_17_1","volume-title":"Tech. Rep. 789, Fachbereich Informatik, Universit\u00e4t Dortmund.","author":"M\u00fcller-Olm M.","year":"2004","unstructured":"M\u00fcller-Olm , M. and Seidl , H . 2004 c. Interprocedural analysis of modular arithmetic. Tech. Rep. 789, Fachbereich Informatik, Universit\u00e4t Dortmund. M\u00fcller-Olm, M. and Seidl, H. 2004c. Interprocedural analysis of modular arithmetic. Tech. Rep. 789, Fachbereich Informatik, Universit\u00e4t Dortmund."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964029"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/357172.357177"},{"key":"e_1_2_1_20_1","unstructured":"Reps T. 2006. Personal communication.  Reps T. 2006. Personal communication."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111542.1111560"},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the International Static Analysis Symposium (SAS). Lecture Notes in Computer Science","volume":"2694","author":"Reps T.","unstructured":"Reps , T. , Schwoon , S. , and Jha , S . 2003. Weighted pushdown systems and their application to interprocedural dataflow analysis . In Proceedings of the International Static Analysis Symposium (SAS). Lecture Notes in Computer Science , vol. 2694 . Springer, 189--213. Reps, T., Schwoon, S., and Jha, S. 2003. Weighted pushdown systems and their application to interprocedural dataflow analysis. In Proceedings of the International Static Analysis Symposium (SAS). Lecture Notes in Computer Science, vol. 2694. Springer, 189--213."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_2_1_25_1","unstructured":"Warren H. S. 2003. Hacker's Delight. Addison-Wesley.   Warren H. S. 2003. Hacker's Delight. Addison-Wesley."}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1275497.1275504","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1275497.1275504","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:00:30Z","timestamp":1750276830000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1275497.1275504"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,8,2]]},"references-count":23,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2007,8,2]]}},"alternative-id":["10.1145\/1275497.1275504"],"URL":"https:\/\/doi.org\/10.1145\/1275497.1275504","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,8,2]]},"assertion":[{"value":"2007-08-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}