Téma disertační práce

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

Ak. rok 2025/2026

Školitel: Vojnar Tomáš, prof. Ing., Ph.D.

Školitel specialista: Lengál Ondřej, Ing., Ph.D.

Ústav: Ústav inteligentních systémů

Programy:
Informační technologie (DIT) - prezenční studium
Informační technologie (DIT) - kombinované studium

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, ve verifikaci kvantových programů 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. Po dokončení habilitačního řízení dr. Lengála se předpokládá jeho přechod do role hlavního školitele, přičemž T. Vojnar může nadále zůstat v roli školitele specialisty. 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",  nově přijatý projekt GA ČR 25-18318S "QUAK: Quantum Program Analysis using Automata Toolkit", or the Horizon Europe project SEP-210979090 "VASSAL: Verification and Analysis for Safety and Security of Applications in Life".

Nahoru