\makenoidxglossaries
\newglossaryentry{bug}{name={bug},
  description={is a software defect that results in undesired behaviors}}
\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 pair-wise different}}
\newglossaryentry{state}{name=state,
  description={or \emph{symbolic process}, includes a program counter,
    an execution environment (a register file, a stack frame,
    and an address space for heap and global variables), and path constraints.
    Variables in an execution environment are all symbolic expressions}}
\newglossaryentry{symout}{name={symbolic output},
  description={is an output or intermediate value of a program
    under symbolic execution that reflects behaviors of the program
    relevant to the analysis}}
\newacronym{apr}{APR}{automated program repair}
\newacronym{ir}{IR}{intermediate representation}
\newacronym{sat}{SAT}{satisfiability}
\newacronym{smt}{SMT}{satisfiability modulo theories}
\newacronym{ffi}{FFI}{foreign function interface}
\newacronym{ub}{UB}{undefined behavior}
\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}}
