DiVinE-CUDA - A Tool for GPU Accelerated LTL Model Checking
| BARNAT, Jiří, Luboš BRIM and Milan ČEŠKA. DiVinE-CUDA - A Tool for GPU Accelerated LTL Model Checking. Electronic Proceedings in Theoretical Computer Science. 2009, vol. 14, Prosinec, p. 107--111. ISSN 2075-2180. |
|
Other formats:
BibTeX
LaTeX
RIS
|
| Basic information | |
|---|---|
| Original name | DiVinE-CUDA - A Tool for GPU Accelerated LTL Model Checking |
| Name in Czech | DiVinE-CUDA - Nástroj pro GPU akcelerované ověřování modelu LTL |
| Authors | BARNAT, Jiří (203 Czech Republic, guarantor, belonging to the institution), Luboš BRIM (203 Czech Republic, belonging to the institution) and Milan ČEŠKA (203 Czech Republic, belonging to the institution). |
| Edition | Electronic Proceedings in Theoretical Computer Science, 2009, 2075-2180. |
| Other information | |
|---|---|
| Original language | English |
| Type of outcome | Article in a journal |
| Field of Study | 10201 Computer sciences, information science, bioinformatics |
| Country of publisher | Netherlands |
| Confidentiality degree | is not subject to a state or trade secret |
| WWW | URL |
| RIV identification code | RIV/00216224:14330/09:00028691 |
| Organization unit | Faculty of Informatics |
| Keywords (in Czech) | LTL; Ověřování modelu; CUDA |
| Keywords in English | LTL; Model Checking; CUDA |
| Tags | International impact, Reviewed |
| Changed by | Changed by: prof. RNDr. Luboš Brim, CSc., učo 197. Changed: 17/12/2010 11:19. |
| Abstract |
|---|
| In this paper we present a tool that performs CUDA accelerated LTL Model Checking. The tool exploits parallel algorithm MAP adjusted to the NVIDIA CUDA architecture in order to efficiently detect the presence of accepting cycles in a directed graph. Accepting cycle detection is the core algorithmic procedure in automata-based LTL Model Checking. We demonstrate that the tool outperforms non-accelerated version of the algorithm and we discuss where the limits of the tool are and what we intend to do in the future to avoid them. |
| Abstract (in Czech) |
|---|
| V tomto čláku prezentujeme nástroj, který provádí CUDA akcelerované ověřování modelu logiky LTL. Nástroj staví na paralelním algoritmu MAP upraveném pro platformu NVIDIA CUDA. Demonstrujeme, že verifikace je s použitím nástroje výrazně rychlejší než bez použití dané architektury. V článku identifikujeme některé problémy, které s realizací nástroje souvisí a diskutujeme, jak je možné tyto problémy řešit v budoucnosti. |
| Links | |
|---|---|
| GD102/09/H042, research and development project | Name: 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ů |
| Investor: Czech Science Foundation | |
| GP201/09/P497, research and development project | Name: Automatizovaná formální verifikace s využitím soudobého hardware |
| Investor: Czech Science Foundation, Automated formal verification using modern hardware | |
| MSM0021622419, plan (intention) | Name: Vysoce paralelní a distribuované výpočetní systémy |
| Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems | |
| 1ET408050503, research and development project | Name: Techniky automatické verifikace a validace softwarových a hardwarových systémů |
| Investor: Academy of Sciences of the Czech Republic, Techniques for automatic verification and validation of software nad hardware systems | |
PrintDisplayed: 30/5/2024 05:20