Publication details
Goblitch: Combining Abstract Interpretation with Symbolic Execution via Witnesses
| Authors | |
|---|---|
| Year of publication | 2026 |
| Type | Paper in proceedings |
| Conference | Tools and Algorithms for the Construction and Analysis of Systems - 32nd International Conference, TACAS 2026, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, April 11-16, 2026, Proceedings, Part II |
| MU Faculty or unit | |
| Citation | |
| web | https://link.springer.com/chapter/10.1007/978-3-032-22749-2_27 |
| Doi | https://doi.org/10.1007/978-3-032-22749-2_27 |
| Keywords | software verification; Goblint; Witch; Goblitch; SV-COMP |
| Description | 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 False results and no incorrect results. Moreover, in the category C.ReachSafety, it produces more True results than Goblint. |
| Related projects: |