CUDA Accelerated LTL Model Checking

Jiri Barnat, Lubos Brim, Milan Ceska, Tomas Lamr
Faculty of Informatics, Masaryk University, Botanicka 68a, 60200 Brno, Czech Republic
15th International Conference on Parallel and Distributed Systems (ICPADS), 2009


   title={CUDA accelerated LTL model checking},

   author={Barnat, J. and Brim, L. and Ceska, M. and Lamr, T.},

   booktitle={Parallel and Distributed Systems (ICPADS), 2009 15th International Conference on},





Download Download (PDF)   View View   Source Source   



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 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.
No votes yet.
Please wait...

* * *

* * *

HGPU group © 2010-2020 hgpu.org

All rights belong to the respective authors

Contact us: