How to Run AProVE: Web Interface, Docker, API, and CLI

With AProVE now open source, we want to make it as easy as possible to run AProVE in your own environment. Depending on whether you just want to try a quick example or integrate AProVE into a larger development process or application, different options fit best. In this post we take a closer look at four of them: the web interface, the official Docker container, the new programmatic API, and the command line interface.

The Quickest Start: The Web Interface

The easiest way to get started with AProVE is our web interface. It requires no installation at all: simply paste or upload your input, pick the language and analysis goal, and let AProVE run on our servers. The results are rendered directly as html in your browser. This makes the web interface ideal for trying out a single example, for teaching, or for quickly inspecting why AProVE returns a particular output, without committing to a local setup.

Reproducible Benchmarking with Docker

In our previous post we promised to cover the Docker container in more detail — so here it is. The container lets you run AProVE in a fully isolated and reproducible environment, without having to worry about installing external tools such as z3, minisat, or loat, which all come pre-configured inside the image.

As promised, an up-to-date image is now also available on Docker Hub, so getting started is as easy as a single pull:

docker pull jckassing/aprove

Alternatively, you can load a prebuilt image with docker load -i image.tar, or build it yourself from the bench/ directory via docker build -t aprove_solver:some_ID .. Once the image name is set in the configuration (e.g. IMAGE="jckassing/aprove"), the benchmark script handles the Docker invocation for you and runs AProVE across whole problem sets in parallel. The pipeline produces detailed reports including result summaries, runtime analysis, and optional CPF3 certificate outputs. A step-by-step guide can be found in the Benchmarking wiki page.

Tool Integration with the New API

For developers who want to build AProVE directly into their own Java applications, we now provide a programmatic API. Instead of writing and parsing .ari files by hand, you construct rewriting problems programmatically.

The entry point is a single call, AproveApi.newInstance(), from which you build either a term rewrite system (newTrsInput()) or a probabilistic term rewrite system (newPtrsInput(Goal), with goals such as AST, SAST, or TERMINATION). After adding your rules, you configure a proof tree (setting timeout, strategy, and certification options) and run it asynchronously via tree.runAsync(), which returns a CompletableFuture resolving to YES, NO, or MAYBE. Proof details can additionally be retrieved in several formats, including plain text and HTML. The full reference, including complete examples, is available on the Using the API wiki page.

Scripting with the Command Line Interface

Finally, the command line interface is the most direct way to run AProVE on a single file from a terminal or a shell script. In its simplest form, you invoke the JAR directly:

java -ea -jar aprove.jar -m wst example.ari

A range of flags lets you tailor the analysis to your needs. The most common ones are:

• -m MODE: selects the result format, e.g. wst (YES / NO / MAYBE), benchmark for complexity classes, or smtlib
• -p MODE: chooses the proof output format (plain, html, or cpf)
• -t TIMEOUT and -w NUM_THREADS: control the timeout (in seconds) and the number of threads
• -s PATH_TO_STRATEGY: applies a custom analysis strategy
• -C MODE: restricts the analysis to certifiable techniques, e.g. producing output for the CeTA certifier

You can also override declarations made inside the input file without editing it, for instance switching the analysis goal (--goal), the rewrite strategy (--rewrite-strategy), or the start terms (--startterm). In addition, dedicated front-ends such as CFrontendMain, JBCFrontendMain, or HaskellFrontendMain provide tailored entry points for analyzing programs written in specific languages. For all available options, see the Using the CLI wiki page and our usage page.

Which One Should You Use?

As a rule of thumb: use the web interface to quickly try out a single example without any setup, the CLI for scriptable one-off analyses on your own machine, the API when you want to embed AProVE into a larger Java application, and the Docker container whenever reproducibility and large-scale benchmarking matter. Together, these options should cover virtually every way you might want to interact with AProVE.

— The AProVE Team