Verified static analysis in Isabelle/HOL

Concrete executions and interval states

The figure applies this to a real program. It shows part of the program's control-flow graph, starting at the first branch. It has one node per program point and one edge per step. Each run appears as a dot at every node it reaches, placed at the value x has there. The abstract view replaces the dots with the one interval the analysis keeps per node. Soundness means that no interval leaves out a dot.

The intervals are not exact, though. The runs only ever reach multiples of three, and an interval cannot express that, so every band also covers integers no run has. On the left this makes a node look reachable although no run reaches it. On the right the guard rules out every value in the interval, and the analysis marks the check DEAD.

Each check gets one of four verdicts, and each states what the analysis established. PROVED: the check holds in every run that reaches it. REFUTED: it fails in every run that reaches it. DEAD: no run reaches it. UNKNOWN: the intervals are too coarse to decide. A check that no run reaches can still come out UNKNOWN, as pp4 does here, because DEAD means the analysis proved the point unreachable, not merely that it happens to be.

fun main() {
  n = __voblint_nondet_int();
  x = 3 * n;

  if (x > 0) {
    if (x < 3) {
      __voblint_check(x == 1);
    }
  } else {
    if (x > 5) {
      __voblint_check(x == 6);
    }
  }
}

Numeric domains

Reduction in the Int product

An Int value describes the integers that all four of its components allow. Each component on its own can miss what another one knows, so the product lets them sharpen one another. A sharpening step never changes the set of integers the value describes. It only finds a smaller description of the same set, and a smaller description can decide a check that the larger one could not. Even a component that starts out knowing nothing can contribute, once the others have told it something.

fun main() {
  n = __voblint_nondet_int();
  x = 4 * n + 1;
  if (x >= -2) {
    if (x <= 10) {
      __voblint_check(x >= 1 && x <= 9);
    }
  }
}

fun main() {
  n = __voblint_nondet_int();interval: [−∞,+∞]
  x = 6 * n + 5;interval: [−∞,+∞] · congruence: 5+6ℤ
  a = x % 6;interval: [−1,5] · congruence: 5+6ℤ · together: {−1, 5}
  __voblint_check(a >= 0);? UNKNOWN
  if (a < 0) {a narrows to −1
    __voblint_check(a == -1);✓ PROVED
  } else {a narrows to 5
    __voblint_check(a == 5);✓ PROVED
  }
}

Cooperating analyses and queries

Int combines four numeric domains inside one value. Separate analyses can also exchange information while the fixpoint is being computed. In the first program below, both guards hold at the assignment, so x = y and z is 1. Interval keeps one range per variable, and after the guards both x and y are still unbounded. The order analysis keeps a set of pairs, each meaning that one variable is at most another. It knows x = y, but it tracks no value for z. Neither can prove the check alone. Run together, Interval's assignment asks all active analyses what x == y evaluates to, and the order analysis answers 1.

fun main() {
  x = __voblint_nondet_int();
  y = __voblint_nondet_int();
  if (x <= y) {
    if (y <= x) {
      z = (x == y);
      __voblint_check(z == 1);
    }
  }
}

fun main() {
  c = __voblint_nondet_int();
  if (0 < c) {
    x = 0;
    y = 10;
  } else {
    x = 20;
    y = 30;
  }
  __voblint_check(x <= y);
}

type_synonym activation_path = "(cfg_node × store) list"

datatype activation_trace =
    Root                                                                   activation_path
  | Call   (activation_trace_caller: activation_trace)                     activation_path
  | Resume (activation_trace_current: activation_trace)
           (activation_trace_callee: activation_trace)                     activation_path

The nesting simplifies the question every soundness proof has to ask: “Which runs can be standing at node v, and what does memory hold there?” With activation traces, the answer is the end of one path. With the flat list, you would have to scan an interleaved sequence and decide, for every occurrence of v, whether it belongs to the activation you are reasoning about. The analysis answers per program point, and per point and context once a policy keeps copies of a procedure apart. Activation traces are shaped so that this per-point question can be obtained directly instead of being reconstructed.

Grouping by activation instead of by procedure has one more consequence. In this run, sum is one procedure with three activations, and the trace keeps all three apart because each is its own box. The analysis cannot keep every activation apart. It has to decide in advance how many copies of sum to reason about separately, and a context is the result of that decision. Because the concrete side distinguishes every activation, the proofs can check that whatever the abstract side merges is still covered.

Compilation to control-flow graphs

The compiler reads a procedure one statement at a time and turns each statement into a numbered node with outgoing edges. Each statement is compiled with the number of the statement that follows it, so its target is known before it is compiled. The figure replays this on the counting loop, with the node numbers and edge labels the real compiler produces.

fun main() {
  i = 0;
  while (i < 5) {
    i = i + 1;
  }
  __voblint_check(i == 5);
}

compile_proc Π p decl n =
      (let r = n + csize (body decl); …
       in … insert (FunctionEntry p, EA_Body p, ben)
              (if falls_through (body decl)
               then insert (Statement r, EA_Ret None p, FunctionResult p) E
               else E) …)

datatype ('x, 'g, 'd) strategy_tree =
    Answer 'd
  | QueryL 'x ('d ⇒ ('x, 'g, 'd) strategy_tree)
  | QueryG 'g ('d ⇒ ('x, 'g, 'd) strategy_tree)
  | Side 'g 'd (('x, 'g, 'd) strategy_tree)

type_synonym ('x, 'g, 'd) eqsT = 'x ⇒ ('x, 'g, 'd) strategy_tree

type_synonym ('x, 'g, 'd, 'a) strategy_program =
  ('a ⇒ ('x, 'g, 'd) strategy_tree) ⇒ ('x, 'g, 'd) strategy_tree

root_query p = (cfg_exit (prog_cfg p), root_ctx)

solved_local_reader vars σ k =
  (case k of Inl vc ⇒ (if vc ∈ vars then locals (σ (Inl vc)) else bot)
           | Inr _ ⇒ bot)

Side effects on equation unknowns

Every right-hand side so far only read. It queried other unknowns and answered with a value for its own, which is why the walkthrough above could be drawn as one variable changing. The solver allows one more operation. A right-hand side can publish a value into an unknown it does not own. The solver joins the value in, records who published it, and re-evaluates every right-hand side that had read that unknown. In a strategy tree this is a Side node, the part the walkthrough left out.

Voblint publishes for exactly two reasons. A flow-insensitive program global has its own unknown. Only assigning edges publish to it, and only points mentioning the variable read it. Calls also publish entry states. A caller does not write the callee's entry point directly. It publishes the entry state under a key (Activation_Seed), which the callee's entry reads back. The vendored solver can only side-effect global unknowns, so this key is a global stand-in for the local unknown that Goblint writes with sidel. The alignment register records this deliberate difference from Goblint.

Both settings act on this one publication. Contexts decide which key a call publishes under, and therefore how many copies of a procedure exist. Globals decides how multiple publications to the same key are merged.

Call equations and the enter/combine protocol

Call behavior is determined by the analysis and context policy. enter builds the callee's entry state from the caller's state. A context policy picks which copy of the callee receives that state. combine merges the callee's exit state back into the caller. enter and combine come from the analysis; the policy is a run setting. The framework wires all three into equations in the same way for every domain, and each connection carries its own soundness obligation.

This wiring stays within one procedure. Each node gets one equation, built from that node's incoming edges, and a call site is a node whose contribution publishes and queries. Generating the equations never looks into the callee, which is why a recursive call needs no special case. The generator does not follow the recursion; the solver determines how far it proceeds. A real run does go into f, and the step-through of a run follows one through a program with calls.

fun main() {  a = f(2);  __voblint_check(a == 2);}

eqs entry_main =
  QG (Seed entry_main) (λs.
    Answer (cinit ⊔ locals s))

eqs pp5 =
  QL entry_main (λs.
    Answer (body(main) s))

eqs pp6 =
  QL pp5 (λcaller.
    Side (Seed entry_f) (enter f(2) caller)
      (QL exit_f (λcallee.
        Answer (combine caller callee))))

eqs pp7 =
  QL pp6 (λs.
    Answer (check(a == 2) s))

eqs exit_main =
  QL pp7 (λs.
    Answer (return s))

Calling-context policies

The equations above simplified one thing. Their unknowns were bare program points, so any two calls to f would land in the same copy of it, and the entry states they produce would be merged. An analysis can be set up to keep those call sites apart. A context is the key a procedure is analyzed under. Call sites that produce the same key share one copy of f, and call sites that produce different keys each get their own. This setting picks how that key is computed, using one of the available policies.

c is main's own context. c₁ and c₂ are the keys the strategy returned at the two call sites, and each appears in exactly two places: the key the call publishes under, and the exit it queries. The rest of the equation stays as before.

Precision of context policies

The available context policies differ only in the key they use. The call string also takes a depth, so the context comparison shows four settings. It concerns a small program in which wrap passes its argument straight to scale, which doubles it, so a is 2 and b is 8.

Whether the analysis can establish a == 2 depends on whether the two calls are still kept apart when they reach scale. If they meet there, scale receives one value covering both arguments and returns one result covering both, so the check is UNKNOWN. The strategy alone decides this. Each mode's Try link opens the playground with that setting.

fun scale(v) {
  return v * 2;
}

fun wrap(w) {
  r = scale(w);            // s3
  return r;
}

fun main() {
  a = wrap(1);             // s1
  b = wrap(4);             // s2
  __voblint_check(a == 2);
}

Precision and cost of calling contexts

Every context is another copy of a procedure to solve. Of the two measurements below, the first counts the nodes of the solved graph and the second counts the contexts themselves. Both grow with the call-string depth until it is long enough to tell every call path apart. The numbers are measured with the analyzer on this site (Interval, Warrow). Additional contexts can improve precision, but the improvement is not monotone.

fun f0(x) { __voblint_check(x <= 22); }
fun f1(x) { f0(x); f0(x + 1); }
fun f2(x) { f1(x); f1(x + 2); }
fun f3(x) { f2(x); f2(x + 3); }
fun f4(x) { f3(x); f3(x + 4); }
fun f5(x) { f4(x); f4(x + 5); }
fun f6(x) { f5(x); f5(x + 6); }

fun main() {
  f6(1);
}

fun down(n) {
  __voblint_check(n >= 0);

  if (n > 0) {
    down(n - 1);
  }
}

fun main() {
  down(100);
}

Contributions to global unknowns

In the playground this is the Globals setting. “Globals” there means the solver's global unknowns, not VIMP's global declarations. Under the default placement, a program's globals are part of the state a call publishes. They therefore cross a call through a solver global. Under the other placement each program global has a solver global of its own, which the end of this section describes. The dashed arrow in the equation diagram represents entry-state publication. A call site writes the callee's entry key, and the entry equation reads it. The rest of this section is about those entry keys, and this setting decides what happens when multiple writes reach one of them.

fun p(x) {
  __voblint_check(x <= 2);
}

fun g(y) {
  __voblint_check(y < 10);
}

fun s(a) {
  if (a < 4) {
    s(9 / (a + 2));              // E
  }
  __voblint_check(a <= 9);
}

fun main() {
  p(1);                          // A
  p(2);                          // B
  i = 0;
  while (i < 10) {               // C, ten times
    g(i);
    i = i + 1;
  }
  s(-1);                         // D
}

Update rules for global unknowns

A site sends the state its call binds the callee's parameters to, so [0, 3] means one site says the parameter arrives somewhere in that range. The rule combines these contributions into a single value, the callee's entry state, from which the callee is analysed and seeds its own calls.

One site can publish repeatedly. A right-hand side is not run once; the solver re-evaluates it whenever an unknown it reads has moved, and each re-evaluation publishes again at the same key from the same origin. Site C above does that each time the loop head's value moves, which is a few rounds however many turns the loop runs for. A contribution comes back smaller when narrowing has pulled a widened value down and the site is recomputed from it.

Below, A and B are two writers at one key. The numbers are not taken from the program. They are chosen so that A sends three times, first smaller and then larger, and this sequence distinguishes the first four rules. Step 2 separates Warrow from the rest, step 3 separates Join from Join per origin, and step 4 separates Join from Warrow per origin. Telling Bounded narrowing apart from Warrow per origin takes more steps. The rules apply to any domain with join, widening, and narrowing. Intervals illustrate the difference between widening and join. Sign and Parity are short enough lattices that their widening is defined as the join.

Termination with join updates

The cost of joining grows with the length of the chain. A joining rule never widens. It follows a growing value one step at a time, requiring one solver round per step. Widening can cover that growth in one step. On f(x) { if (x < N) f(x + 1); }, started from f(0), every rule proves x <= N. But as N grows from 64 to 4096, the two joining rules go from 5 ms to about 240 ms, while the three widening rules stay at 4 ms. Without the bound, the growth never ends, which is the no answer in the update-rule comparison.

Choice of update rule

No setting is best everywhere. They trade how quickly a growing value is cut off against how much a merged value forgets. Nothing proves any of them terminates on every program: Voblint assumes termination per program, so a bad choice shows up as a run that never finishes, not as a wrong answer.

Context policies and update rules

Run every combination of the two settings on the program above, and their effects separate. Cost changes only between rows. The solved graph has 24 nodes with no contexts, 34 at either call-string depth, and 38 under entry states. Update rules do not change the unknowns, so each row retains its node count. Precision changes along both axes, and the coarser the context, the more a widening loses. Warrow proves one of the three checks with no contexts and all three once entry states keep the writers apart. Warrow per origin and Bounded narrowing lose only s's check, and only with no contexts. Both joining rules prove all three everywhere. The cheapest fully precise cells are None with either joining rule. Join is also the rule that gives no answer within the time limit on a recursion whose argument keeps growing.

Recursion with a growing argument

Both settings meet in recursion. f(x) calls f(x + 1) forever, so real runs wind outward on an endless spiral: f(0), f(1), f(2), each turn wider than the last. The analysis must describe these activations with finitely many contexts. Join and entry-state contexts follow the growing arguments and time out. Warrowing covers the growth. Switch to the same function stopped at x = 10 and every setting finishes.

fun f(x) {
  __voblint_check(x >= 0);

  f(x + 1);
}

fun main() {
  f(0);
}

Representation of program globals

So far a VIMP global has behaved like a local that every procedure can see. It travels inside each point's state, entering a callee with the caller's state and returning through combine. The playground's Program globals setting (--program-globals on the command line, program_globals in the theories) offers a second placement, the one the FM 2026 tutorial calls flow-insensitive.

Under Flow-insensitive, each declared global gets a global unknown of its own, and the points stop carrying it. An edge that assigns g publishes the new value of g to that unknown, an edge whose expressions mention g reads it, and a call reads only the globals its arguments mention. A point that touches no global depends on none, and a write to g re-runs only the points that read g (read_g_depends_on_g_only and write_h_publishes_h_only check this on one reading and one writing edge). The initial value 0 is published by the program's entry like any other write.

This placement costs precision, because one value has to cover everything the global ever holds, at every point. Take set() writing Gx = 1 and get() returning Gx, called in that order from main. Flow-sensitively, Sign carries Gx = + from set's exit into get and proves 0 < y. Flow-insensitively, the unknown of Gx joins the initial 0 with the written 1, Sign can only say Gx ≥ 0, and 0 < y stays UNKNOWN. Run it flow-sensitively and flow-insensitively to compare.

For a sequential VIMP program, the additional placement can lose precision, as this example shows. It provides infrastructure for a future language extension. The FM 2026 tutorial names multi-threaded code as a main source of mixed flow-sensitivity. A thread-modular analysis collects values exchanged through shared globals flow-insensitively. This separation allows flow-sensitive tracking of each thread's state without enumerating all concurrent thread states. Goblint analyzes concurrent C this way. VIMP has no threads, so the current result concerns the framework and its end-to-end theorem, which already support a mixed flow-sensitive analysis. An extension with threads would reuse this machinery and add a thread semantics and synchronization.

Both placements carry the same end-to-end theorem, run_voblint_source_sound, because the setting is an argument of the analysis function it is stated about. The flow-insensitive one comes from a lifter, keyed_split_spec, that wraps the active analyses. The lifter's soundness proof (keyed_split_contract) rests on a fact about the concrete semantics. A step leaves every global it does not assign unchanged (edge_step_frame), so skipping the publication of an unwritten global loses nothing. Only per-variable state splits this way. The order analysis relates variables to each other and keeps its whole state at the points.

The global unknowns are side-effected, so the Globals setting above decides how their writes merge. Choosing Flow-insensitive selects Bounded narrowing unless you chose a rule explicitly. Under plain warrowing, a global unknown that alternates between widening and narrowing can fail to stabilize.

fun f(n) {
  if (n < 2) {
    return 1;
  }
  r = f(n - 1);
  return n * r;
}

fun main() {
  x = f(2);
}

Proof obligations for the soundness chain

The chain connects real runs to the verdicts, and the displayed argument uses two theorems and three obligations the analyzer has to discharge. Remove one to see which answers stop being covered.

Design constraints exposed by the proof

Stating the soundness theorem precisely exposed design constraints on the analyzer. The first two below are necessity results. Weakening the condition while keeping the others admits an unsound claim. These results establish necessity for the exhibited conditions. They do not establish necessity for every premise in the development. The third is an executable witness that the implemented equation system obeys another constraint the proof exposed.

Most programs in the regression corpus are quick to analyze. The median one solves in a few milliseconds natively. A proof says nothing about speed, though, and some settings are expensive. The numbers here come from the recorded measurement, on one machine.

Contexts are where the cost goes. With entry-state contexts a recursive procedure gets one context for every abstract argument it is entered with. Under the interval domain, which distinguishes individual numbers, h(n) counting down from n therefore keeps n + 1 copies of h apart. That copy count drives the run time. A CPU profile of such a run spends much of its own time in the generated code's list lookups, which compare nodes and contexts one at a time.

The playground runs the same generated code compiled to WebAssembly. It is slower than the native command line.

The profiling page documents the measurements and methods. It includes results for each domain and context policy across the corpus, scaling curves, and an interactive CPU profile. These measurements do not establish bounds for arbitrary programs. Whether the solver finishes at all is a premise checked per program, as the next section explains.

VIMP and C

Goblint analyzes C. Voblint analyzes VIMP, a language small enough that its semantics could be written down and every analysis step proved against it. Hover a region to see what VIMP leaves out.

Limits of the soundness guarantee

Formalization effort

The analyzer that runs is a small part of the project. Most of the work went into definitions of what a program means and into proofs that every step of the analysis respects them.

Structure of the formal development

The iceberg shows the size of the development; this figure shows its structure. Every Isabelle session is a rock layer, placed just above the highest session it builds on, from the logic at the bottom to the examples at the surface. Hover over a session, and the layers it rests on light up. A layer's thickness grows with its line count, so the core sample also shows where most of the material is.

The CLI and browser expose all six analyses: Sign, Interval, Parity, Congruence, Int and relational Order. Order sits lower because it supplies its local specification directly, without the non-relational builder. Hover over CLI to see the dependencies of their shared entry point.

• Certified pipeline theory Open Voblint.thy, the downstream entry point that presents the certified pipeline and links its major layers and flagship theorems. →
• Interactive proof map Explore the formalization as a corpus wheel or treemap. Zoom into sessions and theories, inspect entities, and open their Isabelle documentation. →
• Master thesis The written thesis, with design rationale, proof architecture, and references back into the Isabelle development. →
• Conference paper draft A 16-page condensed account of the end-to-end soundness argument, drafted for ITP 2027 and not yet submitted. →
• Interactive Isabelle documentation Browse every generated theory page with cross-linked definitions, locales, lemmas, and source structure. →
• Isabelle documentation Isabelle-generated printout of the development, including the certificate appendix. →
• Exported OCaml code The generated implementation behind the CLI and browser analyzer, exported from the Isabelle/HOL development. ↗
• GitHub repository Source theories, generated analyzer, build tooling, regression tests, examples, and project history. ↗