{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,23]],"date-time":"2025-08-23T00:10:05Z","timestamp":1755907805690,"version":"3.44.0"},"publisher-location":"New York, NY, USA","reference-count":9,"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.3660414","type":"proceedings-article","created":{"date-parts":[[2024,6,1]],"date-time":"2024-06-01T18:30:40Z","timestamp":1717266640000},"page":"104-109","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Multi-Property Bounded Model Checking for Java Numerical Error"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-1153-0177","authenticated-orcid":false,"given":"Qilin","family":"Deng","sequence":"first","affiliation":[{"name":"China Aerospace Academy of Systems Science and Engineering, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-9103-7428","authenticated-orcid":false,"given":"Yu","family":"Wu","sequence":"additional","affiliation":[{"name":"China Aerospace Academy of Systems Science and Engineering, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-4920-7348","authenticated-orcid":false,"given":"Fengli","family":"Sun","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","first-page":"10","article-title":"2.1 The Failure of the Ariane 5","volume":"29","author":"Finagle's Third Law A. B.","year":"2019","unstructured":"Finagle's Third Law, A. B. 2019. 2.1 The Failure of the Ariane 5. Bits and Bugs: A Scientific and Historical Review of Software Failures in Computational Science, 29, 10.","journal-title":"Bits and Bugs: A Scientific and Historical Review of Software Failures in Computational Science"},{"doi-asserted-by":"crossref","unstructured":"Min\u00e9 A. 2017. Tutorial on static inference of numeric invariants by abstract interpretation. Foundations and Trends\u00ae in Programming Languages 4(3-4) 120-372.","key":"e_1_3_2_1_2_1","DOI":"10.1561\/2500000034"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_3_1","DOI":"10.1007\/978-3-319-96145-3_10"},{"unstructured":"Huang Ming Zhan Haitan Zhang Wei Jing Xiaochuan Li Ning and Wang Xiaoyin. 2016. Numerical Runtime Error Check of Aerospace Safety-Critical Software. Space Control Technology and Applications (06) 58-62","key":"e_1_3_2_1_4_1"},{"volume-title":"Research and Implementation of Abstract Interpretation Methods for Numerical Properties of Program Variables (Master's Thesis","author":"Lu Chen","unstructured":"Lu Chen. 2017. Research and Implementation of Abstract Interpretation Methods for Numerical Properties of Program Variables (Master's Thesis, Nanjing University of Aeronautics and Astronautics)","key":"e_1_3_2_1_5_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_6_1","DOI":"10.1016\/j.scico.2021.102725"},{"key":"e_1_3_2_1_7_1","volume-title":"November. Detecting Out-of-Bounds Array Access Errors in Aerospace Embedded Software. In 2020 7th International Conference on Dependable Systems and Their Applications (DSA) (pp. 213-218)","author":"Chen R.","year":"2020","unstructured":"Chen, R., Yu, T., Jiang, Y., Jia, C., Li, C., Gao, D., & Yang, M. 2020, November. Detecting Out-of-Bounds Array Access Errors in Aerospace Embedded Software. In 2020 7th International Conference on Dependable Systems and Their Applications (DSA) (pp. 213-218). IEEE."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_8_1","DOI":"10.1007\/s10817-018-9492-2"},{"key":"e_1_3_2_1_9_1","first-page":"978","volume-title":"Cham: Springer.","author":"Clarke E. M.","year":"2018","unstructured":"Clarke, E. M., Henzinger, T. A., Veith, H., & Bloem, R. (Eds.). 2018. Handbook of model checking (Vol. 10, pp. 978-3). Cham: Springer."}],"event":{"acronym":"AIBDF 2023","name":"AIBDF 2023: 2023 3rd Guangdong-Hong Kong-Macao Greater Bay Area Artificial Intelligence and Big Data Forum","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.3660414","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3660395.3660414","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T23:34:06Z","timestamp":1755905646000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3660395.3660414"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,22]]},"references-count":9,"alternative-id":["10.1145\/3660395.3660414","10.1145\/3660395"],"URL":"https:\/\/doi.org\/10.1145\/3660395.3660414","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"}}]}}