\section{Conclusion}
\label{sec:conclusion}

We have connected the source semantics of VIMP to a Goblint-style analyzer
based on context-sensitive, side-effecting equations and a verified solver.
A returned report for an accepted configuration and a scalar VIMP program
covers reached stores at every program point. The report's definite verdicts hold
for those stores. Precision improvements have been shown for individual programs, but no general precision guarantee
is proved.

The report also preserves coverage within each context
(\cref{sec:theorem}).

\subparagraph*{Language extensions.}
The coverage contract abstracts over the language's step functions. Extending
VIMP with machine integers would require new concrete operations, abstract
transfers, and soundness proofs. A heap without pointers into caller frames
could be modeled by extending the store, again with new transfers and proofs.
Pointers into caller frames and interference from other threads would also
require revisiting the trace semantics, which assumes that a callee cannot
modify its caller's locals. These extensions remain future work.

\subparagraph*{Termination.}
Known termination results for top-down solvers assume finitely many
unknowns~\cite{tilscher26jar}. Entry-state context sets can be infinite, and
all timeouts in \cref{sec:evaluation} occur under this policy. Goblint controls
context creation through optional widening on contexts (\texttt{ana.context.widen})
or \emph{context gas}, a budget for context-sensitive calls along a call stack.
Establishing termination for Voblint would require controlling context
creation and satisfying the remaining solver termination conditions.