-
Notifications
You must be signed in to change notification settings - Fork 89
OpenAug 18, 2026
Due by December 1, 2026
•Last updated Functionally equivalent to Goblint in SV-COMP 2027.
26% complete
List view
0 of 14 selected 0 issues of 14 selected
Remove duplicate
ctx-derived arguments in base analysiscleanupRefactoring, clean-upRefactoring, clean-upStatus: Open.#1266 In goblint/analyzer;Avoid eager string conversions during analysis
cleanupRefactoring, clean-upRefactoring, clean-upperformanceAnalysis time, memory usageAnalysis time, memory usageStatus: Open.- Status: Open.
Upgrade to OCaml 5.0 as default
dependenciesPull requests that update a dependency filePull requests that update a dependency filesetupDependencies, CI, releasingDependencies, CI, releasingStatus: Open (in progress).Replace eager
showwith lazyprettyduring analysiscleanupRefactoring, clean-upRefactoring, clean-upperformanceAnalysis time, memory usageAnalysis time, memory usagerelationalRelational analyses (Apron, affeq, lin2var)Relational analyses (Apron, affeq, lin2var)Status: Open (in progress).Violation witness feasibility analysis using
Witchsv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnessesStatus: Draft (not ready).Clean up library function spawning in base analysis
cleanupRefactoring, clean-upRefactoring, clean-upStatus: Open.Add
asm gotosupportpr-dependencyDepends or builds on another PR, which should be merged beforeDepends or builds on another PR, which should be merged beforeStatus: Open (in progress).Port tutorial analyses to
SimplifiedSpecand reuseSimplifiedUnitAnalysisdefaults while preservingunitAnalysiscompatibilitycleanupRefactoring, clean-upRefactoring, clean-upStatus: Open (in progress).- Status: Open.#2039 In goblint/analyzer;
memOutOfBounds analysis causes integer overflow
sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnessesStatus: Open.#1801 In goblint/analyzer;Fix spurious overflow checks in memOutOfBounds
sv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnessesStatus: Open (in progress).Switch to
widenwhich doesn't requireleqon argumentscleanupRefactoring, clean-upRefactoring, clean-upperformanceAnalysis time, memory usageAnalysis time, memory usageStatus: Open (in progress).- Status: Open (in progress).