{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T08:02:49Z","timestamp":1790928169378,"version":"4.1.0"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"2","funder":[{"name":"National Science Foundation","award":["CCF-2211968 and CCF-2212558"],"award-info":[{"award-number":["CCF-2211968 and CCF-2212558"]}]},{"name":"Qualcomm Faculty Award"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2026,2,28]]},"abstract":"\n Designing abstract transformers for program-analysis tools is a challenging task. In the past, bugs have been discovered in such transformers, showing the difficulty of designing such transformers manually, and providing motivation for automated techniques. Recently, Kalita et al. showed how to apply program-synthesis techniques to create abstract transformers in a user-provided domain-specific language (DSL)\n \n \\({\\mathcal{L}}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n (i.e., \u201c\n \n \\({\\mathcal{L}}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n -transformers\u201d). Their technique creates provably sound and maximally precise\n \n \\({\\mathcal{L}}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n -transformers for an abstract domain\n \n \\( A \\)<\/jats:tex-math>\n <\/jats:inline-formula>\n \u2014i.e., given specifications of a concrete operation\n op<\/jats:italic>\n , DSL\n \n \\({\\mathcal{L}}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n , and abstract domain\n \n \\( A \\)<\/jats:tex-math>\n <\/jats:inline-formula>\n , it finds a best abstract\n \n \\({\\mathcal{L}}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n -transformer for\n op<\/jats:italic>\n in\n \n \\( A \\)<\/jats:tex-math>\n <\/jats:inline-formula>\n . However, we found that the algorithm of Kalita et al. does not succeed when applied to reduced-product domains: The need to synthesize transformers for all of the domains simultaneously blows up the search space.\n <\/jats:p>\n \n Because reduced-product domains are an important device for improving the precision of abstract interpretation, in this article, we propose an algorithm to synthesize reduced\n \n \\({\\mathcal{L}}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n -transformers\n \n \\(\\langle{f}^{\\sharp\\textsf{R}}_{1},{f}^{\\sharp\\textsf{R}}_{2},\\dots,{f}^{\\sharp \\textsf{R}}_{n}\\rangle\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n for a product domain\n \n \\(A_{1}\\times A_{2}\\times\\dots\\times A_{n}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n , using multiple DSLs:\n \n \\({\\mathcal{L}}\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n \n \\(=\\langle{\\mathcal{L}}_{1},{\\mathcal{L}}_{2},\\ldots,{\\mathcal{L}}_{n}\\rangle\\)<\/jats:tex-math>\n <\/jats:inline-formula>\n . Synthesis of reduced-product transformers is quite challenging: First, the synthesis task has to tackle an increased \u201cfeature set\u201d because each component transformer now has access to the abstract inputs from all component domains in the product. Second, to ensure that the product transformer is maximally precise, the synthesis task needs to arrange for the component transformers to cooperate with each other.\n <\/jats:p>\n \n We implemented our algorithm in a tool,\n Amurth2<\/jats:sc>\n , and used it to synthesize abstract transformers for two product domains\u2014SAFE and JSAI\u2014available within the SAFE\n str<\/jats:sub>\n framework for JavaScript program analysis. For four of the six operations supported by SAFE\n str<\/jats:sub>\n ,\n Amurth2<\/jats:sc>\n synthesizes more precise abstract transformers than the manually written ones available in SAFE\n str<\/jats:sub>\n .\n <\/jats:p>","DOI":"10.1145\/3733716","type":"journal-article","created":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T12:32:49Z","timestamp":1746189169000},"page":"1-41","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Automated Abstract Transformer Synthesis for Reduced Product Domains"],"prefix":"10.1145","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5826-0030","authenticated-orcid":false,"given":"Pankaj Kumar","family":"Kalita","sequence":"first","affiliation":[{"name":"Indian Institute of Technology Kanpur, Kanpur, India"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5676-9949","authenticated-orcid":false,"given":"Thomas","family":"Reps","sequence":"additional","affiliation":[{"name":"Computer Sciences Department, University of Wisconsin\u2013Madison, Madison, Wisconsin, 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":"Indian Institute of Technology Kanpur, Kanpur, India"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2026,1,21]]},"reference":[{"key":"e_1_3_3_2_2","unstructured":"SyGuS: Syntax-Guided Synthesis. [2019.] Retrieved March 16 2025 from https:\/\/sygus.org\/"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-61425-0_39"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_3"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454056"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062353"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","unstructured":"Matt Elder Junghee Lim Tushar Sharma Tycho Andersen and Thomas Reps. 2014. Abstract domains of affine relations. ACM Transactions on Programming Languages and Systems 36 4 Article 11 (Oct. 2014) 73 pages. DOI: 10.1145\/2651361","DOI":"10.1145\/2651361"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360220"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48288-9_7"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_10"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993506"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993505"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1561\/2500000010"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806833"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.34727\/2022\/isbn.978-3-85448-053-2_37"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3563334"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7092952"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.13114725"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-023-00420-3"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/2635868.2635904"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11319-2_16"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/3691620.3695015"},{"key":"e_1_3_3_26_2","article-title":"SAFE: Formal specification and implementation of a scalable analysis framework for ECMAScript","author":"Lee Hongki","year":"2012","unstructured":"Hongki Lee, Sooncheol Won, Joonho Jin, Junhee Cho, and Sukyoung Ryu. 2012. SAFE: Formal specification and implementation of a scalable analysis framework for ECMAScript. In Proceedings of the 19th International Workshop on Foundations of Object-Oriented Languages (FOOL).","journal-title":"Proceedings of the 19th International Workshop on Foundations of Object-Oriented Languages (FOOL)"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738002"},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884807"},{"key":"e_1_3_3_29_2","unstructured":"Net-Tutorials. 2018. jQuery Tutorial. Retrieved from http:\/\/www.jquery-tutorial.net"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3622861"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290385"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_21"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49122-5_1"},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_9"},{"key":"e_1_3_3_35_2","doi-asserted-by":"crossref","unstructured":"Matan Shachnai Harishankar Vishwanathan Srinivas Narayana and Santosh Nagarakatte. 2024. Fixing latent unsound abstract operators in the eBPF verifier of the Linux kernel. In SAS (NEAT Paper).","DOI":"10.1007\/978-3-031-74776-2_15"},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.29007\/2ndp"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.1145\/3290354"},{"key":"e_1_3_3_38_2","unstructured":"Armando Solar-Lezama. 2023. 6.S981 Introduction to Program Synthesis Fall 2023. Retrieved March 13 2025 from https:\/\/people.csail.mit.edu\/asolar\/SynthesisCourse\/index.htm"},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0249-7"},{"key":"e_1_3_3_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065045"},{"key":"e_1_3_3_41_2","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009845"},{"key":"e_1_3_3_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/3219617.3219652"},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_1"},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37709-9_10"},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33125-1_10"},{"key":"e_1_3_3_46_2","doi-asserted-by":"publisher","unstructured":"Aditya V. Thakur and Thomas W. Reps. 2012. A generalization of St\u00e5lmarck\u2019s method. In Proceedings of the 19th International Symposium on Static Analysis (SAS \u201912) 334\u2013351. DOI: 10.1007\/978-3-642-33125-1_23","DOI":"10.1007\/978-3-642-33125-1_23"},{"key":"e_1_3_3_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_17"},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/3368826.3377910"},{"key":"e_1_3_3_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106263"},{"key":"e_1_3_3_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-021-00387-z"},{"key":"e_1_3_3_51_2","doi-asserted-by":"publisher","DOI":"10.1109\/CGO53902.2022.9741267"},{"key":"e_1_3_3_52_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37709-9_12"},{"key":"e_1_3_3_53_2","article-title":"Data-driven synthesis of provably sound side channel analyses","author":"Wang Jingbo","year":"2021","unstructured":"Jingbo Wang, Chungha Sung, Mukund Raghothaman, and Chao Wang. 2021. Data-driven synthesis of provably sound side channel analyses. In Proceedings of the 2021 IEEE\/ACM 43rd International Conference on Software Engineering (ICSE).","journal-title":"Proceedings of the 2021 IEEE\/ACM 43rd International Conference on Software Engineering (ICSE)"},{"key":"e_1_3_3_54_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_22"},{"key":"e_1_3_3_55_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_39"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3733716","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,21]],"date-time":"2026-01-21T16:32:36Z","timestamp":1769013156000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3733716"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,21]]},"references-count":54,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2026,2,28]]}},"alternative-id":["10.1145\/3733716"],"URL":"https:\/\/doi.org\/10.1145\/3733716","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,21]]},"assertion":[{"value":"2024-09-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-05","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-21","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}