From 1540c49161fc4f9fc075d3fd978f682f8f041dac Mon Sep 17 00:00:00 2001
From: Nguyễn Gia Phong <cnx@loang.net>
Date: Tue, 12 Dec 2023 11:56:49 +0900
Subject: Proof read for the last time

---
 technique.tex | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

(limited to 'technique.tex')

diff --git a/technique.tex b/technique.tex
index af1fa92..63b7ea1 100644
--- a/technique.tex
+++ b/technique.tex
@@ -13,7 +13,7 @@ to generate \glspl{difftest}.  Third, the new conditions the combined
 are assertions on the distinction of corresponding values across revisions,
 so we offer multiple options to capture such \emph{\glspl{symout}}.
 
-Next, we introduces concrete execution to reduce the theorem proving load,
+Next, we introduce concrete execution to reduce the theorem proving load,
 and produce \glspl{difftest} for clustering the patches and finally produce
 a decision tree.  One may observe that the clustering information
 can help with selecting more ``promising'' states, although such scheduling
@@ -161,7 +161,7 @@ used for shadow symbolic execution.  Unlike \textsc{Shadow}
 which tests only one patch~\cite{shadow} to reveal its regressions, though,
 the goal of \psychic{} is to find the difference in behavior
 between multiple patches.  Therefore, the former's annotation
-at level of expressions does not meet our expectation on expressivity.
+at the level of expressions does not meet our expectation on expressivity.
 Instead, we implement higher-order branching.  Annotating patches
 at block level simplifies the generation process
 and improves the readability of the meta program.
@@ -195,7 +195,7 @@ and improves the readability of the meta program.
 
 For instance, given the two unified diffs~\cite{unidiff} of a bug fix
 from upstream \texttt{grep}, and a patch in \textsc{DBGBench}~\cite{dbgbench}
-in figure~\ref{grep-8f08d8e2},\footnote{The snippets have been outdented
+in figure~\ref{grep-8f08d8e2},\footnote{These snippets have been outdented
 to fit within the width of this page.} one can construct the relevant part
 of the meta program in figure~\ref{grep-8f08d8e2-meta}, where \verb|__klee_meta|
 parses the environment for the choice of revision when executed
@@ -227,7 +227,7 @@ if (__klee_meta(3) == \textcolor{purple}{0}) \verb|{|
 
 One may notice that the meta program may have any level of granularity.
 \psychic{} utilizes the meta program to maximize instructions
-and path constraints sharing, which effectively means to defer
+and path constraints that are shared, which effectively means to defer
 the divergence point deep into the control flow.  For its intended use
 on automatically generated patches whose hunks are commonly short,
 optimizing the meta program construction is not a major issue.
@@ -237,7 +237,7 @@ higher-order branching patch identifier, via basic tree pattern matching%
 ~\cite{tree-pattern} and skip adding its condition to the children states.
 Instead, those states carry the revision number outside
 of their path constraints for constant-time access when pruning paths
-going though multiple patches in algorithm~\ref{apply-meta}.
+going through multiple patches in algorithm~\ref{apply-meta}.
 
 \begin{algorithm}
   \caption{Construction of possible states after a patch location}
@@ -247,7 +247,7 @@ going though multiple patches in algorithm~\ref{apply-meta}.
       \State $n' \gets \Call{RevisionNumber}{\varphi}$
       \State $s_a = (i_a, e, \varPhi, n)$
         \Comment{assume the lack of meta branch nesting
-                 and always follow alternative path}
+                 and always follow alternative paths}
       \If{$n = 0$}
         \Return $\{(i_c, e, \varPhi, n'), s_a\}$
         \Comment{$i_c$ enters patch $n'$ }
@@ -288,7 +288,7 @@ or automatically~\cite{fl-eval}, output annotation has limited exhaustiveness.
 To balance between manual annotation and computational scalability,
 methods \ref{ret} and \ref{parg} are introduced to automatically capture output
 more precisely at the end of every interested function.  Debugging information
-forwarded from compiler frontend are kept in bitcodes, and they are used
+forwarded from compiler frontend are kept in bitcodes.  They are used
 to limit the subroutines to be monitored, for example in algorithm~\ref{fnout},
 the file that is patched by an \gls{apr} tool.
 
@@ -314,7 +314,7 @@ the file that is patched by an \gls{apr} tool.
   \end{algorithmic}
 \end{algorithm}
 
-Each \gls{symout} then is given an unique name for later comparison.
+Each \gls{symout} then is given a unique name for later comparison.
 For the sake of simplicity, we name them after the capturing method
 and associated identifier, i.e.~variable or subroutine.
 
@@ -328,7 +328,7 @@ and the conjunction of their path conditions is satisfiable.
 Currently \psychic{} only compare halt states to minimize memory usage
 and \gls{smt} solving cost.  Such \gls{smt} formula is constructed
 in algorithm~\ref{diffgen} by first append a suffix to each output name,
-then for the common ones assert for possible distinction between two paths.
+then for the common ones assert for a possible distinction between two paths.
 If the path constraints of both states are \gls{sat} with at least
 one difference in outputs, a \gls{difftest} can be generated
 from the \gls{smt} model.
@@ -384,4 +384,4 @@ From each \gls{difftest}, a set of clusters of revisions with the same output
 is constructed.  We then superimpose these clustering sets to create
 hierarchical clusterings or a decision tree.  A minimal tree, i.e.~a tree
 with the shortest height, is found by searching through the subsets
-of set of clustering sets.
+of the set of clustering sets.
-- 
cgit 1.4.1

