OBLASTI VÝZKUMU
- Statická analýza a verifikace. na formálních základech v oblasti systémů s nekonečnými stavovými prostory (programy s ukazateli a dynamickými datovými strukturami, paralelní programy s neomezeným počtem vláken, neomezenými celočíselnými proměnnými, poli, parametry, rekurzí, neomezenými komunikačními kanály apod.), a to zejména s využitím teorie automatů, logik a grafů.
- Konečné automaty a logiky. Algoritmy pro efektivní práci s konečnými automaty, s aplikacemi v rozpoznávání a učení se regulárních vzorů, v analýze síťového provozu, verifikaci a analýze programů a systémů obecně, rozhodování logik jako Presburgerova aritmetika, WSkS, nebo jazyky řetězcových omezení.
- Řetězcová omezení. Analýza systémů manipulujících proměnné typu řetězec. Řetězcová omezení leží v jádru verifikace programů manipulujících řetězce, jako jsou zejména webové aplikace, kde je třeba analyzovat zranitelnost útoky typu SQL-injection a cross-site scripting.
- Testování a dynamická analýza (zejména paralelního) software s využitím širokého spektra metod (vkládání šumu, extrapolace, dolování z dat, strojové učení), včetně možnosti sebe-opravování programů za běhu resp. poskytování informací pro řízení kvality vývoje software.
- Formální verifikaci hardware s využitím vysoko-úrovňových návrhových jazyků.
- Automatická analýza a design komplexních systémů
VE VERIFITU DÁVÁME PROSTOR NADANÝM STUDENTŮM
NÁSTROJE
Většina výsledků, publikovaných v našich článcích, zahrnuje experimentální ověření na prototypové implementaci. Zde jsou některé z nástrojů, které jsme vyvinuli (ostatní poskytneme zájemcům na základě jejich dotazu emailem).
Pluginy pro analýzu různých vlastností v rámci různých statických analyzátorů (primárně pro jazyky C/C++). Jedná se o analýzu vybraných vlastností jako uváznutí, atomicita sekvencí volání či výpočetní složitost nad analyzátory jako Facebook Infer či Frama-C.
SPOLUPRÁCE
Naše skupina spolupracuje s řadou jiných týmů v ČR i v zahraničí, zvláště aktivní je momentálně naše spolupráce s:
- Department of Information Technology, Uppsala University, Švédsko,
- Microsoft Research Redmond, USA,
- IIS, Academia Sinica, Tchaj-wan,
- Department of Computer Science, Oxford University, Velká Británie,
- Software Modeling and Verification Group, RWTH Aachen, Německo,
- Institute of Theoretical Computer Science, TU Braunschweig, Německo,
- VERIMAG, University Grenoble Alpes/CNRS, Grenoble, Francie,
- FORSYTE, Faculty of Informatics, TU Vienna, Vídeň, Rakousko,
- Chair for Foundations of Software Reliability and Theoretical Computer Science, TU Munich, Německo,
- Automatic Reasoning, Faculty of Informatics, TU Keiserslautern, Německo,
- IRIF, University Paris Diderot/CNRS, Paříž, Francie,
- School of Informatics, University of Edinburgh, Velká Británie,
- D3S, MFF UK, Praha,
- Fakulta informatiky, Masarykova universita, Brno,
- Red Hat Lab, laboratoř firmy Red Hat Czech na FIT VUT,
- Honeywell Aerospace a International, Brno,
- DiffBlue, Oxford, Velká Británie,
- Konsorcium evropského H2020 ECSEL projektu Arrowhead Tools,
- Konsorcium evropského H2020 ECSEL projektu Aquas.
PROJEKTY
PUBLIKACE
OCENĚNÍ
