{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T16:15:01Z","timestamp":1742919301182,"version":"3.40.3"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031661488"},{"type":"electronic","value":"9783031661495"}],"license":[{"start":{"date-parts":[[2024,10,13]],"date-time":"2024-10-13T00:00:00Z","timestamp":1728777600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,10,13]],"date-time":"2024-10-13T00:00:00Z","timestamp":1728777600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>When verifiers report an alarm, they export a violation witness (exchangeable counterexample) that helps validate the reachability of that alarm. Conventional wisdom says that this violation witness should be very precise: the ideal witness describes a single error\u00a0path for the validator to check. But we claim that verifiers overshoot and produce large witnesses with information that makes validation unnecessarily difficult. To check our hypothesis, we reduce violation witnesses to that information that automated fault-localization approaches deem relevant for triggering the reported\u00a0alarm in the program. We perform a large experimental evaluation on the witnesses produced in\u00a0the International Competition on Software Verification (SV-COMP 2023). It shows that our reduction shrinks the witnesses considerably and enables the confirmation of verification results that were not confirmable before.<\/jats:p>","DOI":"10.1007\/978-3-031-66149-5_12","type":"book-chapter","created":{"date-parts":[[2024,10,12]],"date-time":"2024-10-12T07:01:54Z","timestamp":1728716514000},"page":"205-224","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Fault Localization on Verification Witnesses"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4832-7662","authenticated-orcid":false,"given":"Dirk","family":"Beyer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7365-5030","authenticated-orcid":false,"given":"Matthias","family":"Kettl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0291-815X","authenticated-orcid":false,"given":"Thomas","family":"Lemberger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,10,13]]},"reference":[{"key":"12_CR1","doi-asserted-by":"publisher","unstructured":"Abreu, R., Zoeteweij, P., Golsteijn, R., van Gemund, A.J.C.: A practical evaluation of spectrum-based fault localization. J. Syst. Softw. 82(11), 1780\u20131792 (2009). https:\/\/doi.org\/10.1016\/j.jss.2009.06.035","DOI":"10.1016\/j.jss.2009.06.035"},{"key":"12_CR2","doi-asserted-by":"publisher","unstructured":"Ayaziov\u00e1, P., Strejcek, J.: Symbiotic-Witch 2: More efficient algorithm and witness refutation (competition contribution). In: Proc. TACAS\u00a0(2). pp. 523\u2013528. LNCS\u00a013994, Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_30","DOI":"10.1007\/978-3-031-30820-8_30"},{"key":"12_CR3","doi-asserted-by":"publisher","unstructured":"Beyer, D.: A data set of program invariants and error paths. In: Proc. MSR. pp. 111\u2013115. IEEE (2019). https:\/\/doi.org\/10.1109\/MSR.2019.00026","DOI":"10.1109\/MSR.2019.00026"},{"key":"12_CR4","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Competition on software verification and witness validation: SV-COMP 2023. In: Proc. TACAS\u00a0(2). pp. 495\u2013522. LNCS\u00a013994, Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_29","DOI":"10.1007\/978-3-031-30820-8_29"},{"key":"12_CR5","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Verification witnesses from verification tools (SV-COMP\u00a02023). Zenodo (2023). https:\/\/doi.org\/10.5281\/zenodo.7627791","DOI":"10.5281\/zenodo.7627791"},{"key":"12_CR6","doi-asserted-by":"publisher","unstructured":"Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumdar, R.: Generating tests from counterexamples. In: Proc. ICSE. pp. 326\u2013335. IEEE (2004). https:\/\/doi.org\/10.1109\/ICSE.2004.1317455","DOI":"10.1109\/ICSE.2004.1317455"},{"key":"12_CR7","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M., Lemberger, T., Tautschnig, M.: Verification witnesses. ACM Trans. Softw. Eng. Methodol. 31(4), 57:1\u201357:69 (2022). https:\/\/doi.org\/10.1145\/3477579","DOI":"10.1145\/3477579"},{"key":"12_CR8","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M., Stahlbauer, A.: Witness validation and stepwise testification across software verifiers. In: Proc. FSE. pp. 721\u2013733. ACM (2015). https:\/\/doi.org\/10.1145\/2786805.2786867","DOI":"10.1145\/2786805.2786867"},{"key":"12_CR9","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Lemberger, T., Tautschnig, M.: Tests from witnesses: Execution-based validation of verification results. In: Proc. TAP. pp. 3\u201323. LNCS\u00a010889, Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-92994-1_1","DOI":"10.1007\/978-3-319-92994-1_1"},{"key":"12_CR10","doi-asserted-by":"publisher","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: A tool for configurable software verification. In: Proc. CAV. pp. 184\u2013190. LNCS\u00a06806, Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"12_CR11","doi-asserted-by":"publisher","unstructured":"Beyer, D., Kettl, M., Lemberger, T.: Reproduction package for article \u2018Fault localization on witnesses\u2019. Zenodo (2024). https:\/\/doi.org\/10.5281\/zenodo.10952383","DOI":"10.5281\/zenodo.10952383"},{"key":"12_CR12","doi-asserted-by":"publisher","unstructured":"Beyer, D., L\u00f6we, S., Wendler, P.: Reliable benchmarking: Requirements and solutions. Int. J. Softw. Tools Technol. Transfer 21(1), 1\u201329 (2019). https:\/\/doi.org\/10.1007\/s10009-017-0469-y","DOI":"10.1007\/s10009-017-0469-y"},{"key":"12_CR13","doi-asserted-by":"publisher","unstructured":"Beyer, D., Spiessl, M.: MetaVal: Witness validation via verification. In: Proc. CAV. pp. 165\u2013177. LNCS\u00a012225, Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_10","DOI":"10.1007\/978-3-030-53291-8_10"},{"key":"12_CR14","unstructured":"Beyer, D., Kettl, M., Lemberger, T.: Flow: Fault localization on witnesses. https:\/\/gitlab.com\/sosy-lab\/software\/fault-localization-on-witnesses (2023), [Online; accessed 22-January-2024]"},{"key":"12_CR15","doi-asserted-by":"publisher","unstructured":"Beyer, D., Kettl, M., Lemberger, T.: Fault localization on verification witnesses (poster paper). In: Proc. ICSE. ACM (2024). https:\/\/doi.org\/10.1145\/3639478.3643099","DOI":"10.1145\/3639478.3643099"},{"key":"12_CR16","doi-asserted-by":"publisher","unstructured":"Brandes, U., Eiglsperger, M., Herman, I., Himsolt, M., Marshall, M.S.: GraphML progress report. In: Graph Drawing. pp. 501\u2013512. LNCS\u00a02265, Springer (2001). https:\/\/doi.org\/10.1007\/3-540-45848-4_59","DOI":"10.1007\/3-540-45848-4_59"},{"key":"12_CR17","doi-asserted-by":"publisher","unstructured":"Chalupa, M., Henzinger, T.: Bubaak: Runtime monitoring of program verifiers (competition contribution). In: Proc. TACAS\u00a0(2). pp. 535\u2013540. LNCS\u00a013994, Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_32","DOI":"10.1007\/978-3-031-30820-8_32"},{"key":"12_CR18","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Proc. TACAS. pp. 93\u2013107. LNCS\u00a07795, Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7","DOI":"10.1007\/978-3-642-36742-7_7"},{"key":"12_CR19","doi-asserted-by":"publisher","unstructured":"Ermis, E., Sch\u00e4f, M., Wies, T.: Error invariants. In: Proc. FM. pp. 187\u2013201. LNCS\u00a07436, Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_17","DOI":"10.1007\/978-3-642-32759-9_17"},{"key":"12_CR20","doi-asserted-by":"publisher","unstructured":"Ernst, G., Blau, J., Murray, T.: Deductive verification via the debug adapter protocol. In: Proen\u00e7a, J., Paskevich, A. (eds.) Proceedings of the 6th Workshop on Formal Integrated Development Environment, F-IDE@NFM 2021, Held online, 24-25th May 2021. EPTCS, vol.\u00a0338, pp. 89\u201396 (2021). https:\/\/doi.org\/10.4204\/EPTCS.338.11","DOI":"10.4204\/EPTCS.338.11"},{"key":"12_CR21","doi-asserted-by":"publisher","unstructured":"Gadelha, M.Y., Ismail, H.I., Cordeiro, L.C.: Handling loops in bounded model checking of C programs via k-induction. Int. J. Softw. Tools Technol. Transf. 19(1), 97\u2013114 (February 2017). https:\/\/doi.org\/10.1007\/s10009-015-0407-9","DOI":"10.1007\/s10009-015-0407-9"},{"key":"12_CR22","doi-asserted-by":"publisher","unstructured":"Gennari, J., Gurfinkel, A., Kahsai, T., Navas, J.A., Schwartz, E.J.: Executable counterexamples in software model checking. In: Proc. VSTTE. pp. 17\u201337. LNCS\u00a011294, Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-03592-1_2","DOI":"10.1007\/978-3-030-03592-1_2"},{"key":"12_CR23","doi-asserted-by":"publisher","unstructured":"Groce, A., Visser, W.: What went wrong: Explaining counterexamples. In: Proc. SPIN. pp. 121\u2013135. LNCS\u00a02648, Springer (2003). https:\/\/doi.org\/10.1007\/3-540-44829-2_8","DOI":"10.1007\/3-540-44829-2_8"},{"key":"12_CR24","doi-asserted-by":"publisher","unstructured":"Heizmann, M., Barth, M., Dietsch, D., Fichtner, L., Hoenicke, J., Klumpp, D., Naouar, M., Schindler, T., Sch\u00fcssele, F., Podelski, A.: Ultimate Automizer 2023 (competition contribution). In: Proc. TACAS\u00a0(2). pp. 577\u2013581. LNCS\u00a013994, Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_39","DOI":"10.1007\/978-3-031-30820-8_39"},{"key":"12_CR25","doi-asserted-by":"publisher","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Proc. CAV. pp. 36\u201352. LNCS\u00a08044, Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_2","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"12_CR26","doi-asserted-by":"publisher","unstructured":"Jhala, R., Majumdar, R.: Path slicing. In: Proc. PLDI. pp. 38\u201347. ACM (2005). https:\/\/doi.org\/10.1145\/1065010.1065016","DOI":"10.1145\/1065010.1065016"},{"key":"12_CR27","doi-asserted-by":"publisher","unstructured":"Jones, J.A., Harrold, M.J.: Empirical evaluation of the Tarantula automatic fault-localization technique. In: Proc. ASE. pp. 273\u2013282. ACM (2005). https:\/\/doi.org\/10.1145\/1101908.1101949","DOI":"10.1145\/1101908.1101949"},{"key":"12_CR28","doi-asserted-by":"publisher","unstructured":"Jose, M., Majumdar, R.: Bug-assist: Assisting fault localization in ANSI-C programs. In: Proc. CAV. pp. 504\u2013509. LNCS\u00a06806, Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_40","DOI":"10.1007\/978-3-642-22110-1_40"},{"key":"12_CR29","doi-asserted-by":"publisher","unstructured":"Jose, M., Majumdar, R.: Cause clue clauses: Error localization using maximum satisfiability. In: Proc. PLDI. pp. 437\u2013446. ACM (2011). https:\/\/doi.org\/10.1145\/1993498.1993550","DOI":"10.1145\/1993498.1993550"},{"key":"12_CR30","doi-asserted-by":"publisher","unstructured":"K\u00f6lbl, M., Leue, S., Wies, T.: Tartar: A timed automata repair tool. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification. pp. 529\u2013540. Springer International Publishing, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_25","DOI":"10.1007\/978-3-030-53288-8_25"},{"key":"12_CR31","doi-asserted-by":"publisher","unstructured":"Metta, R., Yeduru, P., Karmarkar, H., Medicherla, R.K.: VeriFuzz 1.4: Checking for (non-)termination (competition contribution). In: Proc. TACAS\u00a0(2). pp. 594\u2013599. LNCS\u00a013994, Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_42","DOI":"10.1007\/978-3-031-30820-8_42"},{"key":"12_CR32","doi-asserted-by":"publisher","unstructured":"Monat, R., Ouadjaout, A., Min\u00e9, A.: Mopsa-C: Modular domains and relational abstract interpretation for C programs (competition contribution). In: Proc. TACAS\u00a0(2). pp. 565\u2013570. LNCS\u00a013994, Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_37","DOI":"10.1007\/978-3-031-30820-8_37"},{"key":"12_CR33","doi-asserted-by":"publisher","unstructured":"M\u00fcller, P., Ruskiewicz, J.N.: Using debuggers to understand failed verification attempts. In: Proc. FM. pp. 73\u201387. LNCS\u00a06664, Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_8","DOI":"10.1007\/978-3-642-21437-0_8"},{"key":"12_CR34","doi-asserted-by":"publisher","unstructured":"Richter, C., H\u00fcllermeier, E., Jakobs, M.C., Wehrheim, H.: Algorithm selection for software validation based on graph kernels. Autom. Softw. Eng. 27(1), 153\u2013186 (2020). https:\/\/doi.org\/10.1007\/s10515-020-00270-x","DOI":"10.1007\/s10515-020-00270-x"},{"key":"12_CR35","doi-asserted-by":"publisher","unstructured":"Richter, C., Wehrheim, H.: PeSCo: Predicting sequential combinations of verifiers (competition contribution). In: Proc. TACAS\u00a0(3). pp. 229\u2013233. LNCS\u00a011429, Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_19","DOI":"10.1007\/978-3-030-17502-3_19"},{"key":"12_CR36","doi-asserted-by":"publisher","unstructured":"Rockai, P., Barnat, J.: DivSIM, an interactive simulator for LLVM bitcode. STTT 24(3), 493\u2013510 (2022). https:\/\/doi.org\/10.1007\/s10009-022-00659-x","DOI":"10.1007\/s10009-022-00659-x"},{"key":"12_CR37","doi-asserted-by":"publisher","unstructured":"Saan, S., Schwarz, M., Erhard, J., Pietsch, M., Seidl, H., Tilscher, S., Vojdani, V.: Goblint: Autotuning thread-modular abstract interpretation (competition contribution). In: Proc. TACAS\u00a0(2). pp. 547\u2013552. LNCS\u00a013994, Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_34","DOI":"10.1007\/978-3-031-30820-8_34"},{"key":"12_CR38","doi-asserted-by":"publisher","unstructured":"Wong, W.E., Debroy, V., Gao, R., Li, Y.: The DStar method for effective software fault localization. IEEE Trans. Reliab. 63(1), 290\u2013308 (2014). https:\/\/doi.org\/10.1109\/TR.2013.2285319","DOI":"10.1109\/TR.2013.2285319"},{"key":"12_CR39","doi-asserted-by":"publisher","unstructured":"\u00c1d\u00e1m, Z., Bajczi, L., Dobos-Kov\u00e1cs, M., Hajdu, A., Moln\u00e1r, V.: Theta: Portfolio of cegar-based analyses with dynamic algorithm selection (competition contribution). In: Proc. TACAS\u00a0(2). pp. 474\u2013478. LNCS\u00a013244, Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_34","DOI":"10.1007\/978-3-030-99527-0_34"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-66149-5_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,12]],"date-time":"2024-10-12T07:07:17Z","timestamp":1728716837000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-66149-5_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,13]]},"ISBN":["9783031661488","9783031661495"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-66149-5_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,10,13]]},"assertion":[{"value":"13 October 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This project was funded in part by the Deutsche Forschungsgemeinschaft (DFG) \u2013  (),  (Coop), and  (IdeFix).","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Funding Statement"}},{"value":"SPIN","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Model Checking Software","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"spin2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/spin-web.github.io\/SPIN2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}