Designing Data-Parallel Graph Algorithms for Model Checking - Češka, Milan, 1946- (2012)
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é j