Verified Three-Way Program Merge
summary
Claims a verifiable definition of semantic conflict freedom and a Java prototype called SafeMerge that uses a four-way AST diff to produce a shared program with holes plus edit scripts, then composes lightweight uninterpreted-function summaries for shared code with a precise four-way product for edits. Evaluated on 52 real GitHub merge scenarios: verifies 39 as conflict-free, reports 13 semantic conflicts (five of which slipped past a textual merge like KD3, three likely real bugs), and runs in 0.5s average (max 4.5s).
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:17What is a threeway merge
- 4:40Vulnerability
- 5:35Limitations
- 6:30Semantic Conflict Freedom
- 8:25Relational Verification
- 9:54Complex Example
- 11:41Verification
- 14:18Implementation details
- 18:38Conclusion
related talks
28mCode Merging Using Transformations and Member Identity
22mShifting Left, Shifting Right
32mCorrectness Witnesses for Concurrent Programs: Bridging the Semantic Divide with Ghosts
01h 05mVerifying Infinitely Many Programs at Once
57mInvited Talk: Bridging Safety and Performance
01h 00mSOAP - Keynote: Formal Reasoning and the Hacker Way
01h 00mCooperative Verification: Towards Reliable Safety-Critical Systems
30mPutting the Semantics into Semantic Versioning