TY - GEN
T1 - ParaMoC
T2 - 19th International Conference on Algorithms and Architectures for Parallel Processing, ICA3PP 2019
AU - Wei, Hansheng
AU - Ye, Xin
AU - Shi, Jianqi
AU - Huang, Yanhong
N1 - Publisher Copyright:
© 2020, Springer Nature Switzerland AG.
PY - 2020
Y1 - 2020
N2 - Model checking on Pushdown Systems (PDSs) has been extensively used to deal with numerous practical problems. However, the existing model checkers for pushdown systems are executed on the central processing unit (CPU), the performance is hampered by the computing power of the CPU. Compared with the CPU, the graphics processing unit (GPU) has more processing cores, which are suitable and efficient for parallel computing. Therefore, it is very attractive to accelerate model checking of PDSs on the GPU. In this paper, we present a new parallel model checker, named ParaMoC, to speed up the performance of model checking problems for pushdown systems (PDSs). Moreover, we focus on how to use Graphics Processing Units (GPUs) to accelerate the reachability verification and the LTL model checking of PDSs. The ParaMoC running on a state-of-the-art GPU can be 100 times faster than the traditional PDS model checker.
AB - Model checking on Pushdown Systems (PDSs) has been extensively used to deal with numerous practical problems. However, the existing model checkers for pushdown systems are executed on the central processing unit (CPU), the performance is hampered by the computing power of the CPU. Compared with the CPU, the graphics processing unit (GPU) has more processing cores, which are suitable and efficient for parallel computing. Therefore, it is very attractive to accelerate model checking of PDSs on the GPU. In this paper, we present a new parallel model checker, named ParaMoC, to speed up the performance of model checking problems for pushdown systems (PDSs). Moreover, we focus on how to use Graphics Processing Units (GPUs) to accelerate the reachability verification and the LTL model checking of PDSs. The ParaMoC running on a state-of-the-art GPU can be 100 times faster than the traditional PDS model checker.
UR - https://www.scopus.com/pages/publications/85082117359
U2 - 10.1007/978-3-030-38961-1_26
DO - 10.1007/978-3-030-38961-1_26
M3 - 会议稿件
AN - SCOPUS:85082117359
SN - 9783030389604
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 305
EP - 312
BT - Algorithms and Architectures for Parallel Processing - 19th International Conference, ICA3PP 2019, Proceedings
A2 - Wen, Sheng
A2 - Zomaya, Albert
A2 - Yang, Laurence T.
PB - Springer
Y2 - 9 December 2019 through 11 December 2019
ER -