Scholarlink

Modeling memory accurately is crucial for the verification of C programs, but its inherent complexity limits scalability and efficiency. A memory model that abstracts unnecessary details while preserving essential information can significantly improve verification performance. In this work, we present a one-dimensional memory model that has recently been integrated into all software verifiers of the Ultimate tool family. Compared to our previous two-dimensional memory model, this abstraction trades some precision for improved efficiency. While it is not suitable for verifying memory safety properties, it enables more scalable reachability verification. An experimental evaluation on SV-COMP reachability benchmarks demonstrates that Ultimate Automizer solves up to 30.45 % more tasks when using the one-dimensional memory model.

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

Ultimate Automizer with a One-Dimensional Memory Model

  • 会议论文

  • 发表日期：

    2026年

查看全文
  • Manuel Bentele,
  • Max Barth,
  • Marcel Ebbinghaus,
  • Jan Körner,
  • Daniel Dietsch,
  • Matthias Heizmann,
  • Dominik Klumpp,
  • Frank Schüssele,
  • Andreas Podelski

摘要

Modeling memory accurately is crucial for the verification of C programs, but its inherent complexity limits scalability and efficiency. A memory model that abstracts unnecessary details while preserving essential information can significantly improve verification performance. In this work, we present a one-dimensional memory model that has recently been integrated into all software verifiers of the Ultimate tool family. Compared to our previous two-dimensional memory model, this abstraction trades some precision for improved efficiency. While it is not suitable for verifying memory safety properties, it enables more scalable reachability verification. An experimental evaluation on SV-COMP reachability benchmarks demonstrates that Ultimate Automizer solves up to 30.45 % more tasks when using the one-dimensional memory model.