Skip to main navigation Skip to search Skip to main content

Parallel model checking on pushdown systems

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

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.

Original languageEnglish
Title of host publicationProceedings - 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
EditorsJinjun Chen, Laurence T. Yang
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages88-95
Number of pages8
ISBN (Electronic)9781728111414
DOIs
StatePublished - 2 Jul 2018
Event16th 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, Australia
Duration: 11 Dec 201813 Dec 2018

Publication series

NameProceedings - 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

Conference

Conference16th 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
Country/TerritoryAustralia
CityMelbourne
Period11/12/1813/12/18

Keywords

  • CUDA
  • GPU
  • Model Checking
  • Parallel computing
  • Pushdown Systems

Fingerprint

Dive into the research topics of 'Parallel model checking on pushdown systems'. Together they form a unique fingerprint.

Cite this