Search results

Invalid widen after join with mhp and threadJoins domains (regression 10/15)

bug

Status: Open.

#1959 In goblint/analyzer;

· arkocal opened on Mar 9, 2026

Synthetize top argument values by type for specially spawned functions

precision

Status: Open.

Feature

#1958 In goblint/analyzer;

· sim642 opened on Mar 9, 2026

Limit hashconsing to apron domain if it is undesired globally instead of refusing to run

Status: Open.

Feature

#1956 In goblint/analyzer;

· michael-schwarz opened on Mar 6, 2026

Tracking function pointers in indirectly pointed structures

analyze-that

unsound

Status: Open.

Bug

#1951 In goblint/analyzer;

· jprotopopov-ut opened on Mar 5, 2026

Handling of compatible structure types under C23 semantics

analyze-that

Status: Open.

Feature

#1950 In goblint/analyzer;

· jprotopopov-ut opened on Mar 5, 2026

affeq analysis crashes on 672 SV-COMP Juliet overflow tasks

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

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

Status: Open.

Bug

#1943 In goblint/analyzer;

· sim642 opened on Feb 6, 2026

·  

SV-COMP 2027

Non-deterministic non-termination of <code>ldv-linux-4.2-rc1/linux-4.2-rc1.tar.xz-43_2a-drivers--scsi--device_handler--scsi_dh_rdac.ko-entry_point.cil.out.i</code>

performanceAnalysis time, memory usageAnalysis time, memory usage

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

Status: Open.

Bug

#1942 In goblint/analyzer;

· sim642 opened on Feb 6, 2026

·  

SV-COMP 2027

MCP Server

Status: Open.

Feature

#1937 In goblint/analyzer;

· michael-schwarz opened on Feb 3, 2026

Investigate growing set of protected mutexes for cluster-analysis

precision

Status: Open.

Feature

#1936 In goblint/analyzer;

· michael-schwarz opened on Feb 3, 2026

False invariants in correctness witnesses generated by Goblint

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

unsound

Status: Open.

Bug

#1926 In goblint/analyzer;

· jprotopopov-ut opened on Jan 21, 2026

·  

SV-COMP 2027

<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

·  

SV-COMP 2027

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

·  

SV-COMP 2027