  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 confict-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 dependence
analysis for shared program fragments and precise relational reasoning for the
modifications. We evaluate our tool called SafeMerge on 52 real-world merge
scenarios obtained from Github and compare the results against a textual merge
tool. The experimental results demonstrate the benefits of our approach over
syntactic confict-freedom and indicate that SafeMerge is both precise and
practical.
