Analýza programů se složitými datovými strukturami

SW projekty, které využívají dynamické datové struktury v kombinaci s ukazateli, jsou velmi náchylné na chyby při práci s pamětí (null pointer dereference, memory leaky, ...). Zároveň jde často o systémový kód používaný v jádrech operačních systémů, sdílených knihovnách, nebo interpreterech vyšších programovacích jazyků.

Cílem této práce je navázat na současné techniky pro analýzu programů s dynamickou pamětí, zejména pak na techniky založené na Separační logice a tzv. bi-abdukci. Práce může být směrována na jazyk C/C++, nebo jiný vhodný programovací jazyk. Práce bude navazovat na práci členů skupiny VeriFIT a práci dr. F. Zulegera z TU Wien.

Alternativním směrováním práce může být navázat na současné techniky pro automatizovanou analýzu složitosti s cílem analýzy otevřeného kódu a/nebo kódu se složitými datovými strukturami. Práce bude navazovat na práci členů skupiny VeriFIT a práci dr. F. Zullegera z TU Wien a dr. M. Sinna z Fachhochschule St. Pölten.

Práce bude řešena ve spolupráci s týmem VeriFIT zabývajícím se na FIT VUT technikami pro verifikace programů se složitými datovými strukturami (zejména dr. L. Holík, prof. T. Vojnar, ing. T. Dacík, ing. V. Šoková). V případě zodpovědného přístupu a kvalitních výsledků je zde možnost zapojení do grantových projektů (včetně mezinárodních). Je zde rovněž možnost úzké spolupráce s různými zahraničními partnery VeriFIT: TU Wien, Rakousko (dr. F. Zulleger); Verimag, Grenoble, Francie (dr. R. Iosif); IRIF, Paříž, Francie (prof. A. Bouajjani, dr. M. Sighireanu).

V rámci tématu se student může také aktivně zapojit do různých grantových projektů řešených v rámci skupiny VeriFIT.