diff options
Diffstat (limited to 'chapters/core/implementation/04-python-module.tex')
| -rw-r--r-- | chapters/core/implementation/04-python-module.tex | 6 |
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 a40df41..6023c2e 100644 --- a/chapters/core/implementation/04-python-module.tex +++ b/chapters/core/implementation/04-python-module.tex @@ -1,8 +1,8 @@ \subsection{Python Module} \label{sec:python-module} -The core functionality of the VEIN system is implemented via the \texttt{vein.Solver}, an extension of -the \texttt{z3.Solver} class offered in the Z3 python +The core functionality of the \textbf{VEIN} system is implemented via the \texttt{vein.Solver}, an extension of +the \texttt{z3.Solver} class offered in the Z3 Python package\footnote{\href{https://pypi.org/project/z3-solver}{\textbf{PyPi package}}}. This design choice ensures flexibility and ease of use for researchers already familiar with using the Z3 Python API. @@ -19,7 +19,7 @@ into a pending queue and it is reduced to normal form only after the \texttt{che 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 declaration, optional range +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) 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. |