The thesis integrates formal methods into the DiffKemp tool, which is a tool applying advanced static program analysis techniques for checking program equivalence. The tool has been developed by the VeriFIT research group in cooperation with Red Hat. The complexity of the assignment itself is above average since it required to study and understand a complex research project (both the implementation and the related publications), advanced formal methods techniques (SMT solving), and propose and implement a novel approach integrating SMT solving into DiffKemp. The thesis has succeeded to fulfill the assignment and significantly improves the capabilities of DiffKemp in terms of analyzing complicated code refactorings. At the same time, the thesis is a solid base for future work and research.

The work has been presented at the student conference Excel@FIT 2024. At the same time, the student has helped with preparing a journal version of a research paper on DiffKemp which is to be submitted to the TOSEM journal (Q1). In addition, as already mentioned, the thesis is a good basis for further research which could potentially result in a publication on an international scientific conference.

I'd also like to mention that František has been collaborating with me since his bachelor study on a different tool for formal verification of C programs called 2LS. Despite switching to a different topic for his Master's thesis, he still managed to help preparing 2LS for this year's volume of International Competition on Software Verification 2024.

The student was very active during the entire academic year, we had regular weekly meetings where he almost every time presented new progress with the thesis.

Stupeň hodnocení: zadání splněno

Zadání práce bylo jednoznačně splněno.

Technická zpráva je strukturována logicky, jednotlivé kapitoly a sekce na sebe dobře navazují a mají vhodně zvolený rozsah. Text je až na několik výjimek technicky přesný, velmi dobře čitelný a doprovozený dobře zvolenými ilustračními příklady.

Zmíněné drobné výjimky jsou z mého pohledu dvě: (1) Na straně 17 v bodě 1 mi není jasné, co jsou „sequential code blocks“ a jaká je jejich vazba na základní bloky kódu. (2) V popisu zakódování dotazů na ekvivalenci zvolených bloků kódu do formy SMT problému na konci úvodní části sekce 4.2 (strana 20) by zřejmě měla být nějakým způsobem zajištěna disjunktnost proměnných, s nimiž se pracuje (a která je pak zajištěna příslušným indexováním v příkladu v sekci 4.2.3). Tyto nedostatky nicméně považuji za drobné a současně se vztahující na náročnější pasáže popisu.

Výběr studijních pramenů je vhodný, zdroje jsou vhodně citovány (snad jen na straně 24 mohla být příslušná citace umístěna uvnitř věty, ne mimo ni).

Práce významně rozšiřuje soubor metod používaných nástrojem DiffKemp pro ověřování sémantické shody rozsáhlých nízko-úrovňových programů, které prošly refaktorováním. Nástroj DiffKemp je jedním z klíčových výzkumných projektů mezi společností Red Hat a univerzitami (zejména, ale nejen FIT VUT). Nástroj ještě není prakticky nasazen, ale je zde solidní naděje, že k tomu dojde. Nástroj posouvá hranice poznání v oblasti posuzování sémantické shody na rozsáhlém systémovém kódu. Studentem vytvořené rozšíření sice nerozřešilo velký počet reálných změn v kódu, které dosud DiffKemp nezvládnul, ale několik takových reálných případů se objevilo. Jedná se přitom o první krok k nalezení vhodného způsobu kombinace „leightweight“ přístupů používaných nástrojem DiffKemp jako primárních s „heavyweight“ přístupy, které méně škálují, ale zvládnou ověřit výraznější změny kódu. Další výzkum v této oblasti je předpokládán, včetně studentovy účasti na něm. Student svou prací a experimenty s nástrojem DiffKemp současně přispěl k dokončovanému článku o metodách stojících za nástrojem DiffKemp, který bude zaslán do časopisu ACM TOSEM, WoS IF Q1/AIS Q2 (se studentem jako spoluautorem).