Goblint: A Portfolio for Mixed Flow-Sensitive Abstract Interpretation

Abstract 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.