{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,6]],"date-time":"2026-10-06T15:16:56Z","timestamp":1791299816383,"version":"4.1.0"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T00:00:00Z","timestamp":1667174400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["1420866, 1763871, 1750965, 1918211, 2023222"],"award-info":[{"award-number":["1420866, 1763871, 1750965, 1918211, 2023222"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"ONR","award":["N00014-17-1-2889, N00014-19-1-2318"],"award-info":[{"award-number":["N00014-17-1-2889, N00014-19-1-2318"]}]},{"name":"Microsoft","award":["Microsoft Faculty Fellowship"],"award-info":[{"award-number":["Microsoft Faculty Fellowship"]}]},{"DOI":"10.13039\/100005801","name":"Facebook","doi-asserted-by":"publisher","award":["Facebook Research Awards"],"award-info":[{"award-number":["Facebook Research Awards"]}],"id":[{"id":"10.13039\/100005801","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,10,31]]},"abstract":"<jats:p>\n            This paper addresses the problem of creating abstract transformers automatically. The method we present automates the construction of static analyzers in a fashion similar to the way\n            <jats:italic>yacc<\/jats:italic>\n            automates the construction of parsers. Our method treats the problem as a program-synthesis problem. The user provides specifications of (i) the concrete semantics of a given operation\n            <jats:italic>op<\/jats:italic>\n            , (ii) the abstract domain\n            <jats:italic>A<\/jats:italic>\n            to be used by the analyzer, and (iii) the semantics of a domain-specific language\n            <jats:italic>L<\/jats:italic>\n            in which the abstract transformer is to be expressed. As output, our method creates an abstract transformer for\n            <jats:italic>op<\/jats:italic>\n            in abstract domain\n            <jats:italic>A<\/jats:italic>\n            , expressed in\n            <jats:italic>L<\/jats:italic>\n            (an \u201c\n            <jats:italic>L<\/jats:italic>\n            -transformer for\n            <jats:italic>op<\/jats:italic>\n            over\n            <jats:italic>A<\/jats:italic>\n            \u201d). Moreover, the abstract transformer obtained is a most-precise\n            <jats:italic>L<\/jats:italic>\n            -transformer for\n            <jats:italic>op<\/jats:italic>\n            over\n            <jats:italic>A<\/jats:italic>\n            ; that is, there is no other\n            <jats:italic>L<\/jats:italic>\n            -transformer for\n            <jats:italic>op<\/jats:italic>\n            over\n            <jats:italic>A<\/jats:italic>\n            that is strictly more precise.\n          <\/jats:p>\n          <jats:p>We implemented our method in a tool called AMURTH. We used AMURTH to create sets of replacement abstract transformers for those used in two existing analyzers, and obtained essentially identical performance. However, when we compared the existing transformers with the transformers obtained using AMURTH, we discovered that four of the existing transformers were unsound, which demonstrates the risk of using manually created transformers.<\/jats:p>","DOI":"10.1145\/3563334","type":"journal-article","created":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T20:23:35Z","timestamp":1667247815000},"page":"1291-1319","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":25,"title":["Synthesizing abstract transformers"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5826-0030","authenticated-orcid":false,"given":"Pankaj Kumar","family":"Kalita","sequence":"first","affiliation":[{"name":"IIT Kanpur, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3506-6742","authenticated-orcid":false,"given":"Sujit Kumar","family":"Muduli","sequence":"additional","affiliation":[{"name":"IIT Kanpur, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9625-4037","authenticated-orcid":false,"given":"Loris","family":"D\u2019Antoni","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5676-9949","authenticated-orcid":false,"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3394-023X","authenticated-orcid":false,"given":"Subhajit","family":"Roy","sequence":"additional","affiliation":[{"name":"IIT Kanpur, India"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,10,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_3"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485481"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2009.5351147"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_12"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2651361"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_10"},{"key":"e_1_2_1_8_1","volume-title":"Loris D\u2019Antoni, Thomas Reps, and Subhajit Roy.","author":"Kalita Pankaj Kumar","year":"2021","unstructured":"Pankaj Kumar Kalita , Sujit Kumar Muduli , Loris D\u2019Antoni, Thomas Reps, and Subhajit Roy. 2021 . Synthesizing Abstract Transformers. https:\/\/doi.org\/10.48550\/ARXIV.2105.00493 Extended version of the current work 10.48550\/ARXIV.2105.00493 Pankaj Kumar Kalita, Sujit Kumar Muduli, Loris D\u2019Antoni, Thomas Reps, and Subhajit Roy. 2021. Synthesizing Abstract Transformers. https:\/\/doi.org\/10.48550\/ARXIV.2105.00493 Extended version of the current work"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7092952"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3533767.3534381"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_5"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_39"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-58603-929-5-613"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54807-9_12"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385967"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563332"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35182-2_9"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293882.3330554"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454104"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_21"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_1"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250750"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0249-7"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33125-1_10"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.02.003"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_17"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE43902.2021.00079"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_22"},{"key":"e_1_2_1_29_1","volume-title":"Hacker\u2019s Delight","author":"Warren Henry S.","year":"1842","unstructured":"Henry S. Warren . 2012. Hacker\u2019s Delight ( 2 nd ed.). Addison-Wesley Professional . isbn:032 1842 685 Henry S. Warren. 2012. Hacker\u2019s Delight (2nd ed.). Addison-Wesley Professional. isbn:0321842685","edition":"2"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563334","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563334","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563334","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:38:10Z","timestamp":1750178290000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563334"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,31]]},"references-count":29,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3563334"],"URL":"https:\/\/doi.org\/10.1145\/3563334","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,31]]},"assertion":[{"value":"2022-10-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}