summary refs log tree commit diff homepage
path: root/bg.tex
blob: 6bc4638cd4f1cdc93e49af04f056faa278941dd1 (plain) (blame)
1
2
3
4
5
6
7
\section{Background}
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~\cite{klee}.

% TODO: base symb exec algo