Laboratoř AVELAB
Kontakty prof. RNDr. Jan Strejček, Ph.D. , prof. Ing. Tomáš Vojnar, Ph.D.
AVELAB je výzkumná skupina, která v roce 2025 vznikla sloučením části laboratoře Formela s bývalými laboratořemi ParaDiSe a QualiFI. Primárně se zaměřujeme na automatizovanou analýzu programů. Také se zabýváme souvisejícími tématy jako automatizované usuzování, konečné automaty, programovací jazyky, kompilátory a vývojová a běhová prostředí. Tato témata v laboratoři zkoumáme v celé jejich šíři, od teorie po vývoj nástrojů a jejich průmyslových použití ve společnostech jako RedHat, Honeywell, Oracle Labs nebo NextSilicon.
Témata výzkumu
V laboratoři AVELAB řešíme primárně následující výzkumná témata.
Analýza programů- Statická a dynamická analýza programů a verifikace software od nízkoúrovňových programů jako jádro systému Linux až po analýzu vysokoúrovňových specifikací v kritických oblastech jako letectví.
- Formální verifikace a automatizované generování testů. Symbolická exekuce, abstraktní interpretace, ověřování modelu, slicing programů, fuzzing a podobně.
- Analýza a verifikace jak funkčních požadavků (paměťová bezpečnost nebo korektnost paralelních programů), tak požadavků nefunkčních (jako například analýza výkonu).
- Generování a validace svědků korektnosti a nekorektnosti programů.
- Ověřování ekvivalence pro kontroluju, jestli optimalizace a refaktoring nemění chování programu.
- Satisfiability modulo theories (SMT) a rozhodovací procedury pro řadu logik, které jsou relevantní pro analýzu a verifikaci programů (například separační logika nebo teorie bit-vektorů).
- Answer set programming, logické programování, produkční systémy (například CLIPS/LEAPS).
- Vysokoúrovňové jazyky pro embedded řídicí systémy: od Embedded JavaScriptu po expertní systémy jako CLIPS/LEAPS.
- Metody pro statickou analýzu používané v kompilátorech jak pro vysokoúrovňové, tak pro nízkoúrovňové jazyky.
- Vývojová prostředí a nástroje pro embedded systémy a robotiku.
- Front-end, vizualizace a integrace nástrojů pro analýzu a verifikaci software.
- Teorie konečných automatů a návrh souvisejících algoritmů a nástrojů, zejména s důrazem na jejich aplikace ve verifikaci.
- Algoritmy pro práci s binárními rozhodovacími diagramy (BDD) a jejich efektivní využití.
Vyvíjené nástroje
Výzkumníci z laboratoře AVELAB jsou zapojeni do vývoje řady špičkových a oceňovaných nástrojů pro analýzu a verifikaci systémů.
- Astral — rozhodovací procedura pro separační logiku (spolupráce s VeriFIT).
- Broom — statická analýza bezpečné práce s pamětí v nízkoúrovňovém kódu (spolupráce s VeriFIT a TU Wien).
- DiffKemp — ověřování ekvivalence nízkoúrovňového kódu (spolupráce s Red Hat a VeriFIT).
- Fizzer — gray-box fuzzer pro programy v jazyce C.
- LTL3BA — převod formulí lineární temporální logiky (LTL) na zobecněné transition-based Büchiho automaty.
- LTL3TELA — převod formulí lineární temporální logiky (LTL) na Emerson-Lei automaty.
- Perun — sada nástrojů pro analýzu výkonu programů (spolupráce s Red Hat a VeriFIT).
- Q3B — SMT solver pro kvantifikované formule nad teorií bit-vektorů.
- RacerF — detekce race-conditions v nízkoúrovňovém kódu (spolupráce s VeriFIT).
- Seminator — převod automatů do semi-deterministického tvaru a komplementace nedeterministických automatů nad nekonečnými slovy.
- Symbiotic — framework pro analýzu a verifikaci programů v jazyce C.
- Witch — validátor svědků nekorektnosti pro programy v jazyce C.
Spolupráce
Úzce spolupracujeme s řadou průmyslových partnerů a s výzkumníky z dalších akademických organizací.
Průmyslové spolupráce- Honeywell
- NextSilicon
- Oracle Labs
- Red Hat
- CEA List Paris
- Fondazione Bruno Kessler
- LRE, Epita
- LSV, ENS Paris Saclay
- SoSy-Lab, LMU Munich
- TU Wien
- VeriFIT, FIT VUT