{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T13:16:56Z","timestamp":1753881416358,"version":"3.41.2"},"reference-count":36,"publisher":"Wiley","issue":"1","license":[{"start":{"date-parts":[[2018,1,28]],"date-time":"2018-01-28T00:00:00Z","timestamp":1517097600000},"content-version":"vor","delay-in-days":27,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61133007"],"award-info":[{"award-number":["61133007"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["onlinelibrary.wiley.com"],"crossmark-restriction":true},"short-container-title":["Wireless Communications and Mobile Computing"],"published-print":{"date-parts":[[2018,1]]},"abstract":"<jats:p>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\u2010based 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\u2010based 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).<\/jats:p>","DOI":"10.1155\/2018\/3193974","type":"journal-article","created":{"date-parts":[[2018,1,28]],"date-time":"2018-01-28T23:31:09Z","timestamp":1517182269000},"update-policy":"https:\/\/doi.org\/10.1002\/crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["An SAT\u2010Based Method to Multithreaded Program Verification for Mobile Crowdsourcing Networks"],"prefix":"10.1155","volume":"2018","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1633-4051","authenticated-orcid":false,"given":"Long","family":"Zhang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3224-8233","authenticated-orcid":false,"given":"Wanxia","family":"Qu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yinjia","family":"Huo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9050-0866","authenticated-orcid":false,"given":"Yang","family":"Guo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sikun","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","published-online":{"date-parts":[[2018,1,28]]},"reference":[{"key":"e_1_2_9_1_2","doi-asserted-by":"publisher","DOI":"10.1109\/MCOM.2015.7180511"},{"key":"e_1_2_9_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2017.2782881"},{"key":"e_1_2_9_3_2","doi-asserted-by":"crossref","unstructured":"ParshotamK. Crowd computing: a literature review and definition Proceedings of the South African Institute for Computer Scientists and Information Technologists Conference October 2013 East London South Africa the Association for Computing Machinery 121\u2013130 https:\/\/doi.org\/10.1145\/2513456.2513470.","DOI":"10.1145\/2513456.2513470"},{"key":"e_1_2_9_4_2","doi-asserted-by":"publisher","DOI":"10.1109\/JIOT.2017.2764259"},{"key":"e_1_2_9_5_2","doi-asserted-by":"publisher","DOI":"10.1109\/mcom.2011.6069707"},{"key":"e_1_2_9_6_2","doi-asserted-by":"publisher","DOI":"10.1109\/tetc.2013.2273359"},{"key":"e_1_2_9_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/COMST.2014.2371813"},{"key":"e_1_2_9_8_2","doi-asserted-by":"publisher","DOI":"10.1109\/TETC.2015.2395959"},{"key":"e_1_2_9_9_2","doi-asserted-by":"crossref","unstructured":"AbdullaP. A. CeransK. JonssonB. andTsayY.-K. General decidability theorems for infinite-state systems Proceedings of the Eleventh Annual IEEE Symposium on Logic in Computer Science (LICS\u201996) 1996 313\u2013321 MR1461844.","DOI":"10.1109\/LICS.1996.561359"},{"key":"e_1_2_9_10_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00102-X"},{"key":"e_1_2_9_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32940-1_35"},{"key":"e_1_2_9_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58152-9_11"},{"key":"e_1_2_9_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055044"},{"key":"e_1_2_9_14_2","doi-asserted-by":"publisher","DOI":"10.7146\/brics.v1i8.21662"},{"key":"e_1_2_9_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40184-8_2"},{"key":"e_1_2_9_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30538-5_24"},{"key":"e_1_2_9_17_2","doi-asserted-by":"crossref","unstructured":"EmersonE. A.andNamjoshiK. S. On model checking for non-deterministic infinite-state systems Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science 1998 IEEE 70\u201380 MR1654516.","DOI":"10.1109\/LICS.1998.705644"},{"key":"e_1_2_9_18_2","doi-asserted-by":"crossref","unstructured":"EsparzaJ. FinkelA. andMayrR. On the verification of broadcast protocols Proceedings of the 14th Symposium on Logic in Computer Science 1999 IEEE 352\u2013359 MR1943429.","DOI":"10.1109\/LICS.1999.782630"},{"key":"e_1_2_9_19_2","doi-asserted-by":"crossref","unstructured":"AbdullaP. A. BouajjaniA. andJonssonB. On-the-fly analysis of systems with unbounded lossy fifo channels Proceedings of the International Conference on Computer Aided Verification 1998 Springer 305\u2013318 MR1729044.","DOI":"10.1007\/BFb0028754"},{"key":"e_1_2_9_20_2","doi-asserted-by":"crossref","unstructured":"BinghamJ.andHuA. J. Empirically Efficient Verification for a Class of Infinite-State Systems 3440 Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems 2005 Springer 77\u201392 https:\/\/doi.org\/10.1007\/978-3-540-31980-1_6 Zbl1087.68584.","DOI":"10.1007\/978-3-540-31980-1_6"},{"key":"e_1_2_9_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_10"},{"key":"e_1_2_9_22_2","doi-asserted-by":"publisher","DOI":"10.1145\/2629608"},{"key":"e_1_2_9_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"e_1_2_9_24_2","unstructured":"EenN. MishchenkoA. andBraytonR. Efficient implementation of property directed reachability Proceedings of the Formal Methods in Computer-Aided Design FMCAD \u203211 November 2011 125\u2013134 2-s2.0-84857697806."},{"key":"e_1_2_9_25_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63166-6_10"},{"key":"e_1_2_9_26_2","doi-asserted-by":"crossref","unstructured":"Col\u00f3nM. A.andUribeT. E. Generating finite-state abstractions of reactive systems using decision procedures 1998 Proceedings of the International Conference on Computer Aided Verification Springer 293\u2013304 MR1729043.","DOI":"10.1007\/BFb0028753"},{"key":"e_1_2_9_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"e_1_2_9_28_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"e_1_2_9_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_40"},{"key":"e_1_2_9_30_2","doi-asserted-by":"publisher","DOI":"10.1109\/5.24143"},{"key":"e_1_2_9_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33278-4"},{"key":"e_1_2_9_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_35"},{"key":"e_1_2_9_33_2","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s3-2.1.326"},{"key":"e_1_2_9_34_2","series-title":"Lecture Notes in Computer Science","first-page":"570","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005)","author":"Clarke E."},{"key":"e_1_2_9_35_2","doi-asserted-by":"publisher","DOI":"10.1155\/2017\/5731678"},{"key":"e_1_2_9_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_24"}],"container-title":["Wireless Communications and Mobile Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/downloads.hindawi.com\/journals\/wcmc\/2018\/3193974.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/downloads.hindawi.com\/journals\/wcmc\/2018\/3193974.xml","content-type":"application\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1155\/2018\/3193974","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,30]],"date-time":"2025-06-30T01:29:44Z","timestamp":1751246984000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1155\/2018\/3193974"}},"subtitle":[],"editor":[{"given":"Edith","family":"Ngai","sequence":"additional","affiliation":[],"role":[{"role":"editor","vocabulary":"crossref"}]}],"short-title":[],"issued":{"date-parts":[[2018,1]]},"references-count":36,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1155\/2018\/3193974"],"URL":"https:\/\/doi.org\/10.1155\/2018\/3193974","archive":["Portico"],"relation":{},"ISSN":["1530-8669","1530-8677"],"issn-type":[{"type":"print","value":"1530-8669"},{"type":"electronic","value":"1530-8677"}],"subject":[],"published":{"date-parts":[[2018,1]]},"assertion":[{"value":"2017-09-23","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-01-01","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-01-28","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}],"article-number":"3193974"}}