{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,17]],"date-time":"2026-03-17T06:04:31Z","timestamp":1773727471808,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":47,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,11,8]],"date-time":"2020-11-08T00:00:00Z","timestamp":1604793600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020,11,8]]},"DOI":"10.1145\/3368089.3409757","type":"proceedings-article","created":{"date-parts":[[2020,11,8]],"date-time":"2020-11-08T06:03:47Z","timestamp":1604815427000},"page":"13-24","source":"Crossref","is-referenced-by-count":35,"title":["ARDiff: scaling program equivalence checking via iterative abstraction and refinement of common code"],"prefix":"10.1145","author":[{"given":"Sahar","family":"Badihi","sequence":"first","affiliation":[{"name":"University of British Columbia, Canada"}]},{"given":"Faridah","family":"Akinotcho","sequence":"additional","affiliation":[{"name":"University of British Columbia, Canada"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4562-8208","authenticated-orcid":false,"given":"Yi","family":"Li","sequence":"additional","affiliation":[{"name":"Nanyang Technological University, Singapore"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7280-1614","authenticated-orcid":false,"given":"Julia","family":"Rubin","sequence":"additional","affiliation":[{"name":"University of British Columbia, Canada"}]}],"member":"320","published-online":{"date-parts":[[2020,11,8]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"[n.d.]. Github. https:\/\/github.com.  [n.d.]. Github. https:\/\/github.com."},{"key":"e_1_3_2_1_2_1","unstructured":"[n.d.]. Refactoring GURU. https:\/\/refactoring.guru\/remove-assignments-toparameters.  [n.d.]. Refactoring GURU. https:\/\/refactoring.guru\/remove-assignments-toparameters."},{"key":"e_1_3_2_1_3_1","unstructured":"2019. ASM-DefUse. Software Analysis Experimentation Group ( 2019 ). https: \/\/github.com\/saeg\/asm-defuse.  2019. ASM-DefUse. Software Analysis Experimentation Group ( 2019 ). https: \/\/github.com\/saeg\/asm-defuse."},{"key":"e_1_3_2_1_4_1","unstructured":"2020. ARDif. https:\/\/ www.doi.org\/ 10.17605\/ OSF.IO\/ CHM2K. www.10.17605\/OSF.IO\/CHM2K.  2020. ARDif. https:\/\/ www.doi.org\/ 10.17605\/ OSF.IO\/ CHM2K. www.10.17605\/OSF.IO\/CHM2K."},{"key":"e_1_3_2_1_5_1","unstructured":"2020. Supplementary Materials. https:\/\/ resess.github.io\/ PaperAppendices\/ ARDif\/.  2020. Supplementary Materials. https:\/\/ resess.github.io\/ PaperAppendices\/ ARDif\/."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39176-7_7"},{"key":"e_1_3_2_1_7_1","unstructured":"Eric Bruneton Romain Lenglet and Thierry Coupaye. 2002. ASM: a Code Manipulation Tool to Implement Adaptable Systems. Adaptable and Extensible Component Systems 30 19 ( 2002 ).  Eric Bruneton Romain Lenglet and Thierry Coupaye. 2002. ASM: a Code Manipulation Tool to Implement Adaptable Systems. Adaptable and Extensible Component Systems 30 19 ( 2002 )."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58179-0_44"},{"key":"e_1_3_2_1_9_1","volume-title":"Proc. of the Symposium on Operating Systems Design and Implementation (OSDI). 209-224","author":"Cadar Cristian","year":"2008"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2591062.2591104"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-008-0053-x"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314596"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_15"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"crossref","unstructured":"Martin Davis. 1973. Hilbert's Tenth Problem is Unsolvable. The American Mathematical Monthly 80 3 ( 1973 ) 233-269.  Martin Davis. 1973. Hilbert's Tenth Problem is Unsolvable. The American Mathematical Monthly 80 3 ( 1973 ) 233-269.","DOI":"10.1080\/00029890.1973.11993265"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Martin Davis. 1973. Hilbert's Tenth Problem is Unsolvable. The American Mathematical Monthly 80 3 ( 1973 ) 233-269.  Martin Davis. 1973. Hilbert's Tenth Problem is Unsolvable. The American Mathematical Monthly 80 3 ( 1973 ) 233-269.","DOI":"10.1080\/00029890.1973.11993265"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"crossref","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner. 2011. Satisfiability Modulo Theories: Introduction and Applications. Commun. ACM 54 9 ( 2011 ) 69-77.  Leonardo De Moura and Nikolaj Bj\u00f8rner. 2011. Satisfiability Modulo Theories: Introduction and Applications. Commun. ACM 54 9 ( 2011 ) 69-77.","DOI":"10.1145\/1995376.1995394"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2635868.2635889"},{"key":"e_1_3_2_1_20_1","volume-title":"Proc. of the International Conference on Automated Software Engineering (ASE). 313-324","author":"Falleri Jean-R\u00e9my","year":"2014"},{"key":"e_1_3_2_1_21_1","volume-title":"Proc. of the International Conference on Computer Aided Verification. 433-453","author":"Fedyukovich Grigory","year":"2016"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2642937.2642987"},{"key":"e_1_3_2_1_23_1","article-title":"The Program Dependence Graph and Its Use in Optimization","volume":"9","author":"Ferrante Jeanne","year":"1987","journal-title":"Transactions on Programming Languages and Systems (TOPLAS)"},{"key":"e_1_3_2_1_24_1","unstructured":"M. Fowler. [n.d.]. Refactoring home page. https:\/\/refactoring.com\/catalog\/.  M. Fowler. [n.d.]. Refactoring home page. https:\/\/refactoring.com\/catalog\/."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-008-0075-2"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Benny Godlin and Ofer Strichman. 2013. Regression verification: proving the equivalence of similar programs. Software Testing Verification and Reliability 23 3 ( 2013 ) 241-258.  Benny Godlin and Ofer Strichman. 2013. Regression verification: proving the equivalence of similar programs. Software Testing Verification and Reliability 23 3 ( 2013 ) 241-258.","DOI":"10.1002\/stvr.1472"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.2307\/2274706"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","unstructured":"James C King. 1976. Symbolic Execution and Program Testing. Commun. ACM 19 7 ( 1976 ) 385-394.  James C King. 1976. Symbolic Execution and Program Testing. Commun. ACM 19 7 ( 1976 ) 385-394.","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74105-3_3"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.1997.597155"},{"key":"e_1_3_2_1_31_1","volume-title":"Proc. of the International Conference on Computer Aided Verification (CAD). 712-717","author":"Lahiri Shuvendu K","year":"2012"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2970276.2970364"},{"key":"e_1_3_2_1_33_1","unstructured":"Yu-Seung Ma and Jef Ofutt. [n.d.]. Description of muJava's Method-level Mutation Operators. ([n. d.]).  Yu-Seung Ma and Jef Ofutt. [n.d.]. Description of muJava's Method-level Mutation Operators. ([n. d.])."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238178"},{"key":"e_1_3_2_1_35_1","first-page":"152","article-title":"Property Directed Inference of Relational Invariants","author":"Mordvinov Dmitry","year":"2019","journal-title":"Proc. of Formal Methods in Computer Aided Design (FMCAD)."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884845"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1858996.1859035"},{"key":"e_1_3_2_1_38_1","volume-title":"Proc. of the International Symposium on Foundations of Software Engineering (FSE).","author":"Person Suzette","year":"2008"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_9"},{"key":"e_1_3_2_1_40_1","volume-title":"Numerical Recipes","author":"Press William H","edition":"3"},{"key":"e_1_3_2_1_41_1","volume-title":"Proc. of the International Conference on Computer Aided Verification (CAV). 669-685","author":"Ramos David A","year":"2011"},{"key":"e_1_3_2_1_42_1","volume-title":"Proc. of the Formal Methods in Computer-Aided Design Conference. 114-427","author":"Sery Ondrej","year":"2012"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_9"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_26"},{"key":"e_1_3_2_1_45_1","volume-title":"Proc. of the International Static Analysis Symposium (SAS). 405-427","author":"Trostanetski Anna","year":"2017"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.1997.632832"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985876"}],"event":{"name":"ESEC\/FSE '20: 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering","location":"Virtual Event USA","acronym":"ESEC\/FSE '20","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3368089.3409757","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3368089.3409757","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:01:58Z","timestamp":1750197718000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3368089.3409757"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,8]]},"references-count":47,"alternative-id":["10.1145\/3368089.3409757","10.1145\/3368089"],"URL":"https:\/\/doi.org\/10.1145\/3368089.3409757","relation":{},"subject":[],"published":{"date-parts":[[2020,11,8]]}}}