Scholarlink

Symbiotic  11 is the first version of Symbiotic that features predicate abstraction. We implemented the recently introduced technique of symbolic execution with implicit predicate abstraction in the underlying symbolic executor Slowbeast. Additionally, we improved non-termination checking and witness production. We show that these changes have positive effect on the overall performance of Symbiotic  11.

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

Symbiotic 11 Predicate Abstraction Joins the Party

  • 会议论文

  • 发表日期：

    2026年

查看全文
  • Paulína Ayaziová,
  • Martin Jonáš,
  • Vincent Mihalkovič,
  • Jindřich Sedláček,
  • Jan Strejček

摘要

Symbiotic  11 is the first version of Symbiotic that features predicate abstraction. We implemented the recently introduced technique of symbolic execution with implicit predicate abstraction in the underlying symbolic executor Slowbeast. Additionally, we improved non-termination checking and witness production. We show that these changes have positive effect on the overall performance of Symbiotic  11.