Efektivní práce s logikami a automaty (nejen) ve formální analýze a verifikaci -- společné vedení s dr. O. Lengálem

Různé typy logik a automatů patří mezi nejzákladnější objekty studované a aplikované v oblasti informatiky již desítky let. Přesto v této oblasti existuje řada dosud neuspokojivě vyřešených problémů a neustále se objevují nové, vzrušující problémy související se stále novými aplikacemi logik a automatů (např. při formální verifikaci konečně i nekonečně stavových systémů s různými pokročilými řídicími či datovými strukturami, v rozhodovacích procedurách, při syntéze programů či hardware nebo i v metodách efektivního vyhledávání v různých typech dat či v síťovém provozu).

Předmětem disertační práce bude primárně rozvoj současného stavu v oblasti efektivní práce s různými logikami (např. nad ukazatelovými strukturami, řetězci, různými aritmetikami, temporálními logikami apod.). Za tím účelem budou zkoumány přístupy založené na různých typech rozhodovacích diagramů, automatů, ale také např. přístupy založené na existenci modelu omezené velikosti či na efektivních redukcích mezi různými typy logických teorií. V souvislosti s tím pak budou rozvíjeny i metody efektivní práce s rozhodovacími diagramy a různými typy automatů (automaty nad slovy, stromy, nekonečnými slovy, automaty s čítači apod.). Práce zahrne jak teoretický výzkum, tak také prototypovou implementaci navržených technik a jejich experimentální vyhodnocení.

Práce bude řešena ve spolupráci s týmem VeriFIT zabývajícím se na FIT VUT rozvojem technik pro práci s logikami a automaty a jejich aplikacemi. Jedná se zejména o dr. O. Lengála, jež bude působit v roli školitele specialisty, nebo také doc. L. Holíka či doc. A. Rogalewicze. 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: Academia Sinica, Tchaj-wan (prof. Y.-F. Chen); TU Vienna, Rakousko (doc. F. Zuleger); LSV, ENS Paris-Saclay (prof. M. Sighireanu); IRIF, Paříž, Francie (prof. A. Bouajjani, doc. P. Habermehl, doc. C. Enea), Verimag, Grenoble, Francie (doc. R. Iosif); Uppsala University, Švédsko (prof. P.A. Abdulla, prof. B. Jonsson); či School of Informatics, University of Edinburgh, Velká Británie (prof. R. Mayr).

V rámci tématu se student může také aktivně zapojit do různých grantových projektů, jako jsou např. projekty GA ČR GA23-07565S "ROULETTE - Reprezentace Booleovských funkcí pomocí adaptabilní datové struktury", GA23-06506S "AIDE - Pokročilá analýza a verifikace pro pokročilý software", ERC.CZ projekt LL1908 "Efektivní konečné automaty pro automatické usuzování" či některý z aktuálně připravovaných Horizon Europe projektů.