Scholarlink

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.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

Goblitch: Combining Abstract Interpretation with Symbolic Execution via Witnesses

  • 会议论文

  • 发表日期：

    2026年

查看全文
  • Karoliine Holter,
  • Paulína Ayaziová,
  • Simmo Saan,
  • Jan Strejček,
  • Vesal Vojdani

摘要

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.