DiVinE-CUDA - A Tool for GPU Accelerated LTL Model Checking

Investor logo
Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BARNAT Jiří BRIM Luboš ČEŠKA Milan

Year of publication 2009
Type Article in Periodical
Magazine / Source Electronic Proceedings in Theoretical Computer Science
MU Faculty or unit

Faculty of Informatics

Citation
Web http://dx.doi.org/10.4204/EPTCS.14.8
Field Informatics
Keywords LTL; Model Checking; CUDA
Description In this paper we present a tool that performs CUDA accelerated LTL Model Checking. The tool exploits parallel algorithm MAP adjusted to the NVIDIA CUDA architecture in order to efficiently detect the presence of accepting cycles in a directed graph. Accepting cycle detection is the core algorithmic procedure in automata-based LTL Model Checking. We demonstrate that the tool outperforms non-accelerated version of the algorithm and we discuss where the limits of the tool are and what we intend to do in the future to avoid them.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.