Ověřování modelů (model checking) je rozšířená technika automatické formální verifikace softwarových a hardwarových systémů. Cílem této techniky je pro daný formální popis systému (konečně stavový model) a požadovanou vlastnost systematicky analyzovat graf všech dosažitelných konfigurací a rozhodnout, zda systém tuto vlastnost splňuje či ne. Proces ověřování modelů typicky trpí tzv. problémem stavové exploze, který způsobuje, že grafy, které je nutno analyzovat, jsou pro skutečné systémy příliš velké. Z tohoto důvodu je efektivita fundamentálních grafových algoritmů (prohledávání do šířky, hledání nejkratších cest, rozklad na silně souvislé komponenty, detekce akceptujících cyklů, atd.), které tvoří základní stavební kameny pro techniky ověřování modelů, velmi důležitá. Nicméně výkonnost sekvenčních implementací těchto algoritmů se ukazuje nedostatečná pro zpracování extrémně velkých grafů. Tato skutečnost mimo jiné vedla k návrhu a implementaci paralelních grafových algoritmů, které jsou schopny efektivně využít výkon paralelních architektur, jako jsou počítačové clustery či více-jádrové procesory. I když je algoritmický přechod k paralelnímu zpracování možný, sekvenční kód musí být vhodně modifikován, aby mohl využít výkon paralelních architektur. To platí zejména pro moderní masivně paralelní grafické výpočetní jednotky (graphics processing units - GPUs). Tyto zařízení obsahují stovky výpočetních jednotek a jsou tak schopny poskytnout zasadní akceleraci mnohých výpočetně náročných vědecko-technických aplikací. Klíčem k efektivnímu využití těchto architektur pro vědecko-technické výpočty je návrh a implementace efektivních datově paralelních algoritmů, které jsou schopny škálovat do stovek úzce propojených výpočetních jednotek. V této tezi se zaměřujeme zejména na datově paralelní algoritmy, které se využívají v procesu ověřování modelů. Nicméně náš přístup je obecnější a lze ho rovněž aplikovat i na jiné grafové algoritmy. V tezi podrobně diskutujeme a popisujeme návrh efektivních datově paralelních algoritmů pro detekci akceptujících cyklů, rozklad na silně souvislé komponenty, detekci optimálních cyklů a grafové řešení soustavy booleovských rovnic. Zejména se zaměřujeme na návrh datově paralelních grafových primitiv a ukazujeme, jak tyto primitiva využít ke konstrukci zmíněných algoritmů. Zatímco hrubá výpočetní síla, kterou mohou moderní masivně paralelní grafické výpočetní jednotky nabídnout, je ohromující, její efektivní využití je často redukováno náročnou přípravou vhodných datových struktur a je limitováno na malé či středně velké instance kvůli omezené paměti, kterou tyto architektury poskytují. Tudíž dále navrhujeme metody, které jsou schopny tyto limity překonat pomocí více-jádrové konstrukce kompaktních datových struktur a využití několika grafických výpočetních jednotek zároveň. Abychom mohli vyhodnotit efektivitu popsaných technik, provedli jsme experimentální ověření výkonnosti navržených datově paralelních algoritmů a provedli jsme jejich srovnaní s nejlepšími sekvečními protějšky. Naše experimenty ukazují, že navržená akcelerace pomoci grafických výpočetních jednotek vede k výraznému zrychlení grafových algoritmů. Navíc experimentální vyhodnocení založené na objektivním výběru použitých instancí ukázalo, že náš nástroj DiVinE-CUDA (využívající grafické výpočetní jednotky pro akceleraci navržených datově paralelních algoritmů pro detekci akceptujících cyklů a více-jádrové architektury pro zrychlení navržené paralelní konstrukce kompaktní reprezentace stavového prostoru) je nejrychlejší mezi současnými nástroji pro LTL ověřování modelů.