Publication Details
Automatically Checking Semantic Equivalence between Versions of Large-Scale C Projects
semantic equivalence, refactoring, static analysis, semantics-preserving patterns, refactoring patterns
Motivated by a need of some software projects to ensure semantic stability of some of their core parts, the paper proposes a highly-scalable approach for automatically checking semantic equivalence of different versions of large C projects, with a particular focus on the Linux kernel. The proposed method uses a novel combination of pattern matching with light-weight static analysis and control-flow transformations. Although the method cannot prove equivalence on heavily refactored code, it can compare thousands of functions in minutes while producing a low number of false non-equality verdicts as our experiments show. We implemented our approach in a tool called DiffKemp and we show that DiffKemp, unlike other existing tools, gives practically useful results even on projects of the size of the Linux kernel.
@inproceedings{BUT175787,
author="Viktor {Malík} and Tomáš {Vojnar}",
title="Automatically Checking Semantic Equivalence between Versions of Large-Scale C Projects",
booktitle="2021 14th IEEE Conference on Software Testing, Verification and Validation (ICST)",
year="2021",
pages="329--339",
publisher="Institute of Electrical and Electronics Engineers",
address="Porto de Galinhas",
doi="10.1109/ICST49551.2021.00045",
isbn="978-1-7281-6837-1",
url="https://ieeexplore.ieee.org/document/9438578"
}