Get AProVE

AProVE is open source under the LGPL-2.1 license and can be used in five different ways. Pick the one that fits your use case.

🌐

Web Interface

Best for: trying a single example, teaching, a quick look at a proof.

No installation. Runs on our servers, result is shown in the browser.

Open web interface
🐳

Docker

Best for: reproducible experiments, benchmarking whole problem sets.

All solvers and backend tools come preconfigured in the image.

Docker instructions
>_

Command Line

Best for: scripted one-off analyses on your own machine.

Download aprove.jar, install the dependencies, run it on a file.

Download the jar
{ }

Java API

Best for: embedding AProVE into your own Java application.

Build rewrite systems programmatically and run the analysis asynchronously.

API overview
🧩

Eclipse Plug-in

Best for: interactive local use while developing the analyzed program.

Edit the input in the IDE and inspect the (partial) proof tree.

Install the plug-in

Docker – recommended for local use

The official Docker image contains AProVE together with all external tools it relies on, e.g., the SAT and SMT solvers Z3, Yices, SMT-RAT and MiniSat, and the backend solvers KoAT and LoAT. Nothing else has to be installed. The image is available on Docker Hub: 

docker pull jckassing/aprove

The container is the recommended way to run AProVE on your own machine and the basis of our benchmarking pipeline, which runs AProVE on whole problem sets in parallel and produces result summaries, runtime statistics, and optional certificates. You can also build the image yourself from the bench/ directory of the source repository. See the Benchmarking wiki page for a step-by-step guide.

Command Line: aprove.jar

AProVE is a Java application built for Java 25; install a Java 25 JDK first. Then download the latest release of aprove.jar and run it on an input file: 

java -ea -jar aprove.jar -m wst example.ari
View Releases All CLI flags

The jar contains AProVE itself, but not the external solvers. For termination analysis, install the SAT and SMT solvers listed below; for complexity analysis, additionally install the backend tools. Add each program to your PATH so that AProVE can find it. If you want to avoid this setup, use the Docker image instead. If you encounter problems or need older versions, please contact us.

Show dependencies and installation instructions

SAT and SMT Solvers, Backend Tools


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.
Linux On Debian and Ubuntu it suffices to install the minisat2 package. For other systems:
  • 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.
Linux
  • 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.
In any case, rename the resulting executable to loat and add its directory to your path environment as described below.


CoFloCo – Tool for complexity analysis

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


Miscellaneous


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.


Setting the path environment

AProVE calls the tools above by name, so the directory containing each executable has to be in your PATH.
Windows Open System Properties → Environment Variables, edit the variable Path and add the directory.
Linux / macOS Add a line such as export PATH="/path/to/tool/bin:$PATH" to your shell profile (e.g., ~/.bashrc or ~/.zshrc) and open a new terminal.

Java API

The API is part of aprove.jar. Add the jar to the classpath of your application and construct (probabilistic) rewrite systems programmatically instead of writing input files. The entry point is AproveApi.newInstance(); the analysis returns YES, NO, or MAYBE, and the proof can be retrieved as plain text or HTML.

Code example API wiki

Eclipse Plug-in

The AProVE GUI is a plug-in for the Eclipse IDE. It requires Java 25 and the same dependencies as the jar. To install it:

  1. Start Eclipse and select Help → Install New Software....
  2. Press Add..., enter AProVE as the name and the following URL as the location: 
    https://aprove-developers.github.io/aprove-eclipse-updatesite/
  3. Expand the category Verification and select the AProVE GUI checkbox.
  4. Press Next twice, accept the license, and press Finish.
  5. Confirm the warning about unsigned content with OK and restart Eclipse.
GUI manual

License

AProVE is open source and released under the GNU Lesser General Public License, version 2.1 (LGPL-2.1).