1 files changed, 7 insertions, 0 deletions
diff --git a/bg.tex b/bg.tex
new file mode 100644
index 0000000..6bc4638
--- /dev/null
+++ b/bg.tex
@@ -0,0 +1,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