\section{Evaluation}
\label{sec:evaluation}

A soundness theorem may have unsatisfiable premises or allow an analyzer that
answers \verdict{UNKNOWN} everywhere (\isaname{unknown_everywhere_sound}).
We therefore exhibit programs for which the theorem applies and the analyzer
proves checks, and show that a domain obligation rejects a known defect.
We then compare the precision of context policies on a recursive program.
Facts about one fixed program are proved by \texttt{eval}, which runs
generated code and therefore also trusts the code generator. Recorded analyzer outputs
are checked against fresh runs by \texttt{pixi run thesis-claims};
\cref{tab:contexts} is generated from these claims.

\subparagraph*{Non-vacuity (machine-checked, one program each).}
For the program of \cref{fig:running}, analyzed with Interval, entry-state
contexts, and the warrowing update rule, we construct a source execution in Isabelle
that returns from both calls. Evaluation shows that the analyzer answers with
both checks \verdict{PROVED}, and \isaname{nv_source_certified} instantiates
\cref{thm:headline} with every premise discharged. Companion instances do the
same for a single check (\isaname{nv_check_proved_sound}) and for a
\verdict{DEAD} check (\isaname{nv_dead_unreached}).

\subparagraph*{Necessity of the soundness obligations (machine-checked).}
The theorem \isaname{total_dropped_unsound} exhibits a cover that meets the
other four coverage obligations but omits a reachable store, showing why
\oblig{Total} is required.

A separate example tests a domain obligation against a real Goblint defect.
Goblint once claimed \texttt{c \% 2 == 1} for $c \in \{-5, -7\}$,
although C's truncating remainder gives $-1$ (issue 1156, fixed
in~\cite{goblint1161}). The defect concerns the domain's arithmetic operation. Each domain's
abstract remainder operation must satisfy \isaname{mod_sound} in the locale
\isaname{sound_arith_ops}: the concretization of its result must contain the truncating remainders
of all concrete operands represented by its arguments.
The theorem \isaname{congruence_mod_sound} establishes this property for the
congruence domain. \isaname{prefix_congruence_mod_unsound} proves
that every abstract remainder returning the constant~$1$ for
$(1 + 2\mathbb{Z}) \bmod 2$ violates the obligation at $-5$, so the defective
operator could not be registered.

\subparagraph*{Calling contexts on recursive programs (executable).}
\Cref{tab:contexts} reports one regression program's results under each context policy.
Mutually recursive procedures \texttt{f} and \texttt{g} return $2$ and $1$ at
the bottom of the recursion. \texttt{main} calls \texttt{f(2)} and
\texttt{g(2)} inside a loop of 200 iterations and checks both results. Each
call chain is three call sites deep. The table also counts the copies of
\texttt{f} and \texttt{g} the analysis creates. With one context per
procedure, or with call strings of length 1, the activations of different
depths share a state and both results widen to $[1,12]$. With call strings of length 2 or with
entry-state contexts, activations at different depths have separate abstract
states, and both checks are proved. The
loop adds no contexts, because the callee contexts do not depend on the loop
counter. A related program has a machine-checked precision comparison
(\isaname{sign_k2_strictly_more_precise_than_k1_at_g}). At one callee entry,
the routed solution for call-string length 2 is strictly more precise than
for length 1. That theorem compares
two equation-system solutions computed by \texttt{eval} for this program.
It establishes neither a corresponding result about \isaname{run_voblint}
nor a general precision ordering between call-string lengths.

\begin{table}[t]
\centering
\small
\input{generated/contexts}
\caption{Callee contexts of \texttt{f} and \texttt{g}, verdicts and computed
values for the two checks of the regression fixture
\texttt{09-depth2\_mutual\_recursion\_in\_loop} (group \texttt{17-call-string})
under Interval, per context policy. Concretely, \texttt{res1} is always $2$ and
\texttt{res2} always $1$. Generated from reproducible analyzer runs.}
\label{tab:contexts}
\end{table}

The thesis~\cite{lerchner26thesis} also reports Voblint's results on the programs of Monniaux's
tutorial on the flavors of abstract interpretation~\cite{monniaux24} and
compares the verdicts with Goblint's.

\subparagraph*{Running time (empirical).}
We use the OCaml code generated by Isabelle without handwritten optimization.
A proved code equation, \isaname{init_publications_code}, avoids recompiling
the program during equation evaluation.
The profiling run at repository revision
\texttt{17fcb363d} analyzed the 380 regression fixtures that set no timeout of
their own. The 15 configurations combine five domains with three context policies
(none, call strings of length 1, entry states). Excluding the eleven
ill-formed programs leaves \stat{prof.fixtures}
fixtures and \stat{prof.cases} cases. A case's time is the median of three repetitions on an
Apple M4 Pro; a case that times out (30\,s) or fails in any repetition counts
as failed. Most fixtures are small regression programs, so low solve times
on this corpus do not establish performance on larger programs. All \stat{prof.timeouts} timeouts are entry-state cases with
Interval, Int or Congruence on seven recursive fixtures, where each recursion
level creates a new context. One is
\texttt{24-site-figures/precision/13-recursion\_grows\_warrow.vimp}: \texttt{f(x)}
checks \texttt{x >= 0} and calls \texttt{f(x + 1)}. With Interval and one context
per procedure, the analyzer proves the check; with entry-state contexts, the
analysis exceeds the 30\,s timeout. Call strings of length 2 were not profiled.

A separate scaling sweep uses Interval on eight generated program families.
For each family, we fit solve time $t$ against its size parameter $n$ as
$t = a n^b$ by least squares on logarithmic axes. We use successful timings
from $n=100$ to the largest completed size (500--2000, depending on the family). The fitted exponents range from \stat{prof.scaling.time_min} to
\stat{prof.scaling.time_max}. The
\href{https://github.com/ManuelLerchner/Voblint-Verification-Master-Thesis/blob/main/pages/data/profiling/2026-10-21-17fcb363d.json}{profiling snapshot}
records the measurements. The
\href{https://github.com/ManuelLerchner/Voblint-Verification-Master-Thesis/blob/main/scripts/profile_corpus.py}{profiling script}
defines the families. The
\href{https://manuellerchner.github.io/Voblint-Verification-Master-Thesis/profiling.html}{profiling page}
shows the runtime distributions and scaling curves. The scaling sweep exposes
costs hidden by the small regression fixtures; it establishes neither an
asymptotic bound nor performance on realistic large programs.