CUDA Accelerated LTL Model Checking

• Název česky: CUDA akcelerované LTL ověřování modelů
• Autoři: BARNAT Jiří; BRIM Luboš; ČEŠKA Milan; LAMR Tomáš
• Rok publikování: 2009
• Druh: Článek ve sborníku
• Konference: Proceedings of the 15th International Conference on Parallel and Distributed Systems
• Fakulta / Pracoviště MU: Fakulta informatiky
• Obor: Informatika
• Klíčová slova: Model Checking; Linear Temporal Logic; CUDA
• Popis: Současný technologický vývoj zpřístupnil různé mnohajádrové architektury. Například SIMD architektury se staly snadno dostupné pro mnoho uživatelů, kteří mají počítače vybavené moderními NVIDIA GPU kartami s CUDA technologií. V tomto článku jsme modifikovali algoritmus maximálního akceptujícího předchůdce [7] používaného pro LTL ověřování modelů pomocí násobení matice vektorem. Tato modifikace umožnila akceleraci LTL ověřování modelů na mnohajádrových GPU architekturách. Naše experimenty demonstrovaly, že použití NVIDIA CUDA technologie vedlo k výraznému zrychlení verifikačního procesu.

Související projekty

• Techniky automatické verifikace a validace softwarových a hardwarových systémů
• Vysoce paralelní a distribuované výpočetní systémy
• Verifikace a analýza velmi velkých počítačových systémů
• 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ů