An SAT-Based Method to Multithreaded Program Verification for Mobile Crowdsourcing Networks

An SAT-Based Method to Multithreaded Program Verification for Mobile Crowdsourcing Networks

This paper focused on the safety verification of the multithreaded programs for mobile crowdsourcing networks. A novel algorithm was proposed to find a way to apply IC3, which is typically the fastest algorithm for SAT-based finite state model checking, in a very clever manner to solve the safety pr...

Full description

Bibliographic Details
Main Authors: Long Zhang, Wanxia Qu, Yinjia Huo, Yang Guo, Sikun Li
Format: Article
Language:English
Published: Hindawi-Wiley 2018-01-01
Series:Wireless Communications and Mobile Computing
Online Access:http://dx.doi.org/10.1155/2018/3193974
id doaj-fe4a61c8485b4d8e90e2ac6dcf0e5bd1
record_format Article
spelling doaj-fe4a61c8485b4d8e90e2ac6dcf0e5bd12020-11-24T23:07:40ZengHindawi-WileyWireless Communications and Mobile Computing1530-86691530-86772018-01-01201810.1155/2018/31939743193974An SAT-Based Method to Multithreaded Program Verification for Mobile Crowdsourcing NetworksLong Zhang0Wanxia Qu1Yinjia Huo2Yang Guo3Sikun Li4College of Computer, National University of Defense Technology, Changsha, ChinaCollege of Computer, National University of Defense Technology, Changsha, ChinaThe University of British Columbia, Vancouver, BC, V6T 1Z4, CanadaCollege of Computer, National University of Defense Technology, Changsha, ChinaCollege of Computer, National University of Defense Technology, Changsha, ChinaThis paper focused on the safety verification of the multithreaded programs for mobile crowdsourcing networks. A novel algorithm was proposed to find a way to apply IC3, which is typically the fastest algorithm for SAT-based finite state model checking, in a very clever manner to solve the safety problem of multithreaded programs. By computing a series of overapproximation reachability, the safety properties can be verified by the SAT-based model checking algorithms. The results show that the new algorithm outperforms all the recently published works, especially on memory consumption (an advantage that comes from IC3).http://dx.doi.org/10.1155/2018/3193974
collection DOAJ
language English
format Article
sources DOAJ
author Long Zhang
Wanxia Qu
Yinjia Huo
Yang Guo
Sikun Li
spellingShingle Long Zhang
Wanxia Qu
Yinjia Huo
Yang Guo
Sikun Li
An SAT-Based Method to Multithreaded Program Verification for Mobile Crowdsourcing Networks
Wireless Communications and Mobile Computing
author_facet Long Zhang
Wanxia Qu
Yinjia Huo
Yang Guo
Sikun Li
author_sort Long Zhang
title An SAT-Based Method to Multithreaded Program Verification for Mobile Crowdsourcing Networks
title_short An SAT-Based Method to Multithreaded Program Verification for Mobile Crowdsourcing Networks
title_full An SAT-Based Method to Multithreaded Program Verification for Mobile Crowdsourcing Networks
title_fullStr An SAT-Based Method to Multithreaded Program Verification for Mobile Crowdsourcing Networks
title_full_unstemmed An SAT-Based Method to Multithreaded Program Verification for Mobile Crowdsourcing Networks
title_sort sat-based method to multithreaded program verification for mobile crowdsourcing networks
publisher Hindawi-Wiley
series Wireless Communications and Mobile Computing
issn 1530-8669
1530-8677
publishDate 2018-01-01
description This paper focused on the safety verification of the multithreaded programs for mobile crowdsourcing networks. A novel algorithm was proposed to find a way to apply IC3, which is typically the fastest algorithm for SAT-based finite state model checking, in a very clever manner to solve the safety problem of multithreaded programs. By computing a series of overapproximation reachability, the safety properties can be verified by the SAT-based model checking algorithms. The results show that the new algorithm outperforms all the recently published works, especially on memory consumption (an advantage that comes from IC3).
url http://dx.doi.org/10.1155/2018/3193974
work_keys_str_mv AT longzhang ansatbasedmethodtomultithreadedprogramverificationformobilecrowdsourcingnetworks
AT wanxiaqu ansatbasedmethodtomultithreadedprogramverificationformobilecrowdsourcingnetworks
AT yinjiahuo ansatbasedmethodtomultithreadedprogramverificationformobilecrowdsourcingnetworks
AT yangguo ansatbasedmethodtomultithreadedprogramverificationformobilecrowdsourcingnetworks
AT sikunli ansatbasedmethodtomultithreadedprogramverificationformobilecrowdsourcingnetworks
AT longzhang satbasedmethodtomultithreadedprogramverificationformobilecrowdsourcingnetworks
AT wanxiaqu satbasedmethodtomultithreadedprogramverificationformobilecrowdsourcingnetworks
AT yinjiahuo satbasedmethodtomultithreadedprogramverificationformobilecrowdsourcingnetworks
AT yangguo satbasedmethodtomultithreadedprogramverificationformobilecrowdsourcingnetworks
AT sikunli satbasedmethodtomultithreadedprogramverificationformobilecrowdsourcingnetworks
_version_ 1725617668386455552

Similar Items