diff options
Diffstat (limited to 'glossary.tex')
| -rw-r--r-- | glossary.tex | 25 |
1 files changed, 14 insertions, 11 deletions
diff --git a/glossary.tex b/glossary.tex index 8f43f5f..1134321 100644 --- a/glossary.tex +++ b/glossary.tex @@ -1,18 +1,21 @@ \makenoidxglossaries \newglossaryentry{difftest}{name={differential test}, - description={Is an input and a collection of outputs of two or more programs + 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}} + 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} \newglossaryentry{searcher}{name=searcher, description={Is what keeps track of states to be executed, along with the information for scheduling them to optimize resources |