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

VeriFIT je skupinou výzkumníků a studentů z FIT VUT, kteří se zaměřují na výzkum v oblasti metod automatizované analýzy a verifikace systémů. Zájem skupiny zahrnuje formální verifikaci (model checking, statická analýza), dynamickou analýzu (tj. analýzu za běhu systému), inteligentní testování i metody automatického opravování systémů. Skupina se zabývá základním výzkumem v uvedených oblastech, ale také vývojem prototypových verifikačních nástrojů a jejich ověřováním na vhodných případových studiích.

[img]

Témata výzkumu

Automatizovaná formální verifikace nekonečně stavových systémů (systémy s dynamickými datovými strukturami, jako jsou různé typy seznamů a stromů -- i v podobě v jaké se užívají např. v jádře Linuxu, 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 jazyků a automatů a také různých typů logik.
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 -- viz www.languageinclusion.org -- apod.).
Automatická verifikace a odhalování chyb v paralelním software s využitím širokého spektra metod (statická a dynamická analýza, inteligentní testování, model checking), včetně možnosti sebe-opravování programů za běhu.

Ocenění

Č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

Seminář

Pracovní seminář skupiny VeriFIT.

Nástrojová podpora

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).

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

Forester -- nástroj pro analýzu programů s dynamickými datovými strukturami využívající stromové automaty.
Predator -- nástroj pro kontrolu správnosti manipulací s dynamickými datovými strukturami využívající separační logiku.
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.

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

SearchBestie -- nástroj pro experimentování s technikami prohledávání prostoru při testování aplikací.
ANaConDA -- prostředí pro dynamickou analýzu paralelních C/C++ programů na binární úrovni
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.

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:

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.

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

Department of Information Technology, Uppsala University
LIAFA, Université Paris 7 -- Denis Diderot/CNRS
VERIMAG, Université Joseph Fourier/INPG/CNRS, Grenoble -- skupina verifikace programů
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 Brně -- viz také doktorský projekt GA ČR Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů a v rámci něj organizovaný workshop MEMICS.

Nacházíte se v sekcích