{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,29]],"date-time":"2026-01-29T21:54:51Z","timestamp":1769723691305,"version":"3.49.0"},"reference-count":46,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2018,10,24]],"date-time":"2018-10-24T00:00:00Z","timestamp":1540339200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100006602","name":"AFRL","doi-asserted-by":"crossref","award":["8750-14-2-0270"],"award-info":[{"award-number":["8750-14-2-0270"]}],"id":[{"id":"10.13039\/100006602","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-1712067"],"award-info":[{"award-number":["CCF-1712067"]}],"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":[[2018,10,24]]},"abstract":"<jats:p>Even though many programmers rely on 3-way merge tools to integrate changes from different branches, such tools can introduce subtle bugs in the integration process. This paper aims to mitigate this problem by defining a semantic notion of conflict-freedom, which ensures that the merged program does not introduce new unwanted behaviors. We also show how to verify this property using a novel, compositional algorithm that combines lightweight summarization for shared program fragments with precise relational reasoning for the modifications. Towards this goal, our method uses a 4-way differencing algorithm on abstract syntax trees to represent different program versions as edits applied to a shared program with holes. This representation allows our verification algorithm to reason about different edits in isolation and compose them to obtain an overall proof of conflict freedom. We have implemented the proposed technique in a new tool called SafeMerge for Java and evaluate it on 52 real-world merge scenarios obtained from Github. The experimental results demonstrate the benefits of our approach over syntactic conflict-freedom and indicate that SafeMerge is both precise and practical.<\/jats:p>","DOI":"10.1145\/3276535","type":"journal-article","created":{"date-parts":[[2018,10,24]],"date-time":"2018-10-24T11:57:18Z","timestamp":1540382238000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":33,"title":["Verified three-way program merge"],"prefix":"10.1145","volume":"2","author":[{"given":"Marcelo","family":"Sousa","sequence":"first","affiliation":[{"name":"University of Oxford, UK"}]},{"given":"Isil","family":"Dillig","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, USA"}]},{"given":"Shuvendu K.","family":"Lahiri","sequence":"additional","affiliation":[{"name":"Microsoft Research, USA"}]}],"member":"320","published-online":{"date-parts":[[2018,10,24]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2351676.2351694"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2025113.2025141"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54494-5_9"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/2021296.2021319"},{"key":"e_1_2_2_5_1","volume-title":"Juan Manuel Crespo, and C\u00e9sar Kunz","author":"Barthe Gilles","year":"2013"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/982962.964003"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2013.28"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133883"},{"key":"e_1_2_2_9_1","unstructured":"David Wheeler. 2017. The Apple goto fail vulnerability: lessons learned. http:\/\/www.dwheeler.com\/essays\/apple-goto-fail. html . (2017).  David Wheeler. 2017. The Apple goto fail vulnerability: lessons learned. http:\/\/www.dwheeler.com\/essays\/apple-goto-fail. html . (2017)."},{"key":"e_1_2_2_10_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Moura Leonardo De"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1925844.1926407"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASWEC.2013.32"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2642937.2642987"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/647540.730008"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512558"},{"key":"e_1_2_2_16_1","unstructured":"Fowler Martin. 2011. Semantic Conflict. https:\/\/martinfowler.com\/bliki\/SemanticConflict.html . (2011).  Fowler Martin. 2011. Semantic Conflict. https:\/\/martinfowler.com\/bliki\/SemanticConflict.html . (2011)."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-008-0075-2"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/2337223.2337264"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_20"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/322033.322044"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/65979.65980"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/645543.655704"},{"key":"e_1_2_2_23_1","unstructured":"John Gruber. 2014. On the Timing of iOS\u2019s SSL Vulnerability. https:\/\/daringfireball.net\/2014\/02\/apple_prism . (2014).  John Gruber. 2014. On the Timing of iOS\u2019s SSL Vulnerability. https:\/\/daringfireball.net\/2014\/02\/apple_prism . (2014)."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/1781794.1781836"},{"key":"e_1_2_2_25_1","unstructured":"Knoy Gabriel. 2012. How Often Does Gitmerge make mistakes? https:\/\/news.ycombinator.com\/item?id=9871042 . (2012).  Knoy Gabriel. 2012. How Often Does Gitmerge make mistakes? https:\/\/news.ycombinator.com\/item?id=9871042 . (2012)."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_54"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491452"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-014-0151-5"},{"key":"e_1_2_2_29_1","unstructured":"Lee TK. 2012. The Problem of Automatic Code Merging. http:\/\/www.personal.psu.edu\/txl20\/blogs\/tks_tech_notes\/2012\/03\/ the-problem-of-automatic-code-merging.html . (2012).  Lee TK. 2012. The Problem of Automatic Code Merging. http:\/\/www.personal.psu.edu\/txl20\/blogs\/tks_tech_notes\/2012\/03\/ the-problem-of-automatic-code-merging.html . (2012)."},{"key":"e_1_2_2_30_1","unstructured":"Lenski Dan. 2015. Is it possible for Git merging to make a mistake without detecting a conflict? https:\/\/www.quora.com\/ Is-it-possible-for-Git-merging-to-make-a-mistake-without-detecting-a-conflict . (2015).  Lenski Dan. 2015. Is it possible for Git merging to make a mistake without detecting a conflict? https:\/\/www.quora.com\/ Is-it-possible-for-Git-merging-to-make-a-mistake-without-detecting-a-conflict . (2015)."},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594326"},{"key":"e_1_2_2_32_1","unstructured":"Lutton Mark. 2014. Infinite Loop Caused by Git Merge. https:\/\/stackoverflow.com\/questions\/23523713\/ how-can-i-trust-git-merge . (2014).  Lutton Mark. 2014. Infinite Loop Caused by Git Merge. https:\/\/stackoverflow.com\/questions\/23523713\/ how-can-i-trust-git-merge . (2014)."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2601248.2601275"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660245"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1453101.1453131"},{"key":"e_1_2_2_36_1","volume-title":"CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings . 669\u2013685","author":"David"},{"key":"e_1_2_2_37_1","unstructured":"Reddit. 2017a. Automatic Merge Mistakes. https:\/\/www.reddit.com\/r\/git\/comments\/5bssjv\/automatic_merge_mistakes\/ . (2017).  Reddit. 2017a. Automatic Merge Mistakes. https:\/\/www.reddit.com\/r\/git\/comments\/5bssjv\/automatic_merge_mistakes\/ . (2017)."},{"key":"e_1_2_2_38_1","unstructured":"Reddit. 2017b. How Do you Deal with Auto Merge? https:\/\/www.reddit.com\/r\/git\/comments\/5hn80k\/how_do_you_deal_ with_auto_merge\/ . (2017).  Reddit. 2017b. How Do you Deal with Auto Merge? https:\/\/www.reddit.com\/r\/git\/comments\/5hn80k\/how_do_you_deal_ with_auto_merge\/ . (2017)."},{"key":"e_1_2_2_39_1","unstructured":"Rostedt Steven. 2011. Fix Bug Caused by Git Merge. http:\/\/lkml.iu.edu\/hypermail\/linux\/kernel\/1106.0\/00645.html . (2011).  Rostedt Steven. 2011. Fix Bug Caused by Git Merge. http:\/\/lkml.iu.edu\/hypermail\/linux\/kernel\/1106.0\/00645.html . (2011)."},{"key":"e_1_2_2_40_1","unstructured":"SlashDot. 2014. Apple SSL Bug In iOS Also Affects OS X. http:\/\/apple.slashdot.org\/story\/14\/02\/22\/2143224\/ apple-ssl-bug-in-ios-also-affects-os-x . (2014).  SlashDot. 2014. Apple SSL Bug In iOS Also Affects OS X. http:\/\/apple.slashdot.org\/story\/14\/02\/22\/2143224\/ apple-ssl-bug-in-ios-also-affects-os-x . (2014)."},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908092"},{"key":"e_1_2_2_42_1","doi-asserted-by":"crossref","volume-title":"Secure information flow as a safety problem","author":"Terauchi Tachio","DOI":"10.1007\/11547662_24"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_35"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.036"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/99278.99290"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_5"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3276535","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3276535","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3276535","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:03:39Z","timestamp":1750273419000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3276535"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10,24]]},"references-count":46,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2018,10,24]]}},"alternative-id":["10.1145\/3276535"],"URL":"https:\/\/doi.org\/10.1145\/3276535","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,10,24]]},"assertion":[{"value":"2018-10-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}