{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,7]],"date-time":"2026-01-07T08:10:48Z","timestamp":1767773448694,"version":"3.44.0"},"publisher-location":"New York, NY, USA","reference-count":10,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,9,22]],"date-time":"2023-09-22T00:00:00Z","timestamp":1695340800000},"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":[[2023,9,22]]},"DOI":"10.1145\/3660395.3660460","type":"proceedings-article","created":{"date-parts":[[2024,6,1]],"date-time":"2024-06-01T18:30:40Z","timestamp":1717266640000},"page":"382-387","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["A Strategy to Unwind Loops in Incremental Bounded Model Checking for Software"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-9103-7428","authenticated-orcid":false,"given":"Yu","family":"Wu","sequence":"first","affiliation":[{"name":"China Aerospace Academy of Systems Science and Engineering, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-1153-0177","authenticated-orcid":false,"given":"Qilin","family":"Deng","sequence":"additional","affiliation":[{"name":"China Aerospace Academy of Systems Science and Engineering, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-2983-8592","authenticated-orcid":false,"given":"Wei","family":"Zhang","sequence":"additional","affiliation":[{"name":"China Aerospace Academy of Systems Science and Engineering, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,6]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/648063.747438"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-11494-7_22"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_31"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/3220903.3221138"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2011.59"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-017-0419-1"},{"key":"e_1_3_2_1_8_1","unstructured":"Aldughaim M. Alshmrany K. Menezes R. Cordeiro L. & Stancu A. 2020. Incremental Symbolic Bounded Model Checking of Software Using Interval Methods via Contractors. arXiv preprint arXiv:2012.11245."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"crossref","unstructured":"Jaulin L. Kieffer M. Didrit O. Walter E. Jaulin L. Kieffer M. ... & Walter \u00c9. 2001. Interval analysis (pp. 11-43).","DOI":"10.1007\/978-1-4471-0249-6_2"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Biere A. Cimatti A. Clarke E. & Zhu Y. 1999. Symbolic model checking without BDDs. In Tools and Algorithms for the Construction and Analysis of Systems: 5th International Conference TACAS\u201999 Held as Part of the Joint European Conferences on Theory and Practice of Software ETAPS\u201999 Amsterdam The Netherlands March 22\u201328 1999 Proceedings 5 (pp. 193-207).","DOI":"10.1007\/3-540-49059-0_14"}],"event":{"name":"AIBDF 2023: 2023 3rd Guangdong-Hong Kong-Macao Greater Bay Area Artificial Intelligence and Big Data Forum","acronym":"AIBDF 2023","location":"Guangzhou China"},"container-title":["Proceedings of the 2023 3rd Guangdong-Hong Kong-Macao Greater Bay Area Artificial Intelligence and Big Data Forum"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3660395.3660460","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3660395.3660460","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T23:34:24Z","timestamp":1755905664000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3660395.3660460"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,22]]},"references-count":10,"alternative-id":["10.1145\/3660395.3660460","10.1145\/3660395"],"URL":"https:\/\/doi.org\/10.1145\/3660395.3660460","relation":{},"subject":[],"published":{"date-parts":[[2023,9,22]]},"assertion":[{"value":"2024-06-01","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}