DiVinE-CUDA - A Tool for GPU Accelerated LTL Model Checking

Logo poskytovatele
Logo poskytovatele

Varování

Publikace nespadá pod Pedagogickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Název česky DiVinE-CUDA - Nástroj pro GPU akcelerované ověřování modelu LTL
Autoři

BARNAT Jiří BRIM Luboš ČEŠKA Milan

Rok publikování 2009
Druh Článek v odborném periodiku
Časopis / Zdroj Electronic Proceedings in Theoretical Computer Science
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www http://dx.doi.org/10.4204/EPTCS.14.8
Obor Informatika
Klíčová slova LTL; Model Checking; CUDA
Popis V tomto čláku prezentujeme nástroj, který provádí CUDA akcelerované ověřování modelu logiky LTL. Nástroj staví na paralelním algoritmu MAP upraveném pro platformu NVIDIA CUDA. Demonstrujeme, že verifikace je s použitím nástroje výrazně rychlejší než bez použití dané architektury. V článku identifikujeme některé problémy, které s realizací nástroje souvisí a diskutujeme, jak je možné tyto problémy řešit v budoucnosti.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.