{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,11]],"date-time":"2026-07-11T02:46:08Z","timestamp":1783737968381,"version":"3.55.0"},"reference-count":75,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1762299"],"award-info":[{"award-number":["CCF-1762299"]}],"id":[{"id":"10.13039\/100000001","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":[[2024,1,2]]},"abstract":"<jats:p>\n            Modifications to the data representation of an abstract data type (ADT) can require significant semantic refactoring of the code. Motivated by this observation, this paper presents a new method to automate semantic code refactoring tasks. Our method takes as input the original ADT implementation, a new data representation, and a so-called\n            <jats:italic toggle=\"yes\">relational representation invariant<\/jats:italic>\n            (relating the old and new data representations), and automatically generates a new ADT implementation that is semantically equivalent to the original version. Our method is based on counterexample-guided inductive synthesis (CEGIS) but leverages three key ideas that allow it to handle real-world refactoring tasks. First, our approach reduces the underlying relational synthesis problem to a set of (simpler) programming-by-example problems, one for each method in the ADT. Second, it leverages symbolic reasoning techniques, based on logical abduction, to deduce code snippets that should occur in the refactored version. Finally, it utilizes a notion of\n            <jats:italic toggle=\"yes\">partial equivalence<\/jats:italic>\n            to make inductive synthesis much more effective in this setting. We have implemented the proposed approach in a new tool called\n            <jats:sc>Revamp<\/jats:sc>\n            for automatically refactoring Java classes and evaluated it on 30 Java class mined from Github. Our evaluation shows that\n            <jats:sc>Revamp<\/jats:sc>\n            can correctly refactor the entire ADT in 97% of the cases and that it can successfully re-implement 144 out of the 146 methods that require modifications.\n          <\/jats:p>","DOI":"10.1145\/3632870","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"816-847","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Semantic Code Refactoring for Abstract Data Types"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9253-9585","authenticated-orcid":false,"given":"Shankara","family":"Pailoor","sequence":"first","affiliation":[{"name":"University of Texas, Austin, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3370-2431","authenticated-orcid":false,"given":"Yuepeng","family":"Wang","sequence":"additional","affiliation":[{"name":"Simon Fraser University, Vancouver, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8006-1230","authenticated-orcid":false,"given":"I\u015f\u0131l","family":"Dillig","sequence":"additional","affiliation":[{"name":"University of Texas, Austin, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","unstructured":"2003. bind8 negative cache poison attack. https:\/\/vulners.com\/freebsd\/F04CC5CB-2D0B-11D8-BEAF-000A95C4D922."},{"key":"e_1_3_1_3_1","unstructured":"2005. CVE-2005-0034. https:\/\/nvd.nist.gov\/vuln\/detail\/CVE-2005-0034."},{"key":"e_1_3_1_4_1","unstructured":"2009. Linux devs exterminate security bugs from kernel. https:\/\/www.theregister.com\/2009\/12\/11\/linux_kernel_bugs_patched\/."},{"key":"e_1_3_1_5_1","unstructured":"2013. Google Cloud Platform (GCP). https:\/\/cloud.google.com\/."},{"key":"e_1_3_1_6_1","unstructured":"2022. Cassandra. https:\/\/github.com\/apache\/cassandra."},{"key":"e_1_3_1_7_1","unstructured":"2022. Elessandra. https:\/\/github.com\/strapdata\/elassandra."},{"key":"e_1_3_1_8_1","unstructured":"2022. How refactoring code in Safari\u2019s WebKit resurrected \u2018zombie\u2019 security bug. https:\/\/www.theregister.com\/2022\/06\/21\/apple-safari-zombie-exploit\/."},{"key":"e_1_3_1_9_1","unstructured":"2022. Netty. https:\/\/github.com\/netty\/netty."},{"key":"e_1_3_1_10_1","unstructured":"2023. Glide. https:\/\/github.com\/bumptech\/glide."},{"key":"e_1_3_1_11_1","unstructured":"2023. Wicket. https:\/\/github.com\/apache\/wicket."},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2914770.2837628"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66158-2_44"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660203"},{"key":"e_1_3_1_15_1","unstructured":"Rajeev Alur Pavol Cern\u00fd and Arjun Radhakrishna. 2015. Synthesis through Unification. CoRR abs\/1505.05868 (2015). arXiv:1505.05868 http:\/\/arxiv.org\/abs\/1505.05868"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563308"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462180"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_10"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677006"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/949305.949314"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE.2003.1251032"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1062455.1062499"},{"key":"e_1_3_1_25_1","unstructured":"DiffChecker. 2021. DiffChecker. https:\/\/www.diffchecker.com\/"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014657"},{"key":"e_1_3_1_28_1","doi-asserted-by":"crossref","first-page":"684","DOI":"10.1007\/978-3-642-39799-8_46","volume-title":"Computer Aided Verification","author":"Dillig Isil","year":"2013","unstructured":"Isil Dillig and Thomas Dillig. 2013. Explain: A Tool for Performing Abductive Inference. In Computer Aided Verification, Natasha Sharygina and Helmut Veith (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 684\u2013689."},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254087"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509136.2509511"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-11245-5_5"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2737977"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2012.6227192"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792878.1792899"},{"key":"e_1_3_1_36_1","first-page":"57","volume-title":"Enumerative Search","author":"Gulwani Sumit","year":"2017","unstructured":"Sumit Gulwani, Oleksandr Polozov, and Rishabh Singh. 2017. Enumerative Search. Now Publishers Inc., 57\u201364."},{"key":"e_1_3_1_37_1","unstructured":"Sumit Gulwani and Ramarathnam Venkatesan. 2009. Component Based Synthesis Applied to Bitvector Circuits. Technical Report MSR-TR-2010-12. https:\/\/www.microsoft.com\/en-us\/research\/publication\/component-based-synthesis-applied-to-bitvector-circuits\/"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/359657.359666"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993504"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254114"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2380656.2380677"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062345"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-32304-2_17"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-22308-2_13"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454087"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2803189"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806833"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSM.2001.972794"},{"key":"e_1_3_1_49_1","doi-asserted-by":"crossref","first-page":"430","DOI":"10.1007\/978-3-642-14295-6_38","volume-title":"Computer Aided Verification","author":"Kuncak Viktor","year":"2010","unstructured":"Viktor Kuncak, Mika\u00ebl Mayer, Ruzica Piskac, and Philippe Suter. 2010a. Comfusy: A Tool for Complete Functional Synthesis. In Computer Aided Verification, Tayssir Touili, Byron Cook, and Paul Jackson (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 430\u2013433."},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806632"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2076450.2076472"},{"key":"e_1_3_1_52_1","unstructured":"Patrick Lam Eric Bodden Ondrej Lhot\u00e1k and Laurie Hendren. 2011. The Soot framework for Java program analysis: a retrospective."},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30579-8_28"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31985-6_16"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434335"},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36579-6_12"},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3180155.3180211"},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908122"},{"key":"e_1_3_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158089"},{"key":"e_1_3_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341699"},{"key":"e_1_3_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385967"},{"key":"e_1_3_1_62_1","unstructured":"OpenAI. 2021. ChatGPT. https:\/\/openai.com"},{"key":"e_1_3_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454063"},{"key":"e_1_3_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133889"},{"key":"e_1_3_1_65_1","doi-asserted-by":"publisher","unstructured":"Malavika Samak Deokhwan Kim and Martin C. Rinard. 2019. Synthesizing Replacement Classes. Proc. ACM Program. Lang. 4 POPL Article 52 (dec 2019) 33 pages. https:\/\/doi.org\/10.1145\/3371120 10.1145\/3371120","DOI":"10.1145\/3371120"},{"key":"e_1_3_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290386"},{"key":"e_1_3_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375599"},{"key":"e_1_3_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065045"},{"key":"e_1_3_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_3_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993557"},{"key":"e_1_3_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/1961204.1961205"},{"key":"e_1_3_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594340"},{"key":"e_1_3_1_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314588"},{"key":"e_1_3_1_74_1","doi-asserted-by":"publisher","DOI":"10.14778\/3384345.3384350"},{"key":"e_1_3_1_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276525"},{"key":"e_1_3_1_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/3187009.3177735"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632870","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632870","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632870","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:07:44Z","timestamp":1751659664000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632870"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":75,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632870"],"URL":"https:\/\/doi.org\/10.1145\/3632870","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}