{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:58:27Z","timestamp":1782867507170,"version":"3.54.5"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227485","type":"print"},{"value":"9783032227492","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"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]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    <jats:sc>goblitch<\/jats:sc>\n                    is a new verification toolchain for reachability safety\u00a0that combines the abstract interpreter\n                    <jats:sc>Goblint<\/jats:sc>\n                    with the witness validator\n                    <jats:sc>Witch<\/jats:sc>\n                    .\n                    <jats:sc>goblitch<\/jats:sc>\n                    integrates these two tools in a refinement loop\u00a0where\n                    <jats:sc>Goblint<\/jats:sc>\n                    repeatedly builds an abstract reachability graph and\n                    <jats:sc>Witch<\/jats:sc>\n                    decides whether an error path in the current graph corresponds to\u00a0any real program execution. Experiments show that\n                    <jats:sc>goblitch<\/jats:sc>\n                    produces many  results and no incorrect results. Moreover, in the category\n                    <jats:italic>C.ReachSafety<\/jats:italic>\n                    , it produces more  results\u00a0than\n                    <jats:sc>Goblint<\/jats:sc>\n                    .\n                  <\/jats:p>","DOI":"10.1007\/978-3-032-22749-2_27","type":"book-chapter","created":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T13:11:41Z","timestamp":1776258701000},"page":"523-529","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Goblitch: Combining Abstract Interpretation with Symbolic Execution via Witnesses"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-3725-4131","authenticated-orcid":false,"given":"Karoliine","family":"Holter","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1072-8137","authenticated-orcid":false,"given":"Paul\u00edna","family":"Ayaziov\u00e1","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4553-1350","authenticated-orcid":false,"given":"Simmo","family":"Saan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5873-403X","authenticated-orcid":false,"given":"Jan","family":"Strej\u010dek","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4336-7980","authenticated-orcid":false,"given":"Vesal","family":"Vojdani","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,4,15]]},"reference":[{"key":"27_CR1","doi-asserted-by":"publisher","unstructured":"Ayaziov\u00e1, P., Beyer, D., Rosenfeld, M.L., Spiessl, M., Strej\u010dek, J.: Software verification witnesses 2.0. In: Neele, T., Wijs, A. (eds.) Model Checking Software - 30th International Symposium, SPIN 2024, Luxembourg City, Luxembourg, April 8-9, 2024, Proceedings, Lecture Notes in Computer Science, vol. 14624, pp. 184\u2013203, Springer (2024), https:\/\/doi.org\/10.1007\/978-3-031-66149-5_11","DOI":"10.1007\/978-3-031-66149-5_11"},{"key":"27_CR2","doi-asserted-by":"publisher","unstructured":"Ayaziov\u00e1, P., Strej\u010dek, J.: Witch 3: Validation of violation witnesses in the witness format 2.0 (competition contribution). In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part III, Lecture Notes in Computer Science, vol. 14572, pp. 341\u2013346, Springer (2024), https:\/\/doi.org\/10.1007\/978-3-031-57256-2_18","DOI":"10.1007\/978-3-031-57256-2_18"},{"key":"27_CR3","doi-asserted-by":"crossref","unstructured":"Ayaziov\u00e1, P., Jon\u00e1\u0161, M., Mihalkovi\u010d, V., Sedl\u00e1\u010dek, J., Strej\u010dek, J.: Symbiotic 11: Predicate abstraction joins the party (competition contribution). In: Proc. TACAS\u00a0(2), Lecture Notes in Computer Science, vol. 16506, Springer (2026)","DOI":"10.1007\/978-3-032-22749-2_36"},{"key":"27_CR4","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: 44th IEEE\/ACM 44th International Conference on Software Engineering, ICSE 2022, Pittsburgh, PA, USA, May 25-27, 2022, pp. 536\u2013548, ACM (2022),https:\/\/doi.org\/10.1145\/3510003.3510064","DOI":"10.1145\/3510003.3510064"},{"key":"27_CR5","doi-asserted-by":"crossref","unstructured":"Beyer, D., Strej\u010dek, J.: Evaluating software verifiers for C, Java, and SV-LIB (report on SV-COMP 2026). In: Proc. TACAS\u00a0(2), Lecture Notes in Computer Science, vol. 16506, Springer (2026)","DOI":"10.1007\/978-3-032-22749-2_23"},{"key":"27_CR6","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Draves, R., van Renesse, R. (eds.) 8th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2008, December 8-10, 2008, San Diego, California, USA, Proceedings, pp. 209\u2013224, USENIX Association (2008), http:\/\/www.usenix.org\/events\/osdi08\/tech\/full_papers\/cadar\/cadar.pdf"},{"key":"27_CR7","doi-asserted-by":"publisher","unstructured":"Holter, K., Ayaziov\u00e1, P., Saan, S.: Goblitch in SV-COMP 2026 (Nov 2025),https:\/\/doi.org\/10.5281\/zenodo.17661717","DOI":"10.5281\/zenodo.17661717"},{"key":"27_CR8","doi-asserted-by":"publisher","unstructured":"Holter, K., Hennoste, J.O., Lam, P., Saan, S., Vojdani, V.: Abstract debuggers: Exploring program behaviors using static analysis results. In: Edwards, J., Taeumel, M. (eds.) Proceedings of the 2024 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, Onward! 2024, Pasadena, CA, USA, October 23-25, 2024, pp. 130\u2013146, ACM (2024), https:\/\/doi.org\/10.1145\/3689492.3690053","DOI":"10.1145\/3689492.3690053"},{"key":"27_CR9","doi-asserted-by":"publisher","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: A library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings, Lecture Notes in Computer Science, vol. 5643, pp. 661\u2013667, Springer (2009), https:\/\/doi.org\/10.1007\/978-3-642-02658-4_52","DOI":"10.1007\/978-3-642-02658-4_52"},{"key":"27_CR10","doi-asserted-by":"publisher","unstructured":"Junker, M., Huuck, R., Fehnker, A., Knapp, A.: SMT-based false positive elimination in static program analysis. In: Aoki, T., Taguchi, K. (eds.) Formal Methods and Software Engineering - 14th International Conference on Formal Engineering Methods, ICFEM 2012, Kyoto, Japan, November 12-16, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7635, pp. 316\u2013331, Springer (2012), https:\/\/doi.org\/10.1007\/978-3-642-34281-3_23","DOI":"10.1007\/978-3-642-34281-3_23"},{"key":"27_CR11","doi-asserted-by":"publisher","unstructured":"Lattner, C., Adve, V.S.: LLVM: A compilation framework for lifelong program analysis & transformation. In: 2nd IEEE \/ ACM International Symposium on Code Generation and Optimization (CGO 2004), 20-24 March 2004, San Jose, CA, USA, pp. 75\u201388, IEEE Computer Society (2004),https:\/\/doi.org\/10.1109\/CGO.2004.1281665","DOI":"10.1109\/CGO.2004.1281665"},{"key":"27_CR12","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, Lecture Notes in Computer Science, vol. 4963, pp. 337\u2013340, Springer (2008), https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"27_CR13","doi-asserted-by":"publisher","unstructured":"Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: intermediate language and tools for analysis and transformation of C programs. In: Horspool, R.N. (ed.) Compiler Construction, 11th International Conference, CC 2002, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002, Proceedings, Lecture Notes in Computer Science, vol. 2304, pp. 213\u2013228, Springer (2002),https:\/\/doi.org\/10.1007\/3-540-45937-5_16","DOI":"10.1007\/3-540-45937-5_16"},{"key":"27_CR14","unstructured":"Saan, S.: Witness Generation for Data-flow Analysis. Master\u2019s thesis, University of Tartu (2020), https:\/\/hdl.handle.net\/10062\/94066"},{"key":"27_CR15","doi-asserted-by":"publisher","unstructured":"Saan, S., Erhard, J., Schwarz, M., Bozhilov, S., Holter, K., Tilscher, S., Vojdani, V., Seidl, H.: Goblint: Abstract interpretation for memory safety and termination (competition contribution). In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part III, Lecture Notes in Computer Science, vol. 14572, pp. 381\u2013386, Springer (2024),https:\/\/doi.org\/10.1007\/978-3-031-57256-2_25","DOI":"10.1007\/978-3-031-57256-2_25"},{"key":"27_CR16","doi-asserted-by":"crossref","unstructured":"Saan, S., Kocal, A.R., Petter, M., Holter, K., Erhard, J., Schwarz, M., Vojdani, V., Seidl, H.: Goblint: A portfolio for mixed flow-sensitive abstract interpretation (competition contribution). In: Proc. TACAS\u00a0(2), Lecture Notes in Computer Science, vol. 16506, Springer (2026)","DOI":"10.1007\/978-3-032-22749-2_26"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-22749-2_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T00:32:37Z","timestamp":1782865957000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22749-2_27"}},"subtitle":["(Competition Contribution)"],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227485","9783032227492"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22749-2_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"15 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The complete SV-COMP\u00a02026\u00a0[\n                      \n                      ] data set, including verification tasks, results, witnesses, and reproduction scripts, is available on\u00a0the\n                      \n                      \u00a0[\n                      \n                      ]. The competition version of\n                      goblitch\n                      is archived on Zenodo\u00a0[\n                      \n                      ].","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Data Availability Statement"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/about\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}