Automatizovaná analýza složitosti programů (nejen) se složitými datovými strukturami

U softwarových systémů očekáváme, že jednak nikdy nenastane žádná závažná chyba (deadlock, neoprávněný přístup do paměti, ...), ale také každá akce systému vždy úspěšně skončí v rozumném časovém intervalu. Problémem ověření ukončení v rozumném čase se zabývá analýza mezí (bound analysis). Problémem analýzy mezí je pro zadaný program (nebo funkci) nalézt (horní) odhad složitosti. Přes pokrok v posledních letech ale stále nejsou současné techniky dostatečné. Problémem jsou hlavně složité datové struktury a tzv. otevřený kód, kde analyzujeme pouze části kódu bez znalosti kontextu.

Cílem této práce je navázat na současné techniky pro analýzu mezí s cílem analýzy mezí 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); Uppsala University, Švédsko (prof. P.A. Abdulla, prof. B. Jonsson, dr. Rummer); Verimag, Grenoble, Francie (dr. R. Iosif); IRIF, Paříž, Francie (prof. A. Bouajjani, dr. M. Sighireanu, dr. C. Enea); Academia Sinica, Tchaj-wan (prof. Y.-F. Chen).

V rámci tématu se student může také aktivně zapojit do různých grantových projektů, jako je např. projekt AIDE - Pokročilá analýza a verifikace pro pokročilý software, GAČR.