{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T06:25:12Z","timestamp":1769754312057,"version":"3.49.0"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2015,11,11]],"date-time":"2015-11-11T00:00:00Z","timestamp":1447200000000},"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":[[2015,11,11]]},"abstract":"<jats:p>Annotating functional correctness properties of code using assertions, in principle, enables systematic checking of code against behavioral properties. In practice however, checking assertions can be costly, especially for complex code annotated with rich behavioral properties. This paper introduces a novel approach for distributing the problem of checking assertions for better scalability. Leveraging that assertions should be side effect free, our approach distributes assertion checking into simpler sub-problems---each focusing on checking one single assertion, so that different assertions are checked in parallel among multiple workers. Furthermore, the sub-problem analysis performed by each worker is guided by the checked assertion to avoid irrelevant path exploration and is prioritized based on the distance towards the checked assertion to provide earlier feedback. A case study shows that our approach can provide a reduction in analysis time required for symbolic execution of Java programs compared to non-distributed approach using the Symbolic PathFinder tool.<\/jats:p>","DOI":"10.1145\/2830719.2830729","type":"journal-article","created":{"date-parts":[[2015,11,13]],"date-time":"2015-11-13T14:19:41Z","timestamp":1447424381000},"page":"1-5","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Distributed Assertion Checking Using Symbolic Execution"],"prefix":"10.1145","volume":"40","author":[{"given":"Guowei","family":"Yang","sequence":"first","affiliation":[{"name":"Texas State University, San Marcos, TX"}]},{"given":"Quan Chau Dong","family":"Do","sequence":"additional","affiliation":[{"name":"Texas State University, San Marcos, TX"}]},{"given":"Junye","family":"Wen","sequence":"additional","affiliation":[{"name":"Texas State University, San Marcos, TX"}]}],"member":"320","published-online":{"date-parts":[[2015,11,11]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0044-z"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/566172.566191"},{"key":"e_1_2_1_3_1","first-page":"209","volume-title":"Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI)","author":"Cadar C.","year":"2008","unstructured":"C. Cadar , D. Dunbar , and D. Engler . KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs . In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI) , pages 209 -- 224 , 2008 . C. Cadar, D. Dunbar, and D. Engler. KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI), pages 209--224, 2008."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/800191.805647"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1127878.1127900"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2007.62"},{"key":"e_1_2_1_8_1","volume-title":"Department of Electrical and Computer Engineering","author":"Ghori K.","year":"2006","unstructured":"K. Ghori . Constraint-based program repair. Master's thesis , Department of Electrical and Computer Engineering , University of Texas at Austin , Aug. 2006 . K. Ghori. Constraint-based program repair. Master's thesis, Department of Electrical and Computer Engineering, University of Texas at Austin, Aug. 2006."},{"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\/1065010.1065036"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001424"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2007.70724"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2010.110"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/347324.383378"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765871.1765924"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.5555\/380921.380931"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-013-0122-2"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1858996.1859035"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081750"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSTE.2010.5608866"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384654"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1831708.1831732"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/647766.736020"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022920129859"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568319"},{"key":"e_1_2_1_28_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\/2830719.2830729","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2830719.2830729","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:48:39Z","timestamp":1750225719000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2830719.2830729"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,11,11]]},"references-count":27,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2015,11,11]]}},"alternative-id":["10.1145\/2830719.2830729"],"URL":"https:\/\/doi.org\/10.1145\/2830719.2830729","relation":{},"ISSN":["0163-5948"],"issn-type":[{"value":"0163-5948","type":"print"}],"subject":[],"published":{"date-parts":[[2015,11,11]]},"assertion":[{"value":"2015-11-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}