Detail práce
Generic Template-Based Synthesis of Program Abstractions
Cieľom tejto práce je návrh a implementácia generického strategy solveru pre nástroj 2LS.2LS je analyzátor na statickú verifikáciu programov napísaných v jazyku C. Verifikovanýprogram je za využita abstraktnej interpretácie analyzovaný SMT solverom. Prevod z ab-straktného stavu programu do logickej formule, s ktorou vie pracovať SMT solver vykonávakomponenta nazývaná strategy solver. Aktuálne pre každú doménu existuje jeden takýtosolver. Navrhované riešenie vytvára jeden obecný strategy solver, ktorý zjednodušuje tvorbunových domén. Zároveň navrhovaný spôsob umožnuje prevedenie existujúcich domén a tedazmenšuje program analyzátora.
formálna verifikácia, 2LS, statická analýza, SSA forma, abstraktná doména, strategy solver,SMT solving, abstraktná interpretácia
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 B.
Pokud 2LS stojí na SAT solverech, bylo by užitečné zapojit SMT solvery?
Vysvětlete rovnici 4.9.
Máte představu, zda by vaše verze 2LS měla znatelně lepší výsledky v soutěži SVComp než předchozí?
Beran Vítězslav, doc. Ing., Ph.D. (UPGM FIT VUT), člen
Grézl František, Ing., Ph.D. (UPGM FIT VUT), člen
Janoušek Jan, doc. Ing., Ph.D. (FIT ČVUT), člen
Peringer Petr, Dr. Ing. (UITS FIT VUT), člen
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT), člen
@mastersthesis{FITMT21674,
author = "Matej Maru\v{s}\'{a}k",
type = "Diplomov\'{a} pr\'{a}ce",
title = "Generic Template-Based Synthesis of Program Abstractions",
school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}",
year = 2019,
location = "Brno, CZ",
language = "english",
url = "https://www.fit.vut.cz/study/thesis/21674/"
}