SAT-DIFF: A Tree Diffing Framework Using SAT Solving
Abstract
Computing differences between tree-structured data is a critical but challenging problem in software analysis. In this paper, we propose a novel tree diffing approach called SatDiff, which reformulates the structural diffing problem into a MaxSAT problem. By encoding the necessary transformations from the source tree to the target tree, SatDiff generates correct, minimal, and type safe low-level edit scripts with formal guarantees. We then synthesize concise high-level edit scripts by effectively merging low-level edits in the appropriate topological order. Our empirical results demonstrate that SatDiff outperforms existing heuristic-based approaches by a significant margin in terms of conciseness while maintaining a reasonable runtime.
Cite
@article{arxiv.2404.04731,
title = {SAT-DIFF: A Tree Diffing Framework Using SAT Solving},
author = {Chuqin Geng and Haolin Ye and Yihan Zhang and Brigitte Pientka and Xujie Si},
journal= {arXiv preprint arXiv:2404.04731},
year = {2024}
}
Comments
23 pages, 7 figures