The Community for Technology Leaders
Parallel and Distributed Systems, International Conference on (2009)
Shenzhen, Guangdong, China
Dec. 9, 2009 to Dec. 11, 2009
ISSN: 1521-9097
ISBN: 978-0-7695-3900-3
pp: 34-41
ABSTRACT
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.
INDEX TERMS
LTL Model Checking, GPU, CUDA
CITATION

L. Brim, T. Lamr, J. Barnat and M. Ceška, "CUDA Accelerated LTL Model Checking," 2009 IEEE 15th International Conference on Parallel and Distributed Systems (ICPADS 2009)(ICPADS), Shenzhen, 2009, pp. 34-41.
doi:10.1109/ICPADS.2009.50
87 ms
(Ver 3.3 (11022016))