List view

Prototype loop transition invariant generation

feature

proof-of-concept

sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses

Status: Draft (not ready).

goblint/analyzernumber 1849

#1849 In goblint/analyzer;

· sim642 opened on Oct 23, 2025

Minimize unnecessary casts and check for overflows in witness invariants

explainability

relationalRelational analyses (Apron, affeq, lin2var)Relational analyses (Apron, affeq, lin2var)

sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses

Status: Open (in progress).

goblint/analyzernumber 1665

#1665 In goblint/analyzer;

· karoliineh opened on Jan 27, 2025

Incompatible ikinds exception on svcomp22 reachsafety tests

bug

sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses

Status: Open.

#751 In goblint/analyzer;

· MartinWehking opened on Jun 2, 2022

Handle large programs context-insensitively with autotuner

performanceAnalysis time, memory usageAnalysis time, memory usage

sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses

Status: Open.

#899 In goblint/analyzer;

· jerhard opened on Nov 10, 2022

Determine list of thread wrappers & Create autotuner for it

good first issue

precision

sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses

Status: Open.

#1066 In goblint/analyzer;

· michael-schwarz opened on May 30, 2023

Witness invariants for widened variables

feature

performanceAnalysis time, memory usageAnalysis time, memory usage

sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses

Status: Open.

#1219 In goblint/analyzer;

· sim642 opened on Oct 20, 2023

More precise float domain for <code>float</code> and <code>double</code>

good first issue

precision

student-job

Status: Open.

#919 In goblint/analyzer;

· michael-schwarz opened on Nov 20, 2022

Dedicated Context Constructions for Termination Analysis

good first issue

precision

student-job

Status: Open.

#1422 In goblint/analyzer;

· michael-schwarz opened on Apr 21, 2024

Re-evaluate defaults for <code>ana.malloc.unique_address_count</code> in SV-Comp

precision

sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses

Status: Open.

#1168 In goblint/analyzer;

· michael-schwarz opened on Sep 14, 2023

Atomic operations support

benchmarking

c11

feature

good first issue

precision

student-job

sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses

Status: Open.

#1057 In goblint/analyzer;

· sim642 opened on May 24, 2023

valid-memtrack analysis doesn't check sizes, only checks at end &amp; doesn't consider locals

bug

sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses

unsound

Status: Open.

#1622 In goblint/analyzer;

· sim642 opened on Nov 5, 2024

Inequalities between pointers do not work

good first issue

precision

sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses

Status: Open.

Feature

#1680 In goblint/analyzer;

· karoliineh opened on Feb 13, 2025

SVCOMP: Investigate / Come up with autotuners for new features

relationalRelational analyses (Apron, affeq, lin2var)Relational analyses (Apron, affeq, lin2var)

sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses

Status: Open.

Feature

#1681 In goblint/analyzer;

· michael-schwarz opened on Feb 14, 2025

Output location invariants for witnesses at labels

sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses

Status: Open.

Feature

#1735 In goblint/analyzer;

· sim642 opened on Apr 24, 2025

SV-COMP autotuner spuriously enables all integer domains

bug

performanceAnalysis time, memory usageAnalysis time, memory usage

precision

sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses

unsound

usability

Status: Open.

#1472 In goblint/analyzer;

· sim642 opened on May 20, 2024

Remaining verdicts <code>Error (both branches dead)</code> on SV-COMP

bug

sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses

Status: Open.

Bug

#1696 In goblint/analyzer;

· michael-schwarz opened on Feb 27, 2025

Spurious out of memory on SV-COMP Intel TDX tasks

benchmarking

performanceAnalysis time, memory usageAnalysis time, memory usage

sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses

Status: Open.

Bug

#1824 In goblint/analyzer;

· sim642 opened on Sep 24, 2025

Autotuner only enables relational analysis for at most 2 globals

precision

relationalRelational analyses (Apron, affeq, lin2var)Relational analyses (Apron, affeq, lin2var)

sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses

Status: Open.

Bug

#1832 In goblint/analyzer;

· sim642 opened on Sep 28, 2025

Unconfirmed invariants in SV-COMP 2026

sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses

Status: Open.

Bug

#1860 In goblint/analyzer;

· karoliineh opened on Nov 3, 2025

Remove restriction that no loop unrolling is done when breaks are in the loop

precision

sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses

Status: Draft (not ready).

goblint/analyzernumber 1518

#1518 In goblint/analyzer;

· karoliineh opened on Jun 19, 2024

Questionable invariants in SV-COMP 2025 witnesses

sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses

unsound

usability

Status: Open.

Bug

#1722 In goblint/analyzer;

· sim642 opened on Apr 9, 2025

Enable <code>sem.malloc.fail</code> or set <code>sem.malloc.zero</code> to <code>pointer</code> for SV-COMP 2027

precision

sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses

unsound

Status: Open.

Task

#1888 In goblint/analyzer;

· sim642 opened on Dec 1, 2025

YAML witnesses containing entries with different versions in SV-COMP 2026

sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses

Status: Open.

Bug

#1902 In goblint/analyzer;

· sim642 opened on Dec 15, 2025

BranchSet: Possibilities for Optimization

bug

performanceAnalysis time, memory usageAnalysis time, memory usage

precision

sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses

Status: Open.

#1903 In goblint/analyzer;

· michael-schwarz opened on Dec 16, 2025

<code>location_invariant</code> should not be at <code>switch</code> <code>case</code> label

sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnesses

Status: Open.

Bug

#1925 In goblint/analyzer;

· sim642 opened on Jan 21, 2026