Download AProVE

Z3 – SMT solver

Please visit https://github.com/Z3Prover/z3/releases to download Z3 (version >= 4.4.0).
Windows For Windows pre-compiled binaries are available. After extracting the files, please make sure to add the Z3 bin sub-directory (e.g., C:\Program Files\z3\bin\) to your path environment as described below. Furthermore, the file libz3java.dll in the bin sub-directory has to be copied to z3java.dll.
Linux For Linux please download the source code, then compile and install it as described in the README file. In addition, you have to pass the option --java to scripts/mk_make.py to build Z3's Java bindings. Alternatively, you can download pre-compiled binaries from https://github.com/Z3Prover/z3/releases. To do so, you have to select ''Planned'' in the section ''OTHER DOWNLOADS'' on the right. Afterwards, please make sure to add the Z3 sub-directory containing the executable z3 to your path environment as described below. Furthermore, the folder containing the file libz3java.so has to be added to the environment variable LD_LIBRARY_PATH. This works similar to setting the path environment (see below).

Yices 1 – SMT solver

AProVE works with Yices 1 (e.g., Yices 1.0.40 released December 4, 2013), but not Yices 2. (Yes, that is definitely a pity and we will update this outdated dependency in the future.) Please download Yices 1 from https://yices.csl.sri.com/old/download-yices1.html. After extracting the files, please make sure to add the yices bin sub-directory (e.g., C:\Program Files\yices-1.0.40\bin\ or /home/username/yices-1.0.40/bin/) to your path environment as described below. Moreover, please make sure that this sub-directory appears before any other directory (e.g., /usr/local/bin) that would contain another Yices binary.

MiniSat – SAT solver

To run AProVE, you need to install MiniSat version 2 or higher (due to licensing issues we are not allowed to provide a download on our own).
Windows

• Download and install Cygwin from https:/www.cygwin.com.
• Re-run setup.exe and select the following packages:
  • Devel → make
  • Devel → zlib-devel
  • Devel → gcc-g++
• Download and unzip https://minisat.se/downloads/minisat2-070721.zip to your Cygwin installation directory (default is C:\cygwin).
• Start the Cygwin Terminal and type the following commands:
  • cd /minisat/simp/ (if this does not work, try cd /minisat2-070721/minisat/simp/)
  • make rs
  • mv minisat_static.exe /bin/minisat.exe
  • exit
• Add the bin subdirectory of your Cygwin installation directory (default is C:\cygwin\bin) to the path environment variable as described below.

• Make sure that make and the developer version of zlib are installed on your sytem.
• Download https://minisat.se/downloads/minisat2-070721.zip and unzip it.
• Inside the minisat/simp directory, run make rs.
• Rename the resulting file minisat_static to minisat and add its directory to your path environment as described below.

KoAT – Tool for complexity analysis

To be able to prove upper bounds on the complexity of Integer Transition Systems from the GUI, one needs to install the tool KoAT. Moreover, KoAT is used by some complexity analysis techniques for classical Term Rewriting.
Windows

• A pre-compiled binary of KoAT is available here.
• Add its directory to your path environment as described below.

• Please checkout KoAT from github. Install KoAT according to the supplied instructions.
• Rename the resulting executable to koat and add its directory to your path environment as described below.

LoAT – Tool for complexity analysis

To be able to prove lower bounds on the complexity of Integer Transition Systems from the GUI, one needs to install the tool LoAT. Currently, LoAT does not support Windows.
Linux

• The recommended way to install LoAT is to download the pre-compiled binary for Linux/x64.
• Alternatively, checkout LoAT from github. Install LoAT according to the supplied instructions.

CoFloCo – Tool for complexity analysis

Some complexity analysis techniques for Term Rewriting require CoFloCo. Please follow the installation instructions from the CoFloCo website.

CeTA – Certification tool for termination and complexity proofs

In order to invoke CeTA from the GUI one needs to install CeTA (version >= 2.22). It is available at https://cl-informatik.uibk.ac.at/software/ceta/, where both precompiled binaries and the sources are available. To compile CeTA you additionally need to install the Glasgow Haskell Compiler.

Clang – Needed for C analysis

To be able to analyze C Programs, one needs to install Clang 2.9. To do so, please download and install the suitable precompiled binary of Clang 2.9, which is available here. Newer version of Clang up to and including Clang 3.5 should also work, but we cannot guarantee this.

For Windows, please download the Clang 2.9 Binaries for Mingw32/x86. To obtain the C standard libraries, we also recommend to download MinGW and to select at least the package "mingw32-base" during its installation. The resulting C standard libraries are then written to the directory "C:\MinGW\include". If needed, this directory can be extended by additional directories (e.g., from here).

Graphviz – Graph rendering

In order to view graphs inside the GUI, please also download and install the Graphviz tools (containing dot) from https://www.graphviz.org/. For Debian and Ubuntu it suffices to install the graphviz package.