{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T15:52:13Z","timestamp":1781884333372,"version":"3.54.5"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031982071","type":"print"},{"value":"9783031982088","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,7,9]],"date-time":"2025-07-09T00:00:00Z","timestamp":1752019200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,7,9]],"date-time":"2025-07-09T00:00:00Z","timestamp":1752019200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-031-98208-8_2","type":"book-chapter","created":{"date-parts":[[2025,7,13]],"date-time":"2025-07-13T17:57:03Z","timestamp":1752429423000},"page":"11-29","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Testing-Based Formal Verification with\u00a0Program Slicing on\u00a0Functional Soundness and\u00a0Completeness"],"prefix":"10.1007","author":[{"given":"Ai","family":"Liu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shaoying","family":"Liu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhibin","family":"Yang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,7,9]]},"reference":[{"key":"2_CR1","doi-asserted-by":"publisher","unstructured":"Alqadi, B.S., Maletic, J.I.: Integration of program slicing with cognitive complexity for defect prediction. In: Proceedings of ICSME 2020, Adelaide, Australia, pp. 839\u2013843. IEEE (2020). https:\/\/doi.org\/10.1109\/ICSME46990.2020.00106","DOI":"10.1109\/ICSME46990.2020.00106"},{"key":"2_CR2","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"2_CR3","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2023.105077","volume":"294","author":"Y Feng","year":"2023","unstructured":"Feng, Y., Li, S.: Abstract interpretation, hoare logic, and incorrectness logic for quantum programs. Inf. Comput. 294, 105077 (2023). https:\/\/doi.org\/10.1016\/J.IC.2023.105077","journal-title":"Inf. Comput."},{"key":"2_CR4","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2022.100832","volume":"130","author":"C Galindo","year":"2023","unstructured":"Galindo, C., P\u00e9rez, S., Silva, J.: Exception-sensitive program slicing. J. Log. Algebraic Methods Program. 130, 100832 (2023). https:\/\/doi.org\/10.1016\/j.jlamp.2022.100832","journal-title":"J. Log. Algebraic Methods Program."},{"key":"2_CR5","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2022.100826","volume":"130","author":"C Galindo","year":"2023","unstructured":"Galindo, C., P\u00e9rez, S., Silva, J.: Program slicing of Java programs. J. Log. Algebraic Methods Program. 130, 100826 (2023). https:\/\/doi.org\/10.1016\/j.jlamp.2022.100826","journal-title":"J. Log. Algebraic Methods Program."},{"key":"2_CR6","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/BF00289504","volume":"2","author":"C Hoare","year":"1973","unstructured":"Hoare, C., Wirth, N.: An axiomatic definition of the programming language PASCAL. Acta Informatica 2, 335\u2013355 (1973)","journal-title":"Acta Informatica"},{"key":"2_CR7","doi-asserted-by":"publisher","unstructured":"Jiang, S., Li, W., Li, H., Zhang, Y., Zhang, H., Liu, Y.: Fault localization for null pointer exception based on stack trace and program slicing. In: Proceedings of QSIC 2012, Xi\u2019an, Shaanxi, China, pp. 9\u201312. IEEE (2012). https:\/\/doi.org\/10.1109\/QSIC.2012.36","DOI":"10.1109\/QSIC.2012.36"},{"key":"2_CR8","doi-asserted-by":"publisher","unstructured":"Jiang, S., Zhang, H., Wang, Q., Zhang, Y.: A debugging approach for Java runtime exceptions based on program slicing and stack traces. In: Proceedings of QSIC 2010, Zhangjiajie, China, pp. 393\u2013398. IEEE Computer Society (2010). https:\/\/doi.org\/10.1109\/QSIC.2010.23","DOI":"10.1109\/QSIC.2010.23"},{"issue":"1","key":"2_CR9","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1109\/TSE.2022.3150333","volume":"49","author":"A Liu","year":"2023","unstructured":"Liu, A., Liu, S.: Enhancing the capability of testing-based formal verification by handling operations in software packages. IEEE Trans. Softw. Eng. 49(1), 304\u2013324 (2023). https:\/\/doi.org\/10.1109\/TSE.2022.3150333","journal-title":"IEEE Trans. Softw. Eng."},{"key":"2_CR10","doi-asserted-by":"publisher","unstructured":"Liu, H., Liu, S., Liu, A., Fang, D., Xu, G.: Verifying and improving neural networks using testing-based formal verification. In: Proceedings of SOFL+MSVL 2022, Madrid, Spain. Lecture Notes in Computer Science, vol. 13854, pp. 126\u2013141. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-29476-1_11","DOI":"10.1007\/978-3-031-29476-1_11"},{"issue":"2","key":"2_CR11","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1142\/S0218194023500523","volume":"34","author":"H Liu","year":"2024","unstructured":"Liu, H., Liu, S., Xu, G., Liu, A., Fang, D.: NNTBFV: simplifying and verifying neural networks using testing-based formal verification. Int. J. Softw. Eng. Knowl. Eng. 34(2), 273\u2013300 (2024). https:\/\/doi.org\/10.1142\/S0218194023500523","journal-title":"Int. J. Softw. Eng. Knowl. Eng."},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Liu, S.: 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.\u00a010, pp. 229\u2013238. EasyChair (2012). https:\/\/easychair.org\/publications\/paper\/476","DOI":"10.29007\/fml1"},{"key":"2_CR13","doi-asserted-by":"publisher","unstructured":"Liu, S.: Automatic selection of system functional scenarios for formal specification animation. In: Proceedings of APSEC 2015, New Delhi, India, pp. 72\u201379. IEEE Computer Society (2015). https:\/\/doi.org\/10.1109\/APSEC.2015.15","DOI":"10.1109\/APSEC.2015.15"},{"key":"2_CR14","doi-asserted-by":"publisher","unstructured":"Liu, S.: A tool supported testing method for reducing cost and improving quality. In: Proceedings of QRS 2016, Vienna, Austria, pp. 448\u2013455. IEEE (2016). https:\/\/doi.org\/10.1109\/QRS.2016.56","DOI":"10.1109\/QRS.2016.56"},{"key":"2_CR15","doi-asserted-by":"publisher","unstructured":"Liu, S., Hayashi, T., Takahashi, K., Kimura, K., Nakayama, T., Nakajima, S.: Automatic transformation from formal specifications to functional scenario forms for automatic test case generation. In: Proceedings of the 9th SoMeT_10, Yokohama City, Japan. Frontiers in Artificial Intelligence and Applications, vol.\u00a0217, pp. 383\u2013397. IOS Press (2010). https:\/\/doi.org\/10.3233\/978-1-60750-629-4-383","DOI":"10.3233\/978-1-60750-629-4-383"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-04915-1_1","volume-title":"Structured Object-Oriented Formal Language and Method","author":"S Liu","year":"2014","unstructured":"Liu, S., Nakajima, S.: Combining specification-based testing, correctness proof, and inspection for program verification in practice. In: Liu, S., Duan, Z. (eds.) SOFL+MSVL 2013. LNCS, vol. 8332, pp. 3\u201316. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-04915-1_1"},{"issue":"2","key":"2_CR17","doi-asserted-by":"publisher","first-page":"691","DOI":"10.1109\/TSE.2020.2999884","volume":"48","author":"S Liu","year":"2022","unstructured":"Liu, S., Nakajima, S.: Automatic test case and test oracle generation based on functional scenarios in formal specifications for conformance testing. IEEE Trans. Softw. Eng. 48(2), 691\u2013712 (2022). https:\/\/doi.org\/10.1109\/TSE.2020.2999884","journal-title":"IEEE Trans. Softw. Eng."},{"key":"2_CR18","doi-asserted-by":"publisher","unstructured":"O\u2019Hearn, P.W.: Incorrectness logic. Proc. ACM Program. Lang. 4(POPL), 10:1\u201310:32 (2020). https:\/\/doi.org\/10.1145\/3371078","DOI":"10.1145\/3371078"},{"key":"2_CR19","doi-asserted-by":"publisher","unstructured":"Peled, D.A.: Software Reliability Methods. Texts in Computer Science. Springer, Cham (2001). https:\/\/doi.org\/10.1007\/978-1-4757-3540-6","DOI":"10.1007\/978-1-4757-3540-6"},{"key":"2_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-030-78946-6_5","volume-title":"Graph Transformation","author":"CM Poskitt","year":"2021","unstructured":"Poskitt, C.M.: Incorrectness logic for graph programs. In: Gadducci, F., Kehrer, T. (eds.) ICGT 2021. LNCS, vol. 12741, pp. 81\u2013101. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-78946-6_5"},{"key":"2_CR21","doi-asserted-by":"publisher","unstructured":"Rao, L., Liu, S., Liu, A.: Testing program segments to detect runtime exceptions in Java. In: Proceedings of SOFL+MSVL 2022, Madrid, Spain. Lecture Notes in Computer Science, vol. 13854, pp. 93\u2013105. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-29476-1_8","DOI":"10.1007\/978-3-031-29476-1_8"},{"key":"2_CR22","doi-asserted-by":"publisher","unstructured":"Roggenbach, M., Cerone, A., Schlingloff, B., Schneider, G., Shaikh, S.A.: Formal Methods for Software Engineering - Languages, Methods, Application Domains. Texts in Theoretical Computer Science. An EATCS Series. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-38800-3","DOI":"10.1007\/978-3-030-38800-3"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Schumann, J.: Automated Theorem Proving in Software Engineering. Springer, Cham (2001). http:\/\/www.springer.com\/computer\/swe\/book\/978-3-540-67989-9","DOI":"10.1007\/978-3-662-22646-9"},{"issue":"3","key":"2_CR24","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10664-020-09931-7","volume":"26","author":"E Soremekun","year":"2021","unstructured":"Soremekun, E., Kirschner, L., B\u00f6hme, M., Zeller, A.: Locating faults with program slicing: an empirical analysis. Empir. Softw. Eng. 26(3), 1\u201345 (2021). https:\/\/doi.org\/10.1007\/s10664-020-09931-7","journal-title":"Empir. Softw. Eng."},{"key":"2_CR25","doi-asserted-by":"publisher","unstructured":"Wang, R., Liu, S.: TBFV-SE: testing-based formal verification with symbolic execution. In: Proceedings of QRS 2018, Lisbon, Portugal, pp. 59\u201366. IEEE (2018). https:\/\/doi.org\/10.1109\/QRS.2018.00019","DOI":"10.1109\/QRS.2018.00019"},{"key":"2_CR26","doi-asserted-by":"publisher","unstructured":"Wang, R., Liu, S.: Branch sequence coverage criterion for testing-based formal verification with symbolic execution. In: Proceedings of QRS Companion 2019, Sofia, Bulgaria, pp. 205\u2013212. IEEE (2019). https:\/\/doi.org\/10.1109\/QRS-C.2019.00049","DOI":"10.1109\/QRS-C.2019.00049"},{"key":"2_CR27","doi-asserted-by":"publisher","unstructured":"Wang, R., Liu, S., Sato, Y.: A fault localization approach derived from testing-based formal verification. In: Proceedings of ICECCS 2020, Singapore, pp. 165\u2013170. IEEE (2020). https:\/\/doi.org\/10.1109\/ICECCS51672.2020.00026","DOI":"10.1109\/ICECCS51672.2020.00026"},{"issue":"4","key":"2_CR28","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1109\/TSE.1984.5010248","volume":"10","author":"MD Weiser","year":"1984","unstructured":"Weiser, M.D.: Program slicing. IEEE Trans. Softw. Eng. 10(4), 352\u2013357 (1984). https:\/\/doi.org\/10.1109\/TSE.1984.5010248","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"OOPSLA1","key":"2_CR29","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3527316","volume":"6","author":"P Yan","year":"2022","unstructured":"Yan, P., Jiang, H., Yu, N.: On incorrectness logic for quantum programs. Proc. ACM Program. Lang. 6(OOPSLA1), 1\u201328 (2022). https:\/\/doi.org\/10.1145\/3527316","journal-title":"Proc. ACM Program. Lang."},{"key":"2_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-030-13651-2_5","volume-title":"Structured Object-Oriented Formal Language and Method","author":"Y Yin","year":"2019","unstructured":"Yin, Y., Liu, S., Chen, Y.: Verification of SysML activity diagrams using Hoare logic and SOFL. In: Duan, Z., Liu, S., Tian, C., Nagoya, F. (eds.) SOFL+MSVL 2018. LNCS, vol. 11392, pp. 71\u201388. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-13651-2_5"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98208-8_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T08:38:09Z","timestamp":1777538289000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98208-8_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,7,9]]},"ISBN":["9783031982071","9783031982088"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98208-8_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,7,9]]},"assertion":[{"value":"9 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Theoretical Aspects of Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Limassol","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Cyprus","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tase2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cyprusconferences.org\/tase2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}