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"
}