Automata@FIT
Informace
Automata@FIT je výzkumná skupina na FIT VUT, zaměřující se na výzkum v okolí konečných automatů a příbuzných formalismů, jejich teorii, fundamentální principy potřebné pro jejich zapojení v aplikacích, a samotné aplikace ve formálním automatickém usuzování, v analýze a verifikaci systémů, v rozhodování logik, v SMT-solvingu, v rozpoznávání regulárních vzorů, v monitorování, detekce anomálií v sítích, syntéza systémů a kontrolerů v nejistém prostředí.
Aktuální výzkum
Současně se skupina věnuje intenzivně zejména
- vývoji technologie string constraint solvingu, založené na konečných automatech, s aplikacemi v analýze systémů manipulujících řetězce, zranitelnosti webových aplikací, v analýze bezpečnostních politik např. cloudových technologií,
- analýze kvantových obvodů pomocí technik založených na stromových automatech
- automatovým procedurám pro rozhodování logik jako jsou celočíselná lineární aritmetika, WS1S, MSO, HyperLTL
- vývoji obecně použitelných technik a nástrojů pro efektivní použití konečných automatů
- vývoji stručných rozšíření konečných automatů a rozhodovacích diagramů a metod pro práci s nimi (např. alternace, registry, čítače, procedury)
- Markovovy modely jako formalismus pro řešení nejistoty a podporu automatizovaného rozhodování
- automaty v monitorování síťového provozu a detekci anomálií
- rozpoznávání regulárních vzorů
Ocenění
- Nominace na nejlepší příspěvek konference ETAPS'24 za práci Z3-Noodler: An Automata-based String Solver autrů Yu-Fang Chen, David Chocholatý, Vojtech Havlena, Lukás Holík, Ondrej Lengál, Juraj Síč
- Nejlepší příspěvek na FM'23 za práci Word Equations in Synergy with Regular Constraints autorů František Blahoudek, Yu-Fang Chen, David Chocholatý, Vojtěch Havlena, Lukás Holík, Ondrej Lengál, Juraj Síč
- Distinguished paper na OOPSLA'23 za práci Solving String Constraints with Lengths by Stabilization autorů Yu-Fang Chen, David Chocholatý, Vojtěch Havlena, Lukáš Holík, Ondřej Lengál, Juraj Síč.
- Distinguished paper na PLDI'23 za práci An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits autorů Yu-Fang Chen, Kai-Min Chung, Ondrej Lengál, Jyun-Ao Lin, Wei-Lun Tsai, Di-De Yen
- Barbora Šmahlíková získala za svůj výzkum ocenění VCLA International Student Awards 2023 a Cenu vlády ČR pro nadané studenty.
Kontakty
Lukáš Holík, holik@fit.vutbr.cz