Scholarlink

Prior to Test-Comp 2026, Ultimate TestGengenerated test cases with a sequential software model checking approach, which is named trace abstraction and performs counterexample-guided abstraction refinement. To generate tests, Ultimate TestGenencodes test goals as property violations and generates test cases from counterexamples detected by trace abstraction.For Test-Comp 2026, we keep this general principle but make two changes.First, we adapt Ultimate TestGento a recent parallelization of trace abstraction.Second, we extend Ultimate TestGenwith a Path-Checker, which runs in parallel with parallel trace abstraction and exhaustively explores counterexamples but skips refinement.

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

Ultimate TestGen: Combining Parallel Trace Abstraction and Symbolic Path Execution (Competition Contribution)

  • 会议论文

  • 发表日期：

    2026年

查看全文
  • Max Barth,
  • Daniel Dietsch,
  • Matthias Heizmann,
  • Marie-Christine Jakobs

摘要

Prior to Test-Comp 2026, Ultimate TestGengenerated test cases with a sequential software model checking approach, which is named trace abstraction and performs counterexample-guided abstraction refinement. To generate tests, Ultimate TestGenencodes test goals as property violations and generates test cases from counterexamples detected by trace abstraction.For Test-Comp 2026, we keep this general principle but make two changes.First, we adapt Ultimate TestGento a recent parallelization of trace abstraction.Second, we extend Ultimate TestGenwith a Path-Checker, which runs in parallel with parallel trace abstraction and exhaustively explores counterexamples but skips refinement.