Search results

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

·  

SV-COMP 2027

[BA] Synthesizing linear ranking functions for LASW programs

student-job

Status: Open.

Feature

#1872 In goblint/analyzer;

· DrMichaelPetter opened on Nov 11, 2025

Parsing results in Stack Overflow

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

Status: Open.

Bug

#1866 In goblint/analyzer;

· michael-schwarz opened on Nov 7, 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

·  

SV-COMP 2027

Docs: Recommend context gas over context widening

documentationDocumentation, commentsDocumentation, comments

Status: Open.

Bug

#1856 In goblint/analyzer;

· michael-schwarz opened on Oct 29, 2025

Use strict inequalities in relational witness invariants

good first issue

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

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

usability

Status: Open.

Feature

#1850 In goblint/analyzer;

· sim642 opened on Oct 23, 2025

<code>exp.volatiles_are_top</code> and <code>exp.globs_are_top</code> are only considered by base analysis

good first issue

precision

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

Status: Open.

Bug

#1843 In goblint/analyzer;

· sim642 opened on Oct 17, 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

·  

SV-COMP 2027

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

·  

SV-COMP 2027

Unsound evaluation of <code>sizeof</code> expressions

unsound

Status: Open.

Bug

#1809 In goblint/analyzer;

· sim642 opened on Aug 14, 2025

Quickcheck int domain overflows

testing

unsound

Status: Open.

Task

#1808 In goblint/analyzer;

· sim642 opened on Aug 14, 2025

Consider some more interactions between thread creation, joins, and mutexes

precision

Status: Open.

Feature

#1805 In goblint/analyzer;

· michael-schwarz opened on Aug 8, 2025