Prettify

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