Verified Three-Way Program Merge

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 presenting an automated technique to verify \emph{semantic conflict freedom}, which ensures that the merged program does not introduce new unwanted behaviors.

Our verification algorithm is compositional in that it reasons about different edits in isolation and combines them to obtain an overall proof of conflict freedom. We have implemented our algorithm in a tool called SafeMerge and evaluate it on 52 real-world merge scenarios obtained from Github repositories. The experimental results corroborate the benefits of our approach over syntactic conflict-freedom and demonstrate that SafeMerge is both precise and practical.