Publication details
CUDA Accelerated LTL Model Checking
| Basic information | |
|---|---|
| Original title: | CUDA Accelerated LTL Model Checking |
| Authors: | Jiří Barnat, Luboš Brim, Milan Češka, Tomáš Lamr |
| Further information | |
|---|---|
| Citation: | BARNAT, Jiří  - BRIM, Luboš - ČEŠKA, Milan - LAMR, Tomáš. CUDA Accelerated LTL Model Checking. In Proceedings of the 15th International Conference on Parallel and Distributed Systems. Neuveden : Roy Sterritt, 2009. ISBN 978-0-7695-3900-3, pp. 34-41. 8.12.2009, Shezhen, Čína. |
| Original language: | English |
| Field: | Informatika |
| Type: | Article in Proceedings |
| Keywords: | Model Checking; Linear Temporal Logic; CUDA |
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.
Related projects:
- Techniques for automatic verification and validation of software nad hardware systems
- Highly Parallel and Distributed Computing Systems
- Verification and Analysis of Large-Scale Computer Systems
- Automated formal verification using modern hardware
- 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ů
