\section{Related Work}
\label{sec:related}

\subparagraph*{Concrete semantics of calling contexts.}
Sharir and Pnueli distinguish two approaches~\cite{sharir81}. The functional
approach computes input--output relations of procedures; the call-string
approach tags information with the history of calls.
Voblint's call-string policy follows the second, and its entry-state policy,
which indexes a callee's exit states by its entry state, resembles a
functional approach tabulated per input. Knoop and Steffen handle the locals of recursive procedures with
stacks of lattice elements; their maximal-fixpoint strategy uses stacks of
length at most two~\cite{knoop92}; Voblint's return has the shape of their return
function~\cite[§4.1]{knoop92}. Reps et al.\ compute precise solutions when
the set of dataflow facts is finite and the transfer functions are
distributive~\cite{reps95}. Voblint requires neither a finite domain nor
distributive transfer functions, but establishes no corresponding general
precision theorem. Jeannet and Serwe derive interprocedural analyses by abstract
interpretation of a standard stack-based operational semantics and combine the
call-string and functional approaches~\cite{jeannet04}. Van Horn and Might
derive sound analyses from abstract machines by bounding their
stores~\cite{vanhorn10}. These approaches relate analysis contexts to concrete
executions. In the a posteriori soundness framework of Might and
Manolios~\cite{might09}, a map from concrete to abstract resources
parameterizes the state abstraction. They construct a suitable map after
the analysis.
Voblint instead derives its entry-state context relation from the solution;
\oblig{Total} ensures that every call from a covered store admits a callee context
(\cref{sec:equations}).

\subparagraph*{Verified analyzers.}
Verasco is a Coq-verified analyzer for most of C99, excluding recursion and
dynamic allocation~\cite{jourdan15}. Its interpreter iterates over the
structure of C\#minor, reanalyzes a function at every call site, and raises an
alarm at a possible recursive call. Blazy et al.\ use a verified checker to
validate the candidate fixpoint produced by an untrusted
iterator~\cite{blazy13}. Nipkow and Klein develop
abstract interpretation for IMP in Isabelle/HOL~\cite{nipkow12,nipkow14}, and
Voblint's non-relational domains follow their generic interpreter. Like the
verified analyzers of Franceschino et al.~\cite{franceschino21} and Cachera and
Pichardie~\cite{cachera10}, Nipkow and Klein's IMP interpreter targets a language without procedures.
Michelland et al.\ derive concrete and abstract interpreters from a shared
monadic denotation and prove the abstract interpreter sound~\cite{michelland24}. Cachera
et al.\ compute a context-insensitive dataflow analysis with a verified solver
for ordinary inequations~\cite{cachera05}.

\subparagraph*{Contexts in mechanized semantics.}
Dabrowski and Pichardie prove a context-sensitive points-to analysis sound
in Coq~\cite{dabrowski09}. Their concrete semantics carries contexts through
a module type whose call-context function computes a callee's context.
This is the closest precedent for Voblint's context-indexed semantics. Their
development specifies the analyses as constraints but does not provide an
executable implementation~\cite[§7]{dabrowski09}. Voblint's
contexts are admitted by a relation, the totality condition makes the indexed
collection exhaustive, and the indexing is connected to an executable verified
solver. Trace partitioning indexes sets of traces by control
history~\cite{rival07}; Rival and Mauborgne allow coverings in which one trace
has several indices and present calling contexts as one such indexing. The
activation collecting semantics is a covering of this relational kind. Among
Isabelle developments, Lammich and Müller-Olm verify the soundness and
precision of a conflict analysis for programs with procedures and
threads~\cite{lammich07afp}, and Breitner formalizes Shivers' control-flow
analysis for functional programs~\cite{breitner10afp}. Wasserrab proves
correctness of interprocedural slicing, which removes statements irrelevant
to selected observations, by weak simulation~\cite{wasserrab09afp}.
This preserves slicing observations; Voblint instead bounds reachable stores.

\subparagraph*{Verified solvers.}
Hofmann et al.\ verify a local generic solver in Coq~\cite{hofmann10}, and de
Vilhena et al.\ verify one that discovers dependencies dynamically in
Iris~\cite{devilhena20}. Stade et al.\ prove the top-down solver partially
correct in Isabelle/HOL~\cite{stade24}, and Tilscher et al.\ extend it to side
effects with a generic interface for update rules~\cite{tilscher26}. Voblint
reuses this solver formalization. Their termination theorem for the solver
with widening and narrowing in phases assumes finitely many
unknowns~\cite{tilscher26jar}. Voblint does not establish this condition
for entry-state contexts.

\subparagraph*{Goblint and local traces.}
Side-effecting constraint systems~\cite{seidl03,apinis12} and the split
between analyses and solvers are Goblint's architecture~\cite{vojdani16,seidl26},
and Voblint's \isaname{dg_spec} follows its \texttt{Spec} interface.
Voblint's theorems do not establish soundness of Goblint's OCaml implementation.
Schwarz et al.\ prove
Goblint's thread-modular analyses sound against local traces on
paper~\cite{schwarz21,schwarz23}. Activation traces adapt this construction
to sequential procedure activations; the adaptation establishes no concurrency result.