Scholarlink

We present the multi-threaded software model checker Ultimate Paralizer, which lets us use multiple CPU cores effectively. Ultimate Paralizer is built on Ultimate Automizer ’s automata-theoretic approach to software model checking, which performs a variant of counterexample-guided abstraction refinement. The parallelization idea of Ultimate Paralizer is simple but effective. For parallelization, Ultimate Paralizer analyzes multiple, diverse counterexample independently in parallel including the computation of an abstraction refinement if necessary. A central coordinator steers the verification process, in particular it selects the counterexamples for analysis and performs the necessary abstraction updates. In SV-COMP 2026, Ultimate Paralizer participates in the categories reach-safety and no-overflows and in the demo wall-time track.

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

Ultimate Paralizer: Parallel Trace Abstraction (Competition Contribution)

  • 会议论文

  • 发表日期：

    2026年

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

摘要

We present the multi-threaded software model checker Ultimate Paralizer, which lets us use multiple CPU cores effectively. Ultimate Paralizer is built on Ultimate Automizer ’s automata-theoretic approach to software model checking, which performs a variant of counterexample-guided abstraction refinement. The parallelization idea of Ultimate Paralizer is simple but effective. For parallelization, Ultimate Paralizer analyzes multiple, diverse counterexample independently in parallel including the computation of an abstraction refinement if necessary. A central coordinator steers the verification process, in particular it selects the counterexamples for analysis and performs the necessary abstraction updates. In SV-COMP 2026, Ultimate Paralizer participates in the categories reach-safety and no-overflows and in the demo wall-time track.