From a8bb7736e2e86963bd5761cc05079447abeeaba6 Mon Sep 17 00:00:00 2001 From: ericmarin Date: Tue, 23 Jun 2026 15:26:01 +0200 Subject: using official template + fixing language errors --- chapters/core/implementation/04-python-module.tex | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'chapters/core/implementation/04-python-module.tex') 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} -- cgit v1.2.3