\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}}
