{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:49:54Z","timestamp":1750308594584,"version":"3.41.0"},"reference-count":24,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2017,1,5]],"date-time":"2017-01-05T00:00:00Z","timestamp":1483574400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGSOFT Softw. Eng. Notes"],"published-print":{"date-parts":[[2017,1,5]]},"abstract":"<jats:p>While annotating functional correctness properties of code, e.g., using assertions, enables automated conformance checking of program behaviors to expected properties and has found its use in many bug finding techniques, efficiently checking properties in practice remains challenging. In this paper, we introduce a novel approach to distributing checking properties using staged symbolic execution, which consists of two stages: (1) the first stage searches for all feasible paths to the checked properties as targets for the second stage, and (2) the second stage distributes property checking along these target paths among multiple workers, each focusing on one or more paths depending on the available computing resources. We implement our approach on top of Symbolic PathFinder, and our experience with our approach in checking assertions annotated in two Java programs shows its effectiveness<\/jats:p>","DOI":"10.1145\/3011286.3011297","type":"journal-article","created":{"date-parts":[[2017,1,6]],"date-time":"2017-01-06T13:30:07Z","timestamp":1483709407000},"page":"1-5","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Staged Symbolic Execution for Parallel Property Checking"],"prefix":"10.1145","volume":"41","author":[{"given":"Junye","family":"Wen","sequence":"first","affiliation":[{"name":"Texas State University, San Marcos, TX"}]},{"given":"Guowei","family":"Yang","sequence":"additional","affiliation":[{"name":"Texas State University, San Marcos, TX"}]}],"member":"320","published-online":{"date-parts":[[2017,1,5]]},"reference":[{"key":"e_1_2_1_1_1","first-page":"115","volume-title":"O'Hearn. Smallfoot: Modular Automatic Assertion Checking with Separation Logic","author":"Berdine J.","year":"2006"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1966445.1966463"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1713254.1713257"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/800191.805647"},{"volume-title":"A historical perspective on runtime assertion checking in software development. SIGSOFT Software Engineering Notes, 31(3)","year":"2006","author":"Clarke L. A.","key":"e_1_2_1_5_1"},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","first-page":"762","DOI":"10.1145\/337180.337625","volume-title":"Proceedings of the 22th International Conference on Software Engineering","author":"Corbett J. C.","year":"2000"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/367390.367400"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2338965.2336763"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2007.370410"},{"key":"e_1_2_1_12_1","first-page":"134","volume-title":"Tackling Large Verification Problems with the Swarm Tool","author":"Holzmann G. J.","year":"2008"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2004.05.015"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0022115"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1858996.1859035"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSTE.2010.5608866"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1831708.1831732"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(84)90020-5"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2830719.2830729"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568319"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606713"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2338965.2336771"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2610384.2610389"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3011286.3011297","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3011286.3011297","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:29Z","timestamp":1750273529000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3011286.3011297"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1,5]]},"references-count":24,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2017,1,5]]}},"alternative-id":["10.1145\/3011286.3011297"],"URL":"https:\/\/doi.org\/10.1145\/3011286.3011297","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2017,1,5]]},"assertion":[{"value":"2017-01-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}