{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:11:28Z","timestamp":1767928288183,"version":"3.49.0"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2014,10,28]],"date-time":"2014-10-28T00:00:00Z","timestamp":1414454400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["CCF-{0810053, 0904371}"],"award-info":[{"award-number":["CCF-{0810053, 0904371}"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000006","name":"Office of Naval Research","doi-asserted-by":"publisher","award":["N00014-{09-1-0510, 10-M-0251, 11-C-0447}"],"award-info":[{"award-number":["N00014-{09-1-0510, 10-M-0251, 11-C-0447}"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006602","name":"Air Force Research Laboratory","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100006602","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006754","name":"U.S. Army Research Laboratory","doi-asserted-by":"publisher","award":["W911NF-09-1-0413"],"award-info":[{"award-number":["W911NF-09-1-0413"]}],"id":[{"id":"10.13039\/100006754","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2014,10,28]]},"abstract":"<jats:p>\n            This article considers some known abstract domains for affine-relation analysis (ARA), along with several variants, and studies how they relate to each other. The various domains represent sets of points that satisfy affine relations over variables that hold machine integers and are based on an extension of linear algebra to modules over a ring (in particular, arithmetic performed modulo 2\n            <jats:sup>\n              <jats:italic>w<\/jats:italic>\n            <\/jats:sup>\n            , for some machine-integer width\n            <jats:italic>w<\/jats:italic>\n            ).\n          <\/jats:p>\n          <jats:p>\n            We show that the abstract domains of M\u00fcller-Olm\/Seidl (MOS) and King\/S\u00f8ndergaard (KS) are, in general, incomparable. However, we give sound interconversion methods. In other words, we give an algorithm to convert a KS element\n            <jats:italic>v<\/jats:italic>\n            <jats:sub>KS<\/jats:sub>\n            to an overapproximating MOS element\n            <jats:italic>v<\/jats:italic>\n            <jats:sub>MOS<\/jats:sub>\n            \u2014that is, \u03b3 (\n            <jats:italic>v<\/jats:italic>\n            <jats:sub>KS<\/jats:sub>\n            ) \u2286 \u03b3 (\n            <jats:italic>v<\/jats:italic>\n            <jats:sub>MOS<\/jats:sub>\n            \u2014as well as an algorithm to convert an MOS element\n            <jats:italic>w<\/jats:italic>\n            <jats:sub>MOS<\/jats:sub>\n            to an overapproximating KS element\n            <jats:italic>w<\/jats:italic>\n            <jats:sub>KS<\/jats:sub>\n            \u2014that is, \u03b3 (\n            <jats:italic>w<\/jats:italic>\n            <jats:sub>MOS<\/jats:sub>\n            ) \u2286 \u03b3 (\n            <jats:italic>w<\/jats:italic>\n            <jats:sub>KS<\/jats:sub>\n            ).\n          <\/jats:p>\n          <jats:p>The article provides insight on the range of options that one has for performing ARA in a program analyzer:<\/jats:p>\n          <jats:p>\u2014We describe how to perform a greedy, operator-by-operator abstraction method to obtain KS abstract transformers.<\/jats:p>\n          <jats:p>\u2014We also describe a more global approach to obtaining KS abstract transformers that considers the semantics of an entire instruction, basic block, or other loop-free program fragment.<\/jats:p>\n          <jats:p>The latter method can yield best abstract transformers, and hence can be more precise than the former method. However, the latter method is more expensive.<\/jats:p>\n          <jats:p>We also explain how to use the KS domain for interprocedural program analysis using a bit-precise concrete semantics, but without bit blasting.<\/jats:p>","DOI":"10.1145\/2651361","type":"journal-article","created":{"date-parts":[[2014,10,29]],"date-time":"2014-10-29T18:05:55Z","timestamp":1414605955000},"page":"1-73","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":23,"title":["Abstract Domains of Affine Relations"],"prefix":"10.1145","volume":"36","author":[{"given":"Matt","family":"Elder","sequence":"first","affiliation":[{"name":"University of Wisconsin, Madison, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Junghee","family":"Lim","sequence":"additional","affiliation":[{"name":"University of Wisconsin, Madison, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tushar","family":"Sharma","sequence":"additional","affiliation":[{"name":"University of Wisconsin, Madison, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tycho","family":"Andersen","sequence":"additional","affiliation":[{"name":"University of Wisconsin, Madison, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[{"name":"University of Wisconsin and GrammaTech, Inc., Madison, WI"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,10,28]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/1759187.1759209"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.08.001"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604137"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/12.1.41"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/237578.237617"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_2_1_8_1","volume-title":"The Yices SMT Solver. Retrieved","author":"Dutertre B.","year":"2014","unstructured":"B. Dutertre and L. de Moura. 2006. The Yices SMT Solver. Retrieved September 2, 2014, from http:\/\/yices.csl.sri.com."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/2041552.2041569"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008013906463"},{"key":"e_1_2_1_11_1","unstructured":"M. Fredrikson and S. Jha. 2013. Personal communication."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1080\/00207168908803778"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604138"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040332"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1080\/03081088608817705"},{"key":"e_1_2_1_16_1","unstructured":"B. Jeannet. Polka. 2007. Retrieved September 2 2014 from http:\/\/pop-art.inrialpes.fr\/&sim;bjeannet\/newpolka\/polka.pdf."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/512644.512672"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00268497"},{"key":"e_1_2_1_19_1","unstructured":"N. Kidd A. Lal and T. Reps. 2007. WALi: The Weighted Automata Library. Retrieved September 2 2014 from www.cs.wisc.edu\/wpis\/wpds\/download.php."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_26"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11319-2_16"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/647471.727286"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_32"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_44"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/1788374.1788379"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2450136.2450139"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/343374"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964029"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_5"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/11547662_17"},{"key":"e_1_2_1_32_1","unstructured":"M. M\u00fcller-Olm and H. Seidl. 2005c. Personal communication."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1275497.1275504"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/22788.22800"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(89)90091-1"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/178243.178254"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_21"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2005.02.009"},{"key":"e_1_2_1_39_1","unstructured":"D. A. Schmidt. 1986. Denotational Semantics. Allyn & Bacon Boston MA."},{"key":"e_1_2_1_40_1","unstructured":"M. Sharir and A. Pnueli. 1981. Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications. Prentice Hall 189--233."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/645604.662896"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33125-1_10"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_17"},{"key":"e_1_2_1_45_1","unstructured":"H. S. Warren Jr. 2003. Hacker\u2019s 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\/2651361","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2651361","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\/2651361"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,10,28]]},"references-count":43,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,10,28]]}},"alternative-id":["10.1145\/2651361"],"URL":"https:\/\/doi.org\/10.1145\/2651361","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,10,28]]},"assertion":[{"value":"2013-05-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":"2014-10-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}