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

---
 bg.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'bg.tex')

diff --git a/bg.tex b/bg.tex
index b1845d4..f8b759f 100644
--- a/bg.tex
+++ b/bg.tex
@@ -9,7 +9,7 @@ At a high level, symbolic execution is an interpreter loop.
 Every iteration, it selects a symbolic process,
 also known as a \emph{\gls{state}}, in whose context an instruction
 is then executed~\cite{klee}.  As shown in algorithm~\ref{symb-exec},
-each path with possible \gls{sat} of the given program is explore.
+each path with possible \gls{sat} of the given program is explored.
 The number of paths grows at an exponential rate, so the interpreter loop
 also breaks at the exhaustion of the time budget~\cite{klee},
 which is omitted from the algorithm for brevity.
@@ -67,7 +67,7 @@ for files (including standard streams) and command-line arguments
 or via in-source annotations~\cite{klee-docs}.
 
 
-As shown in algorithm~\ref{symb-exec}, the path constraints is only expanded
+As shown in algorithm~\ref{symb-exec}, the path constraints are only expanded
 at branching instructions, so only values affecting the control flow
 are tracked, since \klee{} targets the exploration of execution paths.
 In~order to track other values of interest, i.e.~non-inputs, a condition
-- 
cgit 1.4.1

