{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,25]],"date-time":"2026-02-25T17:50:48Z","timestamp":1772041848967,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":18,"publisher":"ACM","license":[{"start":{"date-parts":[[2025,6,11]],"date-time":"2025-06-11T00:00:00Z","timestamp":1749600000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-sa\/4.0\/"}],"funder":[{"name":"Joint Fund of the National Natural Science Foundation of China","award":["No. U2241216"],"award-info":[{"award-number":["No. U2241216"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,6,25]]},"DOI":"10.1145\/3713081.3731740","type":"proceedings-article","created":{"date-parts":[[2025,6,6]],"date-time":"2025-06-06T17:20:36Z","timestamp":1749230436000},"page":"66-70","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["TBFV4J: An Automated Testing-Based Formal Verification Tool for Java"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8222-2157","authenticated-orcid":false,"given":"Ai","family":"Liu","sequence":"first","affiliation":[{"name":"College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing, Jiangsu, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-2624-8324","authenticated-orcid":false,"given":"Yang","family":"Liu","sequence":"additional","affiliation":[{"name":"College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing, Jiangsu, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6748-5052","authenticated-orcid":false,"given":"Shaoying","family":"Liu","sequence":"additional","affiliation":[{"name":"Software Engineering Institute, East China Normal University, Shanghai, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,6,11]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-74234-7"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.22152\/PROGRAMMING-JOURNAL.ORG\/2021\/5\/13"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3159450.3159575"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606754"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30826-0_4"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2022.3150333"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-29476-1_11"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0218194023500523"},{"key":"e_1_3_2_1_11_1","volume-title":"Turing-100 - The Alan Turing Centenary","author":"Liu Shaoying","unstructured":"Shaoying Liu. 2012. Utilizing Hoare Logic to Strengthen Testing for Error Detection in Programs. In Turing-100 - The Alan Turing Centenary, Manchester, UK (EPiC Series in Computing, Vol. 10). EasyChair, 229\u2013238. https:\/\/easychair.org\/publications\/paper\/476"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-04915-1_1"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2020.2999884"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132748"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-71162-6"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3573074.3573080"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36946-9_14"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.JSS.2024.112242"}],"event":{"name":"ISSTA Companion '25: 34th ACM SIGSOFT International Symposium on Software Testing and Analysis","location":"Clarion Hotel Trondheim Trondheim Norway","acronym":"ISSTA Companion '25","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 34th ACM SIGSOFT International Symposium on Software Testing and Analysis"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3713081.3731740","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:18:09Z","timestamp":1750295889000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3713081.3731740"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,11]]},"references-count":18,"alternative-id":["10.1145\/3713081.3731740","10.1145\/3713081"],"URL":"https:\/\/doi.org\/10.1145\/3713081.3731740","relation":{},"subject":[],"published":{"date-parts":[[2025,6,11]]},"assertion":[{"value":"2025-06-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}