Statická analýza, dynamická analýza a testování počítačových systémů, podpora řízení kvality vývoje software a související témata z oblasti teorie automatů a logik zahrnující mimo jiné:

• Statickou analýzu a verifikaci 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ů.
• Testování a dynamickou analýzu (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 v návrhu hardware s využitím vysoko-úrovňových návrhových jazyků.
• Výzkum efektivních technik pro práci s automaty či logikami -- např. simulační redukce nedetereministických automatů, efektivní testování inkluze nad nedeterministickými automaty, rozhodovací procedury různých logik apod.

• Nástroje Predator (P. Peringer, V. Šoková, T. Vojnar) a 2LS (V. Malík, T. Vojnar; nástroj primárně vyvíjen společností DiffBlue) se zúčastnily mezinárodní soutěže ve verifikaci software SV-COMP'20, kde získaly jednu zlatou a jednu bronzovou medaili. V. Šoková, M. Hruška a T. Vojnar se navíc podíleli na kombinaci nástroje Predator s nástrojem Symbiotic, který je vyvíjen primárně na FI MU a který získal jednu zlatou a dvě stříbrné medaile.
• Článek Chain-Free String Constraints (P.A. Abdulla, M.F. Atig, B.P. Diep, L. Holík, P. Janků) získal cenu za nejlepší článek na konferenci ATVA 2019.
• Článek Automata Terms in a Lazy WSkS Decision Procedure (V. Havlena, L. Holík, O. Lengál, T. Vojnar) získal cenu za nejlepší článek na konferenci CADE-27, 2019.
• Nástroje Predator (M. Kotoun, P. Peringer, V. Šoková, T. Vojnar) a 2LS (V. Malík, T. Vojnar; nástroj primárně vyvíjen společností DiffBlue) se zúčastnily mezinárodní soutěže ve verifikaci software SV-COMP'19, kde získaly jednu stříbrnou medaili a nástroj Predator zvítězil v pod-kategoriích MemSafety-Heap a MemSafety-LinkedLists.
• Článek o nástroji ANaConDA získal na konferenci ISSTA'18 ocenění za nejlepší článek o nástroji.
• Technika navržená ve spolupráci se skupinou ehw@FIT a prezentovaná původně v článku Approximating Complex Arithmetic Circuits with Formal Error Guarantees: 32-bit Multipliers Accomplished (M. Ceska, J. Matyas, V. Mrazek, L. Sekanina, Z. Vasicek, T. Vojnar) získala bronzovou medaili v rámci soutěže 2018 Human-Competitive Awards: "Humies".
• V. Malík a J. Matyáš získali stipendium JCMM Brno PhD talent startující od roku 2017.
• J. Matyáš zvítězil v soutěži IT SPY 2017 se svou diplomovou prací "Využití přibližné ekvivalence při návrhu přibližných obvodů" vedenou M. Češkou jr. a řešenou ve spoluprací skupiny VeriFIT se skupinou ehw@fit.
• Nástroje Predator (M. Kotoun, P. Peringer, V. Šoková, T. Vojnar) a Forester (L. Holík, M. Hruška, O. Lengál, A. Rogalewicz, J. Šimáček, T. Vojnar) se zúčastnily mezinárodní soutěže ve verifikaci software SV-COMP'18, kde získaly jednu stříbrnou medaili a nástroj Predator zvítězil v kategoriích ReachSafety-Heap a MemSafety-Heap. Členové skupiny (V. Malík, Š. Martiček, T. Vojnar) se navíc nově zapojili do soutěže i v rámci týmu spojeného s nástrojem 2LS vyvíjeného primárně společností DiffBlue.
• Nástroje Predator (M. Kotoun, P. Peringer, V. Šoková, T. Vojnar) a Forester (L. Holík, M. Hruška, O. Lengál, A. Rogalewicz, J. Šimáček, T. Vojnar) se zúčastnily mezinárodní soutěže ve verifikaci software SV-COMP'17, kde získaly jednu zlatou medaili.
• Ondřej Lengál získal Cenu Antonína Svobody pro nejlepší disertační práci roku 2015 udělovanou Českou společností pro kybernetiku a informatiku.
• Nástroje Predator (M. Kotoun, P. Peringer, V. Šoková, T. Vojnar) a Forester (L. Holík, M. Hruška, O. Lengál, A. Rogalewicz, J. Šimáček, T. Vojnar) se zúčastnily mezinárodní soutěže ve verifikaci software SV-COMP'16, kde získaly jednu zlatou medaili.
• Nástroje Predator (P. Müller, P. Peringer, T. Vojnar) a Forester (L. Holík, M. Hruška, O. Lengál, A. Rogalewicz, J. Šimáček, T. Vojnar) se zúčastnily mezinárodní soutěževe verifikaci software SV-COMP'15, kde získaly jednu zlatou a jednu stříbrnou medaili.
• Nástroje SPEN (C. Enea, O. Lengál, M. Sighireanu a T. Vojnar) a SLIDE (R. Iosif, A. Rogalewicz a T. Vojnar) získaly jednu zlatou a tři stříbrné medaile na první mezinárodní soutěži rozhodovacích procedur pro separační logiku SL-COMP'14.
• Nástroj Predator získal na FLoC Olympic Games 2014 prestižní medaili Kurta Gödela za jeho úspěchy ve třech za sebou jdoucích ročnících mezinárodní soutěže ve verifikaci software SV-COMP.
• Nástroje Predator (K. Dudka, P. Peringer, T. Vojnar) a CPAlien (P. Müller, T. Vojnar) se zúčastnily mezinárodní soutěže ve verifikaci software SV-COMP'14, kde získaly jednu stříbrnou a jednu bronzovou medaili.
• Článek The Tree Width of Separation Logic with Recursive Definitions (R. Iosif, A. Rogalewicz, J. Šimáček) získal cenu za nejlepší článek na konferenci CADE-24, 2013.
• Článek An Integrated Specification and Verification Technique for Highly Concurrent Data Structures (P.A. Abdulla, F. Haziza, L. Holík, B. Jonsson, A. Rezine) získal cenu EASST Best Software Science Paper udělenou v rámci sdružení konferencí ETAPS'13.
• Nástroj Predator (K. Dudka, P. Müller, P. Peringer, T. Vojnar) zvítězil ve třech kategoriích mezinárodní soutěže SV-COMP'13.
• Článek ANaConDA: A Framework for Analysing Multi-threaded C/C++ Programs on the Binary Level (J. Fiedor, T. Vojnar) získal cenu za nejlepší článek o nástroji na konferenci RV'12.
• Nástroj Predator (K. Dudka, P. Müller, P. Peringer, T. Vojnar) zvítězil v jedné z kategorií mezinárodní soutěže SV-COMP'12.
• Článek When Simulation Meets Antichains. On Checking Language Inclusion of NFAs. (P.A. Abdulla, Y.-F. Chen, L. Holik, R. Mayr, T. Vojnar) získal cenu EATCS Best Theory Paper udělenou v rámci sdružení konferencí ETAPS'10.
• Diplomová práce O. Lengála (Efektivní knihovna pro práci s konečnými stromovými automaty) zvítězila v 5. ročníku soutěže Diplomová práce roku, 2010.
• Článek Composed Bisimulation for Tree Automata (P.A. Abdulla, A. Bouajjani, L. Holik, L. Kaati, T. Vojnar) získal cenu za nejlepší článek na konferenci CIAA'08.
• Diplomová práce Z. Letka (Dynamická detekce a léčení časově závislých chyb nad daty v prostředí Java) získala 1. místo ve studentské soutěži AFCEA 2008.

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žist nad analyzátory jako Facebook Infer či Frama-C.

Verifikace práce s dynamickými datovými strukturami založenými na ukazetelích v programech v jazyce C:

• Predator -- nástroj pro kontrolu správnosti manipulací s dynamickými datovými strukturami typu seznam využívající symbolické paměťové grafy.
• 2LS -- nástroj primárně vyvíjen DiffBlue, ale skupina VeriFIT se účastní jeho doplnění o různé analýzy (mimo ukazatele např. i detekce možných nekončících běhů programů).
• Forester -- nástroj pro analýzu programů s dynamickými datovými strukturami využívající stromové automaty.
• CPAlien -- nástroj pro kontrolu správnosti manipulací s dynamickými datovými strukturami využívající symbolické paměťové grafy v kontextu konfigurovatelné analýzy programů.
• Code-listener -- infrastruktura pro budování statických analyzátorů nad překladačem GCC.
• ARTMC -- nástroj využívající stromové automaty pro verifikaci programů se složitými dynamickými datovými strukturami provázanými ukazateli.

Analýza výkonnosti:

• Perun -- nástroj pro dynamickou analýzu výkonnosti programů a automatickou detekci degradace výkonu mezi verzemi programů uložených v repositářích.
• Ranger -- nástroj pro statickou analýzu složitosti běhu programů s dynamickými datovými strukturami, založený na nástrojích Forester a Loopus.

Rozhodovací procedury:

• Sloth a Trau -- rozhodovací procedury pro formule nad řetězci.
• Gaston -- rozhodovací procedura pro logiku WS1S založená na on-the-fly prohledávání stavového prostoru (rozšíření prototypu dWiNA).
• dWiNA -- rozhodovací procedura pro logiku WS1S založená na nedeterministických automatech jako alternativa ke známému. nástroji MONA, který je založen na automatech deterministických.
• SPEN -- rozhodovací procedura pro fragment separační logiky s induktivními predikáty nad seznamy kombinující grafový homorfismus, SAT solving a členství v jazyce stromových automatů.
• SLIDE -- rozhodovací procedura pro fragment separační logiky s komplexními induktivními predikáty založená na redukci na inkluzi jazyků stromových automatů.

Verifikace (paralelních) Java a C/C++ programů:

• ANaConDA -- prostředí pro dynamickou analýzu paralelních C/C++ programů na binární úrovni.
• SearchBestie -- nástroj pro experimentování s technikami prohledávání prostoru při testování aplikací.
• DA-BMC -- sada nástrojů pro dynamickou analýzu paralelních Java programů, zaznamenání podezřelých běhů a jejich následné přehrání a další ověření v model checkeru JPF (dříve RecRev).
• Java Race Detector and Healer -- nástroj pro detekci časově závislých chyb v paralelních Java programech a pro automatickou opravu těchto chyb, obojí za běhu sledovaných programů.
• MUSE -- nástroj pro model checking využívající symbolickou exekuci.

Kolekce případových studií používaných v našich experimentech s testováním a dynamickou analýzou paralelních programů je dostupná ZDE.

Nástroje pro práci s nedeterministickými automaty nad slovy a stromy:

• libVATA -- knihovna pro efektivní práci s explicitně i semi-symbolicky zakódovanými nedeterministickými stromovými automaty (starší verze jedné části této knihovny byla dříve dostupná jako libSFTA).
• SA -- nástroj pro výpočet simulací nad přechodovými systémy s návěštími (Labelled Transition Systems) a stromovými automaty (Tree Automata).

Verifikace hardware:

• Hades -- nástroj pro detekci různých typů hazardů v mikroprocesorech s jednou zřetězenou linkou kombinující řadu různých formálních metod (analýza toku dat, SAT solving, parametrický model checking).
• CDCreloaded -- nástroj pro formální verifikaci asynchronních obvodů s více hodinovými signály.
• VHDL2CA -- nástroj pro překlad parametrizovaných VHDL komponent do čítačových automatů, na nichž je následně možné provést verifikaci pro všechny možné hodnoty parametrů pomocí existujících nástrojů pro verifikaci čítačových automatů.

Verifikace systémů pracujících v reálném čase:

• Zetav & Verif -- nástroje pro verifikaci systémů specifikovaných pomocí RT-logiky nebo Modechart formalismu.

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 např. 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.