1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
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}}
|
