diff options
Diffstat (limited to 'bg.tex')
| -rw-r--r-- | bg.tex | 4 |
1 files changed, 2 insertions, 2 deletions
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 |