Goblitch: Combining Abstract Interpretation with Symbolic Execution via Witnesses

Lecture notes in computer science 2026

View at publisher
Authors: Karoliine Holter, Paulína Ayaziová, Simmo Saan, Jan Strejček, Vesal Vojdani
DOI: 10.1007/978-3-032-22749-2_27
Cited by: 1
References: 11

Abstract

Abstract goblitch is a new verification toolchain for reachability safety that combines the abstract interpreter Goblint with the witness validator Witch . goblitch integrates these two tools in a refinement loop where Goblint repeatedly builds an abstract reachability graph and Witch decides whether an error path in the current graph corresponds to any real program execution. Experiments show that goblitch produces many results and no incorrect results. Moreover, in the category C.ReachSafety , it produces more results than Goblint .

Fields of Study & Subjects

Security and Verification in Computing Formal Methods in Verification Software Testing and Debugging Techniques

Publication details

Journal / source
Lecture notes in computer science
Publisher
Springer Nature Switzerland
Pages
523–529
Publication date
1 January 2026
Language
EN