VeriFIT: úspěšná výzkumná skupina. Nejen na konferenci Computer Aided Verification

Mimořádný publikační výsledek si připsala fakultní výzkumná skupina VeriFIT, zaměřující se na automatizovanou analýzu a verifikaci. Na jedné z nejprestižnějších (CORE A*, acceptance rate 25 %) světových konferencí z oblasti formálních metod a verifikace Computer Aided Verification (CAV) byla přijata hned pětice článků, na nichž mají členové skupiny zásadní podíl. A to je velmi neobvyklá koncentrace. FIT VUT se tak v rámci letošního ročníku CAVu řadí mezi nejúspěšnější světové instituce. Hned čtyři z autorů mají podporu mezinárodního projektu VASSAL, koordinovaného právě fakultou. O světovém přesahu VeriFITu svědčí i to, že tři přední výzkumníci skupiny – Milan Češka, Lukáš Holík a Ondřej Lengál – jsou členy programového výboru této konference.

Spolehlivost agentních systémů

VeriFIT se coby výzkumná skupina nejobecněji řečeno věnuje výzkumu v oblasti metod automatizované analýzy a verifikace systémů, které slouží k zajištění spolehlivosti a vysvětlitelnosti běhu výpočetních operací a celých systémů. Současně je diferencovaným uskupením, v jehož rámci lze vysledovat hned několik podskupin s vlastními výzkumnými tématy. Pojďme si je blíže představit.

První podskupinu vede docent Milan Češka, který spolupracuje aktuálně se třemi doktorandy (Roman Andriushchenko, Filip Macák a David Hudák) a řadou studentů. Češka a jeho spolupracovníci se soustředí na vývoj metod, které umožňují automatizovaný návrh spolehlivých agentních systémů. Zabývají se metodami, které dovolují kvantifikovat, s jakou pravděpodobností výsledný systém splňuje požadované chování. Tento přístup je klíčový pro systémy, které pracují v prostředí s nejistotou, jako jsou autonomní řídicí systémy, robotika či rozhodovací systémy pro ekonomické či zdravotnické aplikace.

„Představme si autonomní auto, které se blíží ke křižovatce, kde na přechodu stojí dítě. Ačkoliv má auto zelenou, je nutné počítat s možností, že dítě vejde na červenou, a tudíž je třeba vhodně reagovat – plynule projet křižovatku a zajistit, že se kolize s dítětem stane velmi nepravděpodobnou, i když dítě do křižovatky vejde,“ popisuje co nejpřístupněji možné pole nasazení podobných systémů Češka.

Mezi pěticí článků přijatých na CAV jsou dva, na nich se autorsky podílel Milan Češka a jeho kolegové:

• Linus Heck, Filip Macák, Roman Andriushchenko, Milan Češka, Sebastian Junges. Shields to Guarantee Probabilistic Safety in MDPs.
• Milan Češka, Sebastian Junges, Luko van der Maas, Filip Macák, Tim Quatmann. Fast Computation of Conditional Probabilities in MDPs and Markov Chain Families.

Automaty

Druhým proudem v rámci výzkumné skupiny VeriFIT je skupina kolem docenta Lukáše Holíka s označením Automata@FIT. Její výzkum stojí na pomezí informatiky, logiky a matematiky: Skupina rozvíjí teoretické metody založené na automatech, tedy konečných popisech často nekonečných množin možností – například všech slov, vstupů, výpočtů nebo stavů programu. Díky tomu lze automaticky uvažovat o tom, do jakých stavů se program může dostat, zda program splňuje požadované vlastnosti nebo kde leží hranice toho, co je ještě možné výpočetně ověřit. Formální metody pomáhají odhalovat chyby a bezpečnostní slabiny tam, kde běžné testování nemůže poskytnout dostatečnou jistotu. Jedním z výrazných témat skupiny je string constraint solving, tedy automatické uvažování o řetězcích (datový typ string), které se objevují například ve webových aplikacích, databázových dotazech nebo přístupových politikách v cloudu. Takové metody mohou pomoci ověřit, že se do programu nedostane vstup, který by způsobil chybu či bezpečnostní incident. K tomuto tématu se váže další z publikací přijatých na CAV:

• David Chocholatý, Vojtěch Havlena Juraj Síč, Lukáš Holík, Michal Šedý. String Solving with Stabilization and Transducers.

Dalším automatovým problémem studovaným ve VeriFITu jsou efektivní metody práce s automaty nad nekonečnými slovy. Tyto automaty často slouží k modelování reaktivních systémů, jako jsou např. komponenty operačního systému nebo hardware počítače, jejichž korektní funkčnost bývá kritická. Výzkum pod vedením docenta Ondřeje Lengála se zaměřuje na to, jak s těmito automaty efektivně pracovat, což má použití např. při verifikaci výše zmíněných kritických systémů.

• O. Alexaj, V. Havlena, L. Holík, O. Lengál, Y. Li, N. Mazzocchi. Kofola 1.0: A Modular Approach to 𝝎-Regular Complementation and Inclusion Checking.

Verifikace kvantových obvodů

Třetí podskupina VeriFITu se formuje kolem docenta Ondřeje Lengála. Zaměřuje se na průnik formálních metod, automatů a kvantových technologií, tedy na oblast, která se na fakultě začala výrazněji rozvíjet v posledních letech. Lengál se věnuje především verifikaci a simulaci kvantových programů. Ve spolupráci s vědci z Tchaj-wanu pracuje na metodách a nástrojích, které mají podporovat návrh kvantových programů a pomáhat ověřovat, že kvantové programy skutečně dělají to, co od nich očekáváme. Tématu se týká poslední z přijatých článků na CAVu:

• W. Tsai, Y. Chen, O. Lengál. A Practical Specification Language for Automatic Quantum Program Verification.

VeriFIT patří k tahounům odborného výzkumu na Fakultě informačních technologií a má svůj výrazný podíl na tom, že fakulta patří mezi špičkové vysokoškolské výzkumné organizace České republiky. Jejím členům děkujeme a přejeme spoustu vytrvalosti a další úspěchy v nejbližší době.

Zdroj: FIT VUT

Témata

Související články:
Chytrý autopilot? V začátku vývoje na FIT to bylo něco výjimečného
Poznají, kdo na nahrávkách mluví. Jejich aplikace pořizují tajné služby i úvěrové společnosti
Z Baskicka do Brna. Mireia Diez Sánchez na VUT učí počítače rozumět lidské řeči
České algoritmy z FIT VUT pomáhají Finům digitalizovat dřevařský průmysl
Na tištěné violoncello hraje koncertní mistr filharmonie i hokejista