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

• 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
• 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ů