跳到主要导航 跳到搜索 跳到主要内容

Parallel model checking on pushdown systems

科研成果: 书/报告/会议事项章节会议稿件同行评审

摘要

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.

源语言英语
主期刊名Proceedings - 16th IEEE International Symposium on Parallel and Distributed Processing with Applications, 17th IEEE International Conference on Ubiquitous Computing and Communications, 8th IEEE International Conference on Big Data and Cloud Computing, 11th IEEE International Conference on Social Computing and Networking and 8th IEEE International Conference on Sustainable Computing and Communications, ISPA/IUCC/BDCloud/SocialCom/SustainCom 2018
编辑Jinjun Chen, Laurence T. Yang
出版商Institute of Electrical and Electronics Engineers Inc.
88-95
页数8
ISBN(电子版)9781728111414
DOI
出版状态已出版 - 2 7月 2018
活动16th IEEE International Symposium on Parallel and Distributed Processing with Applications, 17th IEEE International Conference on Ubiquitous Computing and Communications, 8th IEEE International Conference on Big Data and Cloud Computing, 11th IEEE International Conference on Social Computing and Networking and 8th IEEE International Conference on Sustainable Computing and Communications, ISPA/IUCC/BDCloud/SocialCom/SustainCom 2018 - Melbourne, 澳大利亚
期限: 11 12月 201813 12月 2018

出版系列

姓名Proceedings - 16th IEEE International Symposium on Parallel and Distributed Processing with Applications, 17th IEEE International Conference on Ubiquitous Computing and Communications, 8th IEEE International Conference on Big Data and Cloud Computing, 11th IEEE International Conference on Social Computing and Networking and 8th IEEE International Conference on Sustainable Computing and Communications, ISPA/IUCC/BDCloud/SocialCom/SustainCom 2018

会议

会议16th IEEE International Symposium on Parallel and Distributed Processing with Applications, 17th IEEE International Conference on Ubiquitous Computing and Communications, 8th IEEE International Conference on Big Data and Cloud Computing, 11th IEEE International Conference on Social Computing and Networking and 8th IEEE International Conference on Sustainable Computing and Communications, ISPA/IUCC/BDCloud/SocialCom/SustainCom 2018
国家/地区澳大利亚
Melbourne
时期11/12/1813/12/18

指纹

探究 'Parallel model checking on pushdown systems' 的科研主题。它们共同构成独一无二的指纹。

引用此