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
Description
Summary: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).
ISSN:1530-8669
1530-8677