{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:25:04Z","timestamp":1779074704632,"version":"3.51.4"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031661488","type":"print"},{"value":"9783031661495","type":"electronic"}],"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>Verification witnesses are now widely accepted objects used not only to confirm or refute verification results, but also for general exchange of information among various tools for program verification. The original format for witnesses is based on GraphML, and it has some known issues including a semantics based on control-flow automata, limited tool support of some format features, and a large size of witness files. This paper presents version 2.0 of the witness format, which is based on YAML and overcomes the above-mentioned issues. We describe the new format, provide an experimental comparison of various aspects of the original and the new witness format showing that both witness formats perform similarly, and report on its adoption in the community.<\/jats:p>","DOI":"10.1007\/978-3-031-66149-5_11","type":"book-chapter","created":{"date-parts":[[2024,10,12]],"date-time":"2024-10-12T07:01:54Z","timestamp":1728716514000},"page":"184-203","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["Software Verification Witnesses 2.0"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1072-8137","authenticated-orcid":false,"given":"Paul\u00edna","family":"Ayaziov\u00e1","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4832-7662","authenticated-orcid":false,"given":"Dirk","family":"Beyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8172-3184","authenticated-orcid":false,"given":"Marian","family":"Lingsch-Rosenfeld","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9169-9130","authenticated-orcid":false,"given":"Martin","family":"Spiessl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5873-403X","authenticated-orcid":false,"given":"Jan","family":"Strej\u010dek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,10,13]]},"reference":[{"key":"11_CR1","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":"11_CR2","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M., Dietsch, D., Heizmann, M.: Correctness witnesses: Exchanging verification results between verifiers. In: Proc. FSE. pp. 326\u2013337. ACM (2016). https:\/\/doi.org\/10.1145\/2950290.2950351","DOI":"10.1145\/2950290.2950351"},{"key":"11_CR3","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Software verification and verifiable witnesses (Report on SV-COMP 2015). In: Proc. TACAS. pp. 401\u2013416. LNCS\u00a09035, Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_31","DOI":"10.1007\/978-3-662-46681-0_31"},{"key":"11_CR4","doi-asserted-by":"publisher","unstructured":"Beyer, D., Strej\u010dek, J.: Case study on verification-witness validators: Where we are and where we go. In: Proc. SAS. pp. 160\u2013174. LNCS\u00a013790, Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-22308-2_8","DOI":"10.1007\/978-3-031-22308-2_8"},{"key":"11_CR5","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":"11_CR6","doi-asserted-by":"publisher","unstructured":"Beyer, D., Wehrheim, H.: Verification artifacts in cooperative verification: Survey and unifying component framework. In: Proc. ISoLA\u00a0(1). pp. 143\u2013167. LNCS\u00a012476, Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_8","DOI":"10.1007\/978-3-030-61362-4_8"},{"key":"11_CR7","doi-asserted-by":"publisher","unstructured":"Beyer, D., Haltermann, J., Lemberger, T., Wehrheim, H.: Decomposing Software Verification into Off-the-Shelf Components: An Application to CEGAR. In: Proc. ICSE. pp. 536\u2013548. ACM (2022). https:\/\/doi.org\/10.1145\/3510003.3510064","DOI":"10.1145\/3510003.3510064"},{"key":"11_CR8","doi-asserted-by":"publisher","unstructured":"Beyer, D., Dangl, M.: Verification-aided debugging: An interactive web-service for exploring error witnesses. In: Proc. CAV\u00a0(2). pp. 502\u2013509. LNCS\u00a09780, Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_28","DOI":"10.1007\/978-3-319-41540-6_28"},{"key":"11_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":"11_CR10","doi-asserted-by":"publisher","unstructured":"Beyer, D., Spiessl, M., Umbricht, S.: Cooperation between automatic and interactive software verifiers. In: Proc. SEFM. p. 111\u2013128. LNCS\u00a013550, Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-17108-6_7","DOI":"10.1007\/978-3-031-17108-6_7"},{"key":"11_CR11","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":"11_CR12","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":"11_CR13","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":"11_CR14","doi-asserted-by":"publisher","unstructured":"Chalupa, M., \u0158echt\u00e1\u010dkov\u00e1, A., Mihalkovi\u010d, V., Zaoral, L., Strej\u010dek, J.: Symbiotic\u00a09: String analysis and backward symbolic execution with loop folding (competition contribution). In: Proc. TACAS\u00a0(2). pp. 462\u2013467. LNCS\u00a013244, Springer (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_32","DOI":"10.1007\/978-3-030-99527-0_32"},{"key":"11_CR15","doi-asserted-by":"publisher","unstructured":"Ayaziov\u00e1, P., Strej\u010dek, 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"},{"issue":"2","key":"11_CR16","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/j.cosrev.2010.09.009","volume":"5","author":"RM McConnell","year":"2011","unstructured":"McConnell, R.M., Mehlhorn, K., N\u00e4her, S., Schweitzer, P.: Certifying algorithms. Computer Science Review 5(2), 119\u2013161 (2011). https:\/\/doi.org\/10.1016\/j.cosrev.2010.09.009","journal-title":"Computer Science Review"},{"key":"11_CR17","unstructured":"Turing, A.: Checking a large routine. In: Report on a Conference on High Speed Automatic Calculating Machines. pp. 67\u201369. Cambridge Univ. Math. Lab. (1949), https:\/\/turingarchive.kings.cam.ac.uk\/publications-lectures-and-talks-amtb\/amt-b-8"},{"key":"11_CR18","doi-asserted-by":"publisher","unstructured":"Giesl, J., Mesnard, F., Rubio, A., Thiemann, R., Waldmann, J.: Termination competition (termCOMP 2015). In: Proc. CADE. pp. 105\u2013108. LNCS\u00a09195, Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_6","DOI":"10.1007\/978-3-319-21401-6_6"},{"key":"11_CR19","doi-asserted-by":"publisher","unstructured":"Sternagel, C., Thiemann, R.: The certification problem format. In: Proc. UITP. pp. 61\u201372. EPTCS\u00a0167, EPTCS (2014). https:\/\/doi.org\/10.4204\/EPTCS.167.8","DOI":"10.4204\/EPTCS.167.8"},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"J\u00e4rvisalo, M., Berre, D.L., Roussel, O., Simon, L.: The international SAT solver competitions. AI Magazine 33(1) (2012)","DOI":"10.1609\/aimag.v33i1.2395"},{"key":"11_CR21","unstructured":"Heule, M.J.H.: The DRAT format and drat-trim checker. CoRR 1610(06229) (October 2016)"},{"key":"11_CR22","doi-asserted-by":"publisher","unstructured":"Wetzler, N., Heule, M.J.H., Jr., W.A.H.: Drat-trim: Efficient checking and trimming using expressive clausal proofs. In: Proc. SAT. pp. 422\u2013429. LNCS\u00a08561, Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_31","DOI":"10.1007\/978-3-319-09284-3_31"},{"key":"11_CR23","unstructured":"Bury, G., Bobot, F.: Verifying models with Dolmen. In: Proc. SMT Workshop. CEUR Workshop Proceedings, CEUR (2023)"},{"key":"11_CR24","doi-asserted-by":"publisher","unstructured":"Casta\u00f1o, R., Braberman, V.A., Garbervetsky, D., Uchitel, S.: Model checker execution reports. In: Proc. ASE, pp. 200\u2013205. IEEE (2017). https:\/\/doi.org\/10.1109\/ASE.2017.8115633","DOI":"10.1109\/ASE.2017.8115633"},{"key":"11_CR25","unstructured":"OASIS: Static analysis results interchange format (sarif) version 2.0 (2019)"},{"key":"11_CR26","unstructured":"Baudin, P., Cuoq, P., Filli\u00e2tre, J.C., March\u00e9, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI\/ISO C specification language version 1.17 (2021), available at https:\/\/frama-c.com\/download\/acsl-1.17.pdf"},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"Baier, D., Beyer, D., Chien, P.C., Jankola, M., Kettl, M., Lee, N.Z., Lemberger, T., Lingsch-Rosenfeld, M., Spiessl, M., Wachowitz, H., Wendler, P.: CPAchecker 2.3 with strategy selection (competition contribution). In: Proc. TACAS. LNCS\u00a0, Springer (2024)","DOI":"10.1007\/978-3-031-57256-2_21"},{"key":"11_CR28","doi-asserted-by":"crossref","unstructured":"Jon\u00e1\u0161, M., Kumor, K., Nov\u00e1k, J., Sedl\u00e1\u010dek, J., Trt\u00edk, M., Zaoral, L., Ayaziov\u00e1, P., Strej\u010dek, J.: Symbiotic 10: Lazy memory initialization and compact symbolic execution (competition contribution). In: Proc. TACAS. LNCS\u00a0, Springer (2024)","DOI":"10.1007\/978-3-031-57256-2_29"},{"key":"11_CR29","doi-asserted-by":"crossref","unstructured":"Ayaziov\u00e1, P., Strej\u010dek, J.: Witch 3: Validation of violation witnesses in the witness format\u00a02.0 (competition contribution). In: Proc. TACAS. LNCS\u00a0, Springer (2024)","DOI":"10.1007\/978-3-031-57256-2_18"},{"key":"11_CR30","unstructured":"Heizmann, M., Bentele, M., Dietsch, D., Jiang, X., Klumpp, D., Sch\u00fcssele, F., Podelski, A.: Ultimate automizer and the abstraction of bitwise operations (competition contribution). In: Proc. TACAS. LNCS\u00a0, Springer (2024)"},{"key":"11_CR31","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.10669737","author":"D Beyer","year":"2024","unstructured":"Beyer, D.: Verification witnesses from verification tools (SV-COMP 2024). Zenodo (2024). https:\/\/doi.org\/10.5281\/zenodo.10669737","journal-title":"Zenodo"},{"key":"11_CR32","doi-asserted-by":"crossref","unstructured":"Beyer, D.: State of the art in software verification and witness validation: SV-COMP 2024. In: Proc. TACAS. LNCS\u00a0, Springer (2024)","DOI":"10.1007\/978-3-031-57256-2_15"},{"issue":"1","key":"11_CR33","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10009-017-0469-y","volume":"21","author":"D Beyer","year":"2019","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","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"11_CR34","doi-asserted-by":"publisher","unstructured":"Ayaziov\u00e1, P., Beyer, D., Lingsch-Rosenfeld, M., Spiessl, M., Strej\u010dek, J.: Reproduction package for SPIN\u00a02024 article \u2018Software verification witnesses\u00a02.0\u2019. Zenodo (2024). https:\/\/doi.org\/10.5281\/zenodo.10826204","DOI":"10.5281\/zenodo.10826204"}],"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_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,12]],"date-time":"2024-10-12T07:07:10Z","timestamp":1728716830000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-66149-5_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,13]]},"ISBN":["9783031661488","9783031661495"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-66149-5_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"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":"P.\u00a0Ayaziov\u00e1 and J.\u00a0Strej\u010dek were supported by the Czech Science Foundation grant GA23-06506S. D.\u00a0Beyer, M.\u00a0Lingsch-Rosenfeld, and M.\u00a0Spiessl were supported by the Deutsche Forschungsgemeinschaft (DFG) \u2013  (ConVeY) 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"}}]}}