From 1540c49161fc4f9fc075d3fd978f682f8f041dac Mon Sep 17 00:00:00 2001 From: Nguyễn Gia Phong 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