CUDA Accelerated LTL Model Checking
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F09%3A00028692" target="_blank" >RIV/00216224:14330/09:00028692 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
CUDA Accelerated LTL Model Checking
Original language description
Recent technological developments made available various many-core hardware platforms. For example, a SIMD-like hardware architecture became easily accessible for many users who have their computers equipped with modern NVIDIA GPU cards with CUDA technology. In this paper we redesign the maximal accepting predecessors algorithm [7] for LTL model checking in terms of matrix-vector product in order to accelerate LTL model checking on many-core GPU platforms. Our experiments demonstrate that using the NVIDIA CUDA technology results in a significant speedup of verification process.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
Result was created during the realization of more than one project. More information in the Projects tab.
Continuities
Z - Vyzkumny zamer (s odkazem do CEZ)
Others
Publication year
2009
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Proceedings of the 15th International Conference on Parallel and Distributed Systems
ISBN
978-0-7695-3900-3
ISSN
—
e-ISSN
—
Number of pages
8
Pages from-to
—
Publisher name
Roy Sterritt
Place of publication
Neuveden
Event location
Shezhen, Čína
Event date
Dec 8, 2009
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—