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-06-26 09:57:03 +0200
commit95d48c4a13fe8716cd38e5a076a54b68c8223dd1 (patch)
tree71401450a9464d25e9ac1a1624bddbf1ce172a54 /chapters/01-introduction.tex
parenta3411c1561690d13e376498a5f560abf2ca2c371 (diff)
downloadvein-95d48c4a13fe8716cd38e5a076a54b68c8223dd1.tar.gz
vein-95d48c4a13fe8716cd38e5a076a54b68c8223dd1.zip
interaction rules subsection 3.1.2
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}