Detail práce
A Decision Procedure for Strong-Separation Logic
Separační logika (SL) patří mezi nejúspěšnější nástroje pro verifikaci programů pracujících s dynamicky alokovanou pamětí. Její vysoká expresivita ovšem přináší nerozhodnutelnost pokud formule kombinují více jejích spojek, především separační implikace. Jako řešení byla navrhnuta takzvaná silně-separační logika (SSL), která díky striktnější definici sémantiky rozšiřuje rozhodnutelný fragment a přitom zůstává vhodná pro verifikaci programů. V současnosti ale neexistuje žádná implementace rozhodovací procedury pro tuto logiku. Tato práce se zaměřuje na návrh a implementaci rozhodovací procedury pro SSL založené na překladu vstupní formule na formuli v prvořádové logice, jejíž splnitelnost je poté možné ověřit pomocí specializovaných nástrojů. Experimentální výsledky na omezeném fragmentu, kde SL a SSL splývají, ukazují, že navržený nástroj je schopen efektivně řešit formule pocházející z verifikačních nástrojů a výrazně překonává všechny ostatní existující rozhodovací procedury, které jsou také založené na překladu. Během experimentů jsme také odhalili několik případů nekorektnosti heuristik použitých v rozhodovací proceduře pro SL implementované v nástroji cvc5. Na základě našich hlášení byly tyto heuristiky opraveny.
Separační logika, silně-separační logika, rozhodovací procedura, SMT
Student nejprve prezentoval výsledky, kterých dosáhl v rámci své práce. Komise se poté seznámila s hodnocením vedoucího a posudkem oponenta práce. Student následně odpověděl na otázky oponenta a na další otázky přítomných. Komise se na základě posudku oponenta, hodnocení vedoucího, přednesené prezentace a odpovědí studenta na položené otázky rozhodla práci hodnotit stupněm A.
- Je vaše práce použitelná i pro složitější struktury než jen seznamy?
- Kde je možné výsledek vaší práce prakticky použít?
Drábek Vladimír, doc. Ing., CSc. (UPSY FIT VUT), člen
Matoušek Petr, doc. Ing., Ph.D., M.A. (UIFS FIT VUT), člen
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT), člen
Ryšavý Ondřej, doc. Ing., Ph.D. (UIFS FIT VUT), člen
Zbořil František, doc. Ing., Ph.D. (UITS FIT VUT), člen
@mastersthesis{FITMT25151,
author = "Tom\'{a}\v{s} Dac\'{i}k",
type = "Diplomov\'{a} pr\'{a}ce",
title = "A Decision Procedure for Strong-Separation Logic",
school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}",
year = 2022,
location = "Brno, CZ",
language = "english",
url = "https://www.fit.vut.cz/study/thesis/25151/"
}