using official template + fixing language errorsthesis

1 files changed, 3 insertions, 3 deletions

diff --git a/chapters/core/implementation/04-python-module.tex b/chapters/core/implementation/04-python-module.tex
index 6023c2e..ab817c4 100644
--- a/chapters/core/implementation/04-python-module.tex
+++ b/chapters/core/implementation/04-python-module.tex
@@ -15,14 +15,14 @@ The methods offered by \texttt{vein.Solver} are:
 \end{itemize}
 
 The framework uses a \textit{lazy evaluation} strategy: when loading a neural network, it is placed
-into a pending queue and it is reduced to normal form only after the \texttt{check} method is
+into a pending queue, and it is reduced to normal form only after the \texttt{check} method is
 called.
 
 The specification follows the SMT-LIB\footnote{\href{https://smt-lib.org}{\textbf{SMT-LIB Website}}}
 format. It should contain the input and output symbolic variables declarations, optional range
-constraints on the input variables and the properties to be verified. For Multi-Network (relational)
+constraints on the input variables, and the properties to be verified. For Multi-Network (relational)
 verification, the system ensures that multiple networks share the same input symbolic variables.
-This approach allows Z3 to compare their outputs directly given the same inputs.
+This approach allows Z3 to compare the outputs directly, given the same inputs.
 
 The execution pipeline is implemented within the \texttt{check} method:
 \begin{itemize}