1 files changed, 32 insertions, 0 deletions
diff --git a/glossary.tex b/glossary.tex
new file mode 100644
index 0000000..8f43f5f
--- /dev/null
+++ b/glossary.tex
@@ -0,0 +1,32 @@
+\makenoidxglossaries
+\newglossaryentry{difftest}{name={differential test},
+  description={Is an input and a collection of outputs of two or more programs
+    of the same purpose, such that each output is pairwise different}}
+\newglossaryentry{state}{name=state,
+  description={Or \emph{symbolic process}, includes a register file,
+    a stack frame, an address space for heap and global variables,
+    a program counter and path conditions.  Stack, heap and global variables
+    here are all symbolic expressions.  For our algorithm, the state
+    additionally contain the identifier of its program revision}}
+\newglossaryentry{pstates}{name={parallel states},
+  description={Two states are parallel if and only if their program counter
+    points to the same instruction\footnote{They do not necessarily
+    share the same program counter however.} and the conjunction
+    of their path conditions is satisfiable}}
+\newglossaryentry{searcher}{name=searcher,
+  description={Is what keeps track of states to be executed,
+    along with the information for scheduling them to optimize resources
+    on the progress of reaching the goal.  In this work, the searcher
+    includes a set of states and execution frontier tracking}}
+\newglossaryentry{execfront}{name={execution frontier},
+  description={An instruction $i$ is said to be an execution frontier
+    of the other $j$ if and only if there exists an execution path
+    in which the first occurrence of $i$ is before that of $j$.
+    In more relaxed terminologies, a state $s$ is said to be a frontier
+    of the other state $z$ if $s$'s program counter is a frontier of $z$'s}}
+\newglossaryentry{lexecfront}{name={local execution frontier},
+  description={Between a program's states, those not having a frontier
+    are called the local execution frontiers}}
+\newglossaryentry{gexecfront}{name={global execution frontier},
+  description={Between the states of multiple program's revisions,
+    those not having an frontier are called the global execution frontiers}}