SAT-DIFF: A Tree Diffing Framework Using SAT Solving
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866913304623972352 |
|---|---|
| author | Geng, Chuqin Ye, Haolin Zhang, Yihan Pientka, Brigitte Si, Xujie |
| author_facet | Geng, Chuqin Ye, Haolin Zhang, Yihan Pientka, Brigitte Si, Xujie |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2404_04731 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | SAT-DIFF: A Tree Diffing Framework Using SAT Solving Geng, Chuqin Ye, Haolin Zhang, Yihan Pientka, Brigitte Si, Xujie Programming Languages Software Engineering 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. |
| title | SAT-DIFF: A Tree Diffing Framework Using SAT Solving |
| topic | Programming Languages Software Engineering |
| url | https://arxiv.org/abs/2404.04731 |