Informace o projektu

Rozšíření nástroje DIVINE pro verifikaci vstupně-výstupně otevřených programů

Kód projektu MUNI/33/15/2015 CEP CORDIS MU WEB INET MU
Doba řešení 01.12.2015–30.11.2016
Stav ukončený
Investor Masarykova univerzita
Program Program děkana FI
Řešitel za FI
Členové realizačního týmu za FI

Anotace

DIVINE je open-source nástroj pro ověřování LTL vlastností vstupně-výstupně uzavřených počítačových programů v C a C++. K efektivní verifikaci využívá výhod soudobého hardware a sofistikovaných redukčních technik.
SymDIVINE je open-source nástroj pro ověřování LTL vlastností vstupně-výstupně otevřených počítačových programů v C a C++.
Cílem projektu je implementace cache pro dotazy na SMT solver v nástroji SymDIVINE za účelem jeho zefektivnění a integrace nástrojů SymDIVINE do DIVINE.

Zpět na seznam investorů