Scholarlink

Goblint is a static analyzer for C programs based on abstract interpretation. It provides a flexible framework for combining analyses and specifying what information is tracked flow- and context-sensitively. For SV-COMP 2026, we adopt a sequential portfolio of configurations of increasing precision that exploits Goblint ’s rich family of abstract domains and sensitivity options. We have improved the analyses by adding bit-level and sparse affine equalities domains, new forms of path-sensitivity, and a context gas mechanism that controls context-sensitivity for recursive programs. Goblint continues its unblemished track record of sound verification across all SV-COMP benchmarks.

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

Goblint: A Portfolio for Mixed Flow-Sensitive Abstract Interpretation

  • 会议论文

  • 发表日期：

    2026年

查看全文
  • Simmo Saan,
  • Ali Rasim Kocal,
  • Michael Petter,
  • Karoliine Holter,
  • Julian Erhard,
  • Michael Schwarz,
  • Vesal Vojdani,
  • Helmut Seidl

摘要

Goblint is a static analyzer for C programs based on abstract interpretation. It provides a flexible framework for combining analyses and specifying what information is tracked flow- and context-sensitively. For SV-COMP 2026, we adopt a sequential portfolio of configurations of increasing precision that exploits Goblint ’s rich family of abstract domains and sensitivity options. We have improved the analyses by adding bit-level and sparse affine equalities domains, new forms of path-sensitivity, and a context gas mechanism that controls context-sensitivity for recursive programs. Goblint continues its unblemished track record of sound verification across all SV-COMP benchmarks.