Efektivní práce s konečnymi automaty v automatickém usuzování

Budeme vyvíjet techniky pro práci s konečnými automaty s aplikacemi v automatickém usuzování, ve verifikaci a rozhodování logik.
Obecně, přestože jsou automaty základním a konceptem informatiky s obrovským množstvím aplikací, velmi dobře pochopeným v základní teoretické rovině, techniky jejich použití v praxi a související rozšíření konečných automatů jsou stále velmi bohatým a živým polem výzkumu.

Oblast má silnou praktickou motivaci v oblastech jako verifikace a testování, vyhledávání regulárních vzorů, umělá inteligence a automatické usuzování, rozhodování logik a SMT-solving, návrh a analýza systémů, automatická syntéza systémů.
Například, nejefektivnější algoritmy pro vyhledávání regulárních vzorů jsou založeny na automatech, ale stále není jasné, jak tyto algoritmy zobecnit na zpětné reference, čítače opakování, nebo takzvané look-arounds. Rozhodování logik o řetězcích, string-solving, má aplikace ve verifikaci programů s řetězci, zejména v analýze bezpečnosti webových aplikací (náchylnost na útoky typu SQL-injection, cross-site-scripting), analýze uživatelských politik přítupu ke cloudovým zdrojům, verifikaci kritického avionického software. Otevřeným problémem je efektivní implementace automatových rozhodovacích procedur pro celočíselnou aritmetiku a další logiky. Regulární model-checking je automatová metoda použitelná pro verifikaci široké škály systémů s nekonečným stavovým prostorem, jako jsou programy s dynamickými datovými strukturami nebo komunikační protokoly. Automatovými technikami je možno automaticky syntetizovat programy, například komunikační rozhraní a drivery.

V těchto a dalších oblastech existuje řada hlubokých teoretických otázek o rozhodnutelnosti a složitosti problémů.
Například, jak modelovat zpětné-reference pomocí konečných automatů? Co vše je rozhodnutelné o programech manipulujících řetězce, jako jsou webové aplikace, nebo o programech s dynamickými datovými strukturami? Za jakou cenu?

Praktické otázky se týkají efektivní implementace existujících automatových algoritmů a teoretických poznatků.
Jak zabránit stavové explozi při komplexních manipulacích automatů? Jak je kompaktně reprezentovat, pomocí technik minimalizace, syntaktických rozšíření, abstrakce, aproximace?
Jak efektivně pracovat s kompaktními reprezentacemi automatů, jako jsou alternující automaty, symbolické automaty, automaty s čítači a registry? Jaké jsou teoretické vlastnosti těchto rozšíření? Jak vyvíjené techniky efektivně implementovat, aby opravdu fungovaly na konkrétních praktických problémech?

Tímto a souvisejícím výzkumem se kromě L. Holíka zabývá část skupiny VeriFIT, prof. Vojnar, dr. Lengál, doc. Rogalewicz, doc. Češka. Skupina dosahuje špičkové mezinárodní úrovně, se stovkami publikací na nejprestižňějších fórech, desítkami softwarových nástrojů, řadou meznárodních ocenění, a intenzivní mezinárodní spoluprací s prestižními výzkumnými institucemi (Microsofr research, Redmond; Academia Sinica, Taipei, Uppsala Univerisy, Univerity of Braunschweig, University of Edinburgh, Univeristy of Kaserslautern, University of Paris, Univerité Grenoble Alpes, Chinese Academy of Sciences).
Spolupracujeme s průmyslem (Red Hat, Honeywell). Naši absolventi doktorského studia tak mají příležitosti získat zajímavé a specializované pozice v průmyslu nebo smysluplně pokračovat v akademické sféře.
Skupina je úspěšná v získávání grantů, doktorští studenti tak mohou být nadstandardně finančně ohodnoceni.