Automatically Checking Semantic Equivalence between Versions of Large-Scale C Projects

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F21%3APU142910" target="_blank" >RIV/00216305:26230/21:PU142910 - isvavai.cz</a>

Výsledek na webu

<a href="https://ieeexplore.ieee.org/document/9438578" target="_blank" >https://ieeexplore.ieee.org/document/9438578</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1109/ICST49551.2021.00045" target="_blank" >10.1109/ICST49551.2021.00045</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Automatically Checking Semantic Equivalence between Versions of Large-Scale C Projects

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Automatically Checking Semantic Equivalence between Versions of Large-Scale C Projects

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

<a href="/cs/project/GA20-07487S" target="_blank" >GA20-07487S: Škálovatelné techniky pro analýzu komplexních vlastností počítačových systémů</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2021

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

2021 14th IEEE Conference on Software Testing, Verification and Validation (ICST)

ISBN

978-1-7281-6837-1

ISSN

—

e-ISSN

—

Počet stran výsledku

11

Strana od-do

329-339

Název nakladatele

Institute of Electrical and Electronics Engineers

Místo vydání

Porto de Galinhas

Místo konání akce

Porto de Galinhas, Brazil

Datum konání akce

12. 4. 2021

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

000680831800033