{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:13:43Z","timestamp":1750220023805,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":8,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,9,28]],"date-time":"2022-09-28T00:00:00Z","timestamp":1664323200000},"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":[],"published-print":{"date-parts":[[2022,9,28]]},"DOI":"10.1145\/3568364.3568371","type":"proceedings-article","created":{"date-parts":[[2022,12,23]],"date-time":"2022-12-23T16:44:55Z","timestamp":1671813895000},"page":"39-44","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Quantified Assertion Verification Method for Non-linear Arithmetic and Mutable Data Structures"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9284-7433","authenticated-orcid":false,"given":"Xuejian","family":"Li","sequence":"first","affiliation":[{"name":"Anhui University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0456-6629","authenticated-orcid":false,"given":"Yun","family":"Yu","sequence":"additional","affiliation":[{"name":"Anhui University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,12,23]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"A Generic Theorem Prover","author":"Paulson L. C.","year":"1994","unstructured":"Paulson , L. C. , & Isabelle , A. ( 1994 ). A Generic Theorem Prover . Paulson, L. C., & Isabelle, A. (1994). A Generic Theorem Prover."},{"key":"e_1_3_2_1_3_1","volume-title":"A shape graph logic and a shape system.\u00a0Journal of Computer Science and Technology,\u00a028(6), 1063-1084","author":"Li Z. P.","year":"2013","unstructured":"Li , Z. P. , Zhang , Y. , & Chen , Y. Y. ( 2013 ). A shape graph logic and a shape system.\u00a0Journal of Computer Science and Technology,\u00a028(6), 1063-1084 . Li, Z. P., Zhang, Y., & Chen, Y. Y. (2013). A shape graph logic and a shape system.\u00a0Journal of Computer Science and Technology,\u00a028(6), 1063-1084."},{"key":"e_1_3_2_1_4_1","volume-title":"Acsl: Ansi c specification language.\u00a0CEA-LIST","author":"Baudin P.","year":"2008","unstructured":"Baudin , P. , Filli\u00e2tre , J. C. , March\u00e9 , C. , Monate , B. , Moy , Y. , & Prevosto , V. ( 2008 ). Acsl: Ansi c specification language.\u00a0CEA-LIST , Saclay, France , Tech. Rep . v1,\u00a02. Baudin, P., Filli\u00e2tre, J. C., March\u00e9, C., Monate, B., Moy, Y., & Prevosto, V. (2008). Acsl: Ansi c specification language.\u00a0CEA-LIST, Saclay, France, Tech. Rep. v1,\u00a02."},{"key":"e_1_3_2_1_5_1","volume-title":"In\u00a0International conference on Tools and Algorithms for the Construction and Analysis of Systems\u00a0(pp. 337-340)","author":"Moura L. D.","year":"2008","unstructured":"Moura , L. D. , & Bj\u00f8rner , N. ( 2008 , March). Z3: An efficient SMT solver . In\u00a0International conference on Tools and Algorithms for the Construction and Analysis of Systems\u00a0(pp. 337-340) . Springer, Berlin, Heidelberg. Moura, L. D., & Bj\u00f8rner, N. (2008, March). Z3: An efficient SMT solver. In\u00a0International conference on Tools and Algorithms for the Construction and Analysis of Systems\u00a0(pp. 337-340). Springer, Berlin, Heidelberg."},{"issue":"5","key":"e_1_3_2_1_6_1","first-page":"1002","article-title":"Formal Verification of One-dimensional Array Programs","volume":"36","author":"Han Y. H","year":"2015","unstructured":"Han Y. H , Chen Y. Y , Li Z. P. ( 2015 ). Formal Verification of One-dimensional Array Programs . Journal of Chinese Computer Systems , 36 ( 5 ): 1002 - 1006 . Han Y. H, Chen Y. Y, Li Z. P. (2015). Formal Verification of One-dimensional Array Programs. Journal of Chinese Computer Systems, 36(5): 1002-1006.","journal-title":"Journal of Chinese Computer Systems"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_2_1_8_1","volume-title":"An automatic program verifier for PointerC: design and implementation.\u00a0Journal of Computer Research and Development,\u00a050(5), 1044","author":"Zhang Z.","year":"2013","unstructured":"Zhang , Z. , Li , Z. , Chen , Y. , & Liu , G. ( 2013 ). An automatic program verifier for PointerC: design and implementation.\u00a0Journal of Computer Research and Development,\u00a050(5), 1044 . Zhang, Z., Li, Z., Chen, Y., & Liu, G. (2013). An automatic program verifier for PointerC: design and implementation.\u00a0Journal of Computer Research and Development,\u00a050(5), 1044."},{"key":"e_1_3_2_1_9_1","volume-title":"A new correctness proof of the Nelson-Oppen combination procedure. In\u00a0Frontiers of Combining Systems (pp. 103-119)","author":"Tinelli C.","year":"1996","unstructured":"Tinelli , C. , & Harandi , M. ( 1996 ). A new correctness proof of the Nelson-Oppen combination procedure. In\u00a0Frontiers of Combining Systems (pp. 103-119) . Springer , Dordrecht . Tinelli, C., & Harandi, M. (1996). A new correctness proof of the Nelson-Oppen combination procedure. In\u00a0Frontiers of Combining Systems (pp. 103-119). Springer, Dordrecht."}],"event":{"name":"WSSE 2022: 2022 The 4th World Symposium on Software Engineering","acronym":"WSSE 2022","location":"Xiamen China"},"container-title":["Proceedings of the 4th World Symposium on Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3568364.3568371","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3568364.3568371","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T17:51:33Z","timestamp":1750182693000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3568364.3568371"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,9,28]]},"references-count":8,"alternative-id":["10.1145\/3568364.3568371","10.1145\/3568364"],"URL":"https:\/\/doi.org\/10.1145\/3568364.3568371","relation":{},"subject":[],"published":{"date-parts":[[2022,9,28]]},"assertion":[{"value":"2022-12-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}