Výzkumná skupina automatizované analýzy a verifikace - VeriFIT

VeriFIT je skupinou výzkumníku a studentu z FIT VUT, kterí se zamerují na výzkum v oblasti metod automatizované analýzy a verifikace systému. Zájem skupiny zahrnuje formální verifikaci (model checking, statická analýza), dynamickou analýzu (tj. analýzu za behu systému), inteligentní testování i metody automatického opravování systému. Skupina se zabývá základním výzkumem v uvedených oblastech, ale také vývojem prototypových verifikacních nástroju a jejich overováním na vhodných prípadových studiích.

[img]

Témata výzkumu

Automatizovaná formální verifikace nekonecne stavových systému (systémy s dynamickými datovými strukturami, jako jsou ruzné typy seznamu a stromu -- i v podobe v jaké se uzívají napr. v jádre Linuxu, neomezenými celocíselnými promennými, poli, parametry, rekurzí, neomezenými komunikacními kanály apod.), a to zejména s vyuzitím teorie jazyku a automatu a také ruzných typu logik.
Výzkum efektivních technik pro práci s automaty ci logikami (napr. simulacní redukce nedetereministických automatu, efektivní testování inkluze nad nedeterministickými automaty -- viz www.languageinclusion.org -- apod.).
Automatická verifikace a odhalování chyb v paralelním software s vyuzitím sirokého spektra metod (statická a dynamická analýza, inteligentní testování, model checking), vcetne moznosti sebe-opravování programu za behu.

Ocenení

Clá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 udelenou v rámci sdruzení konferencí ETAPS'13.
Nástroj Predator (K. Dudka, P. Müller, P. Peringer, T. Vojnar) zvítezil ve trech kategoriích mezinárodní souteze SV-COMP'13.
Clánek ANaConDA: A Framework for Analysing Multi-threaded C/C++ Programs on the Binary Level (J. Fiedor, T. Vojnar) získal cenu za nejlepsí clánek o nástroji na konferenci RV'12.
Nástroj Predator (K. Dudka, P. Müller, P. Peringer, T. Vojnar) zvítezil v jedné z kategorií mezinárodní souteze SV-COMP'12.
Clá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 udelenou v rámci sdruzení konferencí ETAPS'10.
Diplomová práce O. Lengála (Efektivní knihovna pro práci s konecnými stromovými automaty) zvítezila v 5. rocníku souteze Diplomová práce roku, 2010.
Clánek Composed Bisimulation for Tree Automata (P.A. Abdulla, A. Bouajjani, L. Holik, L. Kaati, T. Vojnar) získal cenu za nejlepsí clánek na konferenci CIAA'08.
Diplomová práce Z. Letka (Dynamická detekce a lécení casove závislých chyb nad daty v prostredí Java) získala 1. místo ve studentské soutezi AFCEA 2008

Seminár

Pracovní seminár skupiny VeriFIT.

Nástrojová podpora

Vetsina výsledku, publikovaných v nasich cláncích, zahrnuje experimentální overení na prototypové implementaci. Zde jsou nekteré z nástroju, které jsme vyvinuli (ostatní poskytneme zájemcum na základe jejich dotazu emailem).

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

Forester -- nástroj pro analýzu programu s dynamickými datovými strukturami vyuzívající stromové automaty.
Predator -- nástroj pro kontrolu správnosti manipulací s dynamickými datovými strukturami vyuzívající separacní logiku.
Code-listener -- infrastruktura pro budování statických analyzátoru nad prekladacem GCC.
ARTMC -- nástroj vyuzívající stromové automaty pro verifikaci programu se slozitými dynamickými datovými strukturami provázanými ukazateli.

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

SearchBestie -- nástroj pro experimentování s technikami prohledávání prostoru pri testování aplikací.
ANaConDA -- prostredí pro dynamickou analýzu paralelních C/C++ programu na binární úrovni
DA-BMC -- sada nástroju pro dynamickou analýzu paralelních Java programu, zaznamenání podezrelých behu a jejich následné prehrání a dalsí overení v model checkeru JPF (dríve RecRev).
Java Race Detector and Healer -- nástroj pro detekci casove závislých chyb v paralelních Java programech a pro automatickou opravu techto chyb, obojí za behu sledovaných programu.
MUSE -- nástroj pro model checking vyuzívající symbolickou exekuci.

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

libVATA -- knihovna pro efektivní práci s explicitne i semi-symbolicky zakódovanými nedeterministickými stromovými automaty (starsí verze jedné cásti této knihovny byla dríve dostupná jako libSFTA).
SA -- nástroj pro výpocet simulací nad prechodovými systémy s návestími (Labelled Transition Systems) a stromovými automaty (Tree Automata).

Verifikace hardware:

CDCreloaded -- nástroj pro formální verifikaci asynchronních obvodu s více hodinovými signály.
VHDL2CA -- nástroj pro preklad parametrizovaných VHDL komponent do cítacových automatu, na nichz je následne mozné provést verifikaci pro vsechny mozné hodnoty parametru pomocí existujících nástroju pro verifikaci cítacových automatu.

Verifikace systému pracujících v reálném case:

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

Spolupráce

Nase skupina spolupracuje s radou jiných týmu v CR i v zahranicí, zvláste aktivní je momentálne nase spolupráce napr. s:

Department of Information Technology, Uppsala University
LIAFA, Université Paris 7 -- Denis Diderot/CNRS
VERIMAG, Université Joseph Fourier/INPG/CNRS, Grenoble -- skupina verifikace programu
IIS, Academia Sinica, Taiwan
Software Systems Lab, University of Passau, Germany
LFCS, University of Edinburgh
LTA, DISCo, University Milano Bicocca
IBM Haifa Research Laboratories
Fakulta informatiky, Masarykova universita v Brne -- viz také doktorský projekt GA CR Matematické a inzenýrské metody pro vývoj spolehlivých a bezpecných paralelních a distribuovaných pocítacových systému a v rámci nej organizovaný workshop MEMICS.

Nacházíte se v sekcích