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