Download

Download

Remark: VeriLHyS can be used only for non-commercial or academic purposes. See License for details.

VeriLHyS is currently available as a python package.

!! This software relies on third-party tools (MATLAB, MOSEK) that require a valid license for use. It is the sole responsibility of the user to ensure that all necessary licenses are obtained and comply with the term of use of those third-party components. We do not assume any responsibility or liability for issues arising from the use of unlicensed or improperly licensed third-party software.

Python wheel package

VeriLHyS package is available here: verilhys_1.0.0.zip.

It includes a src folder containing the wheel python package (verilhys-1.0.0-py3-none-any.whl) of VeriLHyS and a data folder containing some configuration files and some MATLAB scripts.

To install it, first ensure you have Python and pip installed. Then, run the following command in your terminal:

1
pip install path/to/verilhys-1.0.0-py3-none-any.whl

Install cvc5 and z3 by running

1
pysmt-install --z3 --cvc5 --confirm-agreement

Download the following version of nuXmv:

1
2
wget https://es-static-lfs.fbk.eu/access/lbattista/nuXmv
chmod +x nuXmv

Notice that by downloading nuXmv you agree to the conditions of its license, available in the binary and at https://nuxmv.fbk.eu/ .

Then, set the following environment variables:

  • NUXMV_PATH: path to the downloaded executable of nuXmv
  • MOSEK_MATLAB_PATH: path to a valid installation of mosek
  • YALMIP_PATH: path to a valid installation of yalmip (folder YALMIP-master)
  • CORA_PATH: path to a valid installation of CORA
  • CORA_OURS_PATH: path to the data/CORA folder included in the VeriLHyS archive

As an example, on a Linux/macOS operating system, this is done via the following command:

1
export NUXMV_PATH=/path/to/nuXmv/executable

Dockerfile

In order to configure a valid environment for running VeriLHyS, we provide the following Dockerfile.

It is required that the user owns:

  • a mosek.lic valid license file for Mosek version 10 or newer
  • a license.lic valid license file for Matlab version R2025a

The MATLAB license file is related to a username and mac-address; in the following, we refer to them as <MATLAB_USERNAME> and <MATLAB_MAC_ADDRESS>, respectively.

To configure correctly the docker, run the following commands:

1
2
3
4
5
cd <CWD>
mv <MOSEK_LIC> licenses/mosek/mosek.lic
mv <MATLAB_LIC> licenses/MATLAB/license.lic
docker build --build-arg USER_NAME=<MATLAB_USERNAME> -t <IMAGE_NAME> .
docker run -it <IMAGE_NAME> --mac-address="<MATLAB_MAC_ADDRESS>"

A virtual environment containing all needed requirements is provided at path /python_venv; verilhys-1.0.0-py3-none-any.whl can then be installed using pip.