Arrow Research search

Author name cluster

Ali Rasim Kocal

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers
1 author row

Possible papers

2

TACAS Conference 2026 Conference Paper

Goblint: A Portfolio for Mixed Flow-Sensitive Abstract Interpretation

  • Simmo Saan
  • Ali Rasim Kocal
  • Michael Petter
  • Karoliine Holter
  • Julian Erhard
  • Michael Schwarz
  • Vesal Vojdani
  • Helmut Seidl

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.

DOI

TACAS Conference 2026 Conference Paper

Same Engine, Multiple Gears: Parallelizing Fixpoint Iteration at Different Granularities

  • Ali Rasim Kocal
  • Michael Schwarz
  • Simmo Saan
  • Helmut Seidl

Abstract Fixpoint iteration constitutes the algorithmic core of static analyzers. Parallelizing the fixpoint engine can significantly reduce analysis times. Previous approaches typically fix the granularity of tasks upfront, e. g. , at the level of program threads or procedures — yielding an engine permanently stuck in one gear. Instead, we propose to parallelize a generic fixpoint engine in a way that is parametric in the task granularity — meaning that our engine can be run in different gears. We build on the top-down solver TD, extended with support for mixed-flow sensitivity, and realize two competing philosophies for parallelization, both building on a task pool that schedules tasks to a fixed number of workers. The nature of tasks differs between the philosophies. In the immediate approach, all tasks access a single thread-safe hash table maintaining solver state, while in the independent approach, each task has its own state and exchanges data with other tasks via a publish/subscribe data structure. We have equipped the fixpoint engine of the static analysis framework Goblint with implementations following both philosophies and report on our results for large real-world programs.

DOI
v2026.09.13