blob: e2dfea3e6fd4050526024baa62f731ac73f7d9a3 (
plain) (
blame)
1
2
3
4
5
6
7
|
\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
|
