CUDA Accelerated LTL Model Checking

Logo poskytovatele
Logo poskytovatele
Logo poskytovatele

Varování

Publikace nespadá pod Fakultu sportovních studií, 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:

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

Další info