{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T03:12:44Z","timestamp":1782875564619,"version":"3.54.5"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2014,9,5]],"date-time":"2014-09-05T00:00:00Z","timestamp":1409875200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["D917007, 1218993, and 1320326"],"award-info":[{"award-number":["D917007, 1218993, and 1320326"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002920","name":"Research Grants Council, University Grants Committee, Hong Kong","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100002920","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2014,9,5]]},"abstract":"<jats:p>Path explosion is a major issue in applying path-sensitive symbolic analysis to large programs. We observe that many symbolic states generated by the symbolic analysis of a procedure are indistinguishable to its callers. It is, therefore, possible to keep only one state from each set of equivalent symbolic states without affecting the analysis result. Based on this observation, we propose an equivalence relation called z-equivalence, which is weaker than logical equivalence, to relate a large number of z-equivalent states. We prove that z-equivalence is strong enough to guarantee that paths to be traversed by the symbolic analysis of two z-equivalent states are identical, giving the same solutions to satisfiability and validity queries. We propose a sound linear algorithm to detect z-equivalence. Our experiments show that the symbolic analysis that leverages z-equivalence is able to achieve more than ten orders of magnitude reduction in terms of search space. The reduction significantly alleviates the path explosion problem, enabling us to apply symbolic analysis in large programs such as Hadoop and Linux Kernel.<\/jats:p>","DOI":"10.1145\/2652484","type":"journal-article","created":{"date-parts":[[2014,9,9]],"date-time":"2014-09-09T14:39:29Z","timestamp":1410273569000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Scaling Up Symbolic Analysis by Removing Z-Equivalent States"],"prefix":"10.1145","volume":"23","author":[{"given":"Yueqi","family":"Li","sequence":"first","affiliation":[{"name":"Hong Kong University of Science and Technology"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"S. C.","family":"Cheung","sequence":"additional","affiliation":[{"name":"Hong Kong University of Science and Technology"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xiangyu","family":"Zhang","sequence":"additional","affiliation":[{"name":"Purdue University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yepang","family":"Liu","sequence":"additional","affiliation":[{"name":"Hong Kong University of Science and Technology"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2014,9,5]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-008-0090-1"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368088.1368118"},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the 19th International Conference on Computer Aided Verification (CAV'07)","author":"Babic Domagoj"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792770"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the USENIX Annual Technical Conference (ATC'13)","author":"Bugrara Suhabe","year":"2013"},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI'08)","author":"Cadar Cristian","year":"2008"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542517"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1866307.1866373"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2110356.2110358"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1976.233817"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/775832.775928"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2451116.2451152"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375615"},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of the 19th International Conference on Computer Aided Verification (CAV'07)","author":"Ganesh Vijay"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190226"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375616"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1181775.1181785"},{"key":"e_1_2_1_19_1","volume-title":"Logic in Computer Science: Modelling and Reasoning about Systems","author":"Huth Michael"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765871.1765924"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPSN.2008.62"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254088"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.24143"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103701"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1453101.1453131"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993558"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390635"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/WCRE.2012.51"},{"key":"e_1_2_1_31_1","volume-title":"Reiter and Matthew Johnson Clayton","author":"Edna","year":"2013"},{"key":"e_1_2_1_32_1","volume-title":"Artificial Intelligence, A Modern Approach","author":"Russell Stuart"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1831708.1831733"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081750"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384654"},{"key":"e_1_2_1_36_1","series-title":"Computation in Cognitive Science Series","volume-title":"Foundations of Constraint Satisfaction","author":"Tsang Edward"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146238.1146243"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/940071.940115"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2652484","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2652484","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:11:55Z","timestamp":1750227115000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2652484"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,9,5]]},"references-count":37,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,9,5]]}},"alternative-id":["10.1145\/2652484"],"URL":"https:\/\/doi.org\/10.1145\/2652484","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"value":"1049-331X","type":"print"},{"value":"1557-7392","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,9,5]]},"assertion":[{"value":"2013-07-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-09-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}