\section{Preliminaries}
Our \gls{difftest} generation is based on the symbolic executor
\textsc{klee}'s architecture, which at a high level is an interpreter loop.
At each iteration, it selects a symbolic process, also known as a \gls{state},
in whose context an instruction is then executed.

% TODO: base symb exec algo