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í, verifikaci a rozhodování logik. Přestože jsou automaty základním konceptem informatiky s širokými aplikacemi a dobře prozkoumanými teoretickými základy, jejich praktické využití a rozšíření zůstává aktivní a náročnou oblastí výzkumu.

Oblast je silně motivována aplikacemi ve verifikaci a testování, vyhledávání regulárních vzorů, umělé inteligenci, SMT-solvingu, návrhu systémů a automatické syntéze. Například nejefektivnější algoritmy pro regulární vyhledávání jsou automatové, avšak jejich zobecnění na zpětné reference, čítače opakování či look-arounds zůstává otevřené. String-solving má význam ve verifikaci programů, zejména v bezpečnostní analýze webových aplikací (SQL injection, XSS), analýze přístupových politik v cloudu či verifikaci kritického software. Výzvou je také efektivní implementace rozhodovacích procedur pro celočíselnou aritmetiku a další logiky. Regulární model checking umožňuje verifikaci systémů s nekonečným stavovým prostorem (např. dynamické datové struktury, komunikační protokoly). Automatové techniky lze využít i pro syntézu programů (např. rozhraní či drivery).

Tyto oblasti otevírají zásadní teoretické otázky rozhodnutelnosti a složitosti. Např.: jak modelovat zpětné reference pomocí automatů? Co je rozhodnutelné o programech manipulujících řetězce či dynamické struktury a za jakou cenu?

Z praktického hlediska jde o efektivní implementaci automatových algoritmů a omezení stavové exploze. Klíčové jsou kompaktní reprezentace (minimalizace, abstrakce, aproximace) a rozšíření jako alternující, symbolické či čítačové automaty. Důležité je porozumět jejich vlastnostem a navrhnout implementace, které obstojí v reálných aplikacích.

Výzkum probíhá ve skupině VeriFIT (L. Holík, prof. Vojnar, dr. Lengál, doc. Rogalewicz, doc. Češka, doktor Smrčka), která dosahuje špičkové mezinárodní úrovně (publikace, nástroje, ocenění, spolupráce např. s Microsoft Research, Academia Sinica, Uppsala University aj.). Spolupracujeme i s průmyslem (Red Hat, Honeywell, Embraer). Absolventi mají výborné uplatnění v akademii i praxi. Skupina je úspěšná v grantové činnosti, což umožňuje nadstandardní finanční podporu doktorandů.