Detail práce
Equivalence-Based Slicing of Programs
Cieľom tejto práce je navrhnúť metódu, ktorá zjednoduší dva porovnávané programy na základe výsledkov ich sémantickej analýzy. Cieľom je odstránenie čo najväčšieho množstva sémanticky ekvivalentných častí porovnávaných programov. Pre nájdenie týchto ekvivalentných častí aplikujeme vlastné riešenie problému nájdenia najväčšieho spoločného indukovaného podgrafu. Následne sme schopní zjednodušiť programy využitím spätného statického prerezávania. Aplikáciou tohto zjednodušenia získame prerezané programy, ktoré obsahujú rozdielne časti a časti programov, ktoré môžu tieto rozdiely ovplyvniť. Táto metóda je naimplementovaná ako rozšírenie nástroja DiffKemp, čo je statický analyzátor sémantických rozdielov medzi rôznymi verziami rozsiahlych programov. Experimenty vykonané na jadrách Linux-u ukazujú, že metóda je schopná veľmi efektívne vyprodukovať korektné prerezané programy (analýza sa predĺžila len o 3.2%). Navyše, vzniknuté prerezané programy sú omnoho menšie, ako originálne, čo ich činí vhodnými pre ďalšiu analýzu.
DiffKemp, statická analýza, spätné statické prerezávanie programov, najväčší spoločný indukovaný podgraf
Studentka nejprve prezentovala výsledky, kterých dosáhla v rámci své práce. Komise se poté seznámila s hodnocením vedoucího a posudkem oponenta práce. Studentka následně odpověděla na otázky oponenta. Komise se na základě posudku oponenta, hodnocení vedoucího, přednesené prezentace a odpovědí studentky na položené otázky rozhodla práci hodnotit stupněm A.
- On page 9 of your thesis, you say you simplified the presentation wrt the original algorithm used by DiffKemp by considering an instruction-by-instruction comparison only. Is it really a simplification of the presentation only? This is, does your tool support dealing with more general comparisons than instruction-by-instruction?
- Have you ever tried at least a simple experiment with applying some heavy-weight formal verifier, such as LLReve, on the code simplified by you? You mention that you reduced the changed code by 54.8 % overall. I am afraid that this needs still not be enough for the heavy weight tools to succeed. However, perhaps you saw some (many?) particular functions reduced much more so that LLReve would indeed catch up? May be this could even be tried for the defence?
- If there is enough time, you could comment on some of the issues mentioned in the part of the review devoted to the writing of your thesis. Particularly, points 12, 8, 3, and 10 are interesting from my point of view (in this order).
Kořenek Jan, doc. Ing., Ph.D. (UPSY FIT VUT), člen
Peringer Petr, Dr. Ing. (UITS FIT VUT), člen
Ryšavý Ondřej, doc. Ing., Ph.D. (UIFS FIT VUT), člen
@bachelorsthesis{FITBT24038,
author = "Tatiana Malecov\'{a}",
type = "Bakal\'{a}\v{r}sk\'{a} pr\'{a}ce",
title = "Equivalence-Based Slicing of Programs",
school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}",
year = 2021,
location = "Brno, CZ",
language = "english",
url = "https://www.fit.vut.cz/study/thesis/24038/"
}