CUDA Accelerated LTL Model Checking
- 1 January 2009
- conference paper
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
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 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.Keywords
This publication has 12 references indexed in Scilit:
- DiVinE Multi-Core – A Parallel LTL Model-CheckerLecture Notes in Computer Science, 2008
- Scalable Multi-core LTL Model-CheckingPublished by Springer Science and Business Media LLC ,2007
- How to Order Vertices for Distributed LTL Model-Checking Based on Accepting PredecessorsElectronic Notes in Theoretical Computer Science, 2006
- DiVinE – A Tool for Distributed VerificationLecture Notes in Computer Science, 2006
- A Note on On-the-Fly Verification AlgorithmsLecture Notes in Computer Science, 2005
- Accepting Predecessors Are Better than Back Edges in Distributed LTL Model-CheckingLecture Notes in Computer Science, 2004
- Distributed Explicit Fair Cycle Detection (Set Based Approach)Lecture Notes in Computer Science, 2003
- Memory-efficient algorithms for the verification of temporal propertiesFormal Methods in System Design, 1992
- Depth-first search is inherently sequentialInformation Processing Letters, 1985
- Depth-First Search and Linear Graph AlgorithmsSIAM Journal on Computing, 1972