summaryrefslogtreecommitdiff
path: root/chapters/01-introduction.tex
diff options
context:
space:
mode:
authorericmarin <maarin.eric@gmail.com>2026-05-06 19:31:37 +0200
committerericmarin <maarin.eric@gmail.com>2026-05-07 17:08:23 +0200
commit66857fcce9159e98ec777a781d8b13b4f37c021d (patch)
tree71401450a9464d25e9ac1a1624bddbf1ce172a54 /chapters/01-introduction.tex
parent00439f8eacc04bee31dad6cb476d6f23f0b868dd (diff)
downloadvein-66857fcce9159e98ec777a781d8b13b4f37c021d.tar.gz
vein-66857fcce9159e98ec777a781d8b13b4f37c021d.zip
interaction rules subsection 3.1.2thesis
Diffstat (limited to 'chapters/01-introduction.tex')
-rw-r--r--chapters/01-introduction.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/chapters/01-introduction.tex b/chapters/01-introduction.tex
index 36919e5..a6a69c5 100644
--- a/chapters/01-introduction.tex
+++ b/chapters/01-introduction.tex
@@ -28,7 +28,7 @@ The tool is divided into three steps:
\item \textbf{Reduction}: the interaction net gets reduced to its normal form by Inpla;
\item \textbf{Evaluation}: the normal form gets processed along with the property to verify by Z3.
\end{itemize}
-Z3 is not optimized for ReLU splitting, but it was chosen for it's mature Python package.
+Z3 is not optimized for ReLU splitting, but it was chosen for its mature Python package.
In any case a specialized solver like Marabou can be integrated to improve performance.
Our contributions are:
\begin{itemize}