CUDA 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	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
Citace
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ů