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:

Verifikace práce s dynamickými datovými strukturami založenými na ukazatelí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, Trau, Norn, Z3-Trau - rozhodovací procedury pro logiky nad řetězci s aplikací s verifikací programů manipulujících s ř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).
• Rabbit and Reduce - nástroje pro testovaní inkluze jazyků a pro redukci velikosti Büchiho automatů.

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.