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

Varování

Publikace nespadá pod Filozofickou 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:	Techniky automatické verifikace a validace softwarových a hardwarových systémů Vysoce paralelní a distribuované výpočetní systémy Automatizovaná formální verifikace s využitím soudobého hardware 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ů