Name
Abstract | ||
|---|---|---|
Pushdown systems (PDSs) have been widely used in program verification, such as recursive programs, malware detection, and other model-checking problems. As programs become more complicated, the model-checking process of PDSs represents a real challenge, which is the well-known state explosion problem. This problem may be cost expensive both in terms of memory and time. Parallel computing has been introduced to overcome this limitation, especially GPU computing. In this paper, we propose novel parallel algorithms to accelerate model checking on PDSs according to the characteristics of automata-theoretic. To represent the model-checking process on parallel architectures, we propose two new models: multi-threaded P-automaton and multi-threaded Buchi pushdown systems. Moreover, we design a highly efficient data structure for PDSs and dynamic task management to accommodate the GPU. Compared with Moped, a popular model checker for PDSs, our approach achieves promising performance. |
Year | DOI | Venue |
|---|---|---|
2018 | 10.1109/BDCloud.2018.00026 | 2018 IEEE Intl Conf on Parallel & Distributed Processing with Applications, Ubiquitous Computing & Communications, Big Data & Cloud Computing, Social Computing & Networking, Sustainable Computing & Communications (ISPA/IUCC/BDCloud/SocialCom/SustainCom) |
Keywords | Field | DocType |
GPU,Parallel computing,CUDA,Model Checking,Pushdown Systems | Data structure,Task management,Model checking,Parallel algorithm,Computer science,CUDA,Parallel computing,Human–computer interaction,General-purpose computing on graphics processing units,Malware,Recursion | Conference |
ISSN | ISBN | Citations |
2158-9178 | 978-1-7281-1141-4 | 0 |
PageRank | References | Authors |
0.34 | 0 | 6 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Hansheng Wei | 1 | 6 | 1.84 |
| Xinyu Chen | 2 | 29 | 7.43 |
| Xin Ye | 3 | 1 | 1.71 |
| Neng Fu | 4 | 0 | 0.34 |
| Yanhong Huang | 5 | 49 | 10.56 |
| Jianqi Shi | 6 | 12 | 5.70 |