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