Using AProVE in Practice

In the following page you can find all the different input formats that AProVE can parse and analyze. Moreover, we explain how to use AProVE's command line interface and what flags you can use.

Supported Input Formats

The following is a list of all programming languages AProVE can analyze and their input syntax. It is split into the frontend languages, i.e., languages that users write their software in, and the backend languages, i.e., analysis-oriented representations designed specifically for automated reasoning.

Frontend Languages

Java

AProVE is able to analyze many java programs including recurive algorithms.
Important Limitation:

Java numeric types are treated as unbounded mathematical integers.

Can only handle a restricted number of Java Libraries and no multithreading support.

Cannot handle floating-point arithmetic.

Possible input format: *.jar – Jar files containing a single main function.

Example Java code that can be used as input

/**
 * This class represents a list. The function get(n) can be used to access
 * the n-th element.
 * @author Marc Brockschmidt
 */
public class CyclicList {
    /**
     * A reference to the next list element.
     */
    private CyclicList next;

    public static void main(String[] args) {
        CyclicList list = CyclicList.create(args.length);
        list.get(args[0].length());
    }

    /**
     * Create a new list element.
     * @param n a reference to the next element.
     */
    public CyclicList(final CyclicList n) {
        this.next = n;
    }

    /**
     * Create a new cyclical list of a length l.
     * @param l some length
     * @return cyclical list of length max(1, l)
     */
    public static CyclicList create(int x) {
        CyclicList last, current;
        last = current = new CyclicList(null);
        while (--x > 0)
            current = new CyclicList(current);
        return last.next = current;
    }

    public CyclicList get(int n) {
        CyclicList cur = this;
        while (--n > 0) {
            cur = cur.next;
        }
        return cur;
    }
}

LLVM

AProVE is able to analyze llvm programs dealing with data structures like lists and integers. The main function without arguments is analyzed for termination.
Possible input format: *.llvm – LLVM files containing a single main function.

Example *.llvm Input

; ModuleID = 'cstrlen.c'
target datalayout = "e-m:o-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128"
target triple = "x86_64-apple-macosx10.15.0"
; Function Attrs: noinline nounwind optnone ssp uwtable

define i32 @cstrlen(i8* %0) {
  %2 = alloca i8*, align 8
  %3 = alloca i8*, align 8
  store i8* %0, i8** %2, align 8
  %4 = load i8*, i8** %2, align 8
  store i8* %4, i8** %3, align 8
  br label %5

5:                                                ; preds = %10, %1
  %6 = load i8*, i8** %3, align 8
  %7 = load i8, i8* %6, align 1
  %8 = sext i8 %7 to i32
  %9 = icmp ne i32 %8, 0
  br i1 %9, label %10, label %13

10:                                               ; preds = %5
  %11 = load i8*, i8** %3, align 8
  %12 = getelementptr inbounds i8, i8* %11, i32 1
  store i8* %12, i8** %3, align 8
  br label %5

13:                                               ; preds = %5
  %14 = load i8*, i8** %3, align 8
  %15 = load i8*, i8** %2, align 8
  %16 = ptrtoint i8* %14 to i64
  %17 = ptrtoint i8* %15 to i64
  %18 = sub i64 %16, %17
  %19 = trunc i64 %18 to i32
  ret i32 %19
}
; Function Attrs: noinline nounwind optnone ssp uwtable
define i32 @main() {
  %1 = alloca i32, align 4
  %2 = alloca i32, align 4
  %3 = alloca i8*, align 8
  store i32 0, i32* %1, align 4
  %4 = call i32 @__VERIFIER_nondet_int()
  store i32 %4, i32* %2, align 4
  %5 = load i32, i32* %2, align 4
  %6 = icmp slt i32 %5, 1
  br i1 %6, label %7, label %8

7:                                                ; preds = %0
  store i32 1, i32* %2, align 4
  br label %8

8:                                                ; preds = %7, %0
  %9 = load i32, i32* %2, align 4
  %10 = sext i32 %9 to i64
  %11 = mul i64 %10, 1
  %12 = alloca i8, i64 %11, align 16
  store i8* %12, i8** %3, align 8
  %13 = load i8*, i8** %3, align 8
  %14 = load i32, i32* %2, align 4
  %15 = sub nsw i32 %14, 1
  %16 = sext i32 %15 to i64
  %17 = getelementptr inbounds i8, i8* %13, i64 %16
  store i8 0, i8* %17, align 1
  %18 = load i8*, i8** %3, align 8
  %19 = call i32 @cstrlen(i8* %18)
  ret i32 %19
}
declare i32 @__VERIFIER_nondet_int()

C

AProVE is able to analyze C programs dealing with data structures like lists and integers. These are compiled to LLVM programs using Clang and then analyzed as described above.
Possible input format: *.c – C files containing a single main function.

Example *.c Input

extern int __VERIFIER_nondet_int(void);

int cstrlen(const char *s) {
    const char *p = s;
    while (*p != '\0')
        p++;
    return (int)(p - s);
}

int main() {
    int length = __VERIFIER_nondet_int();
    if (length < 1) {
        length = 1;
    }
    char* nondetString = __builtin_alloca(length * sizeof(char));
    nondetString[length-1] = '\0';
    return cstrlen(nondetString);
}

Prolog

AProVE is able to analyze prolog programs given an additional query that we want to analyze in terms of termination.
Possible input format: *.pl – Prolog file.

Example *.pl Input

%query: append(b,f,f)
append([],L,L).
append([X|Xs],Ys,[X|Zs]) :- append(Xs,Ys,Zs).

Haskell

AProVE is able to analyze haskell programs, e.g., from 1676 functions from the Haskell Prelude, and AProVE shows termination of 1294 of them.
Important Limitation: The Int type is treated as unbounded mathematical integers.
Possible input format: *.hs – Prolog file.

Example *.hs Input

{-# htermination (foldr1 :: (a -> a -> a) -> (List a) -> a) #-}


import qualified Prelude


data MyBool = MyTrue | MyFalse

data List a = Cons a (List a) | Nil


foldr1 :: (a -> a -> a) -> (List a) -> a

foldr1 f (Cons x Nil) = x

foldr1 f (Cons x xs) = f x (foldr1 f xs)

Backend Languages

Term Rewrite Systems

Term rewriting is a very basic functional programming language based on pattern matching. It is mostly used as a backend language to analyze other programming languages that are used by real developers. But it has also applications in equational reasoning, for computer algebra systems, etc.
Possible input formats:

*.ari – ARI format currently used in the termination competition.
*.xml – XML format previously used in the termination competition.
*.trs – TRS format previously used in the termination competition.
*.tes – AProVE's own human-readable TRS format.

There are many different extensions of term rewrite systems, e.g., equational rewriting, contextsensitive rewriting, rewriting with respect to a specific evaluation strategy like innermost rewriting, etc. One can analyze different properties of term rewrite systems like upper bounds on the runtime complexity as well. All of these extensions can be represented by this uniform input format and the details are explained in the respective documentations of the input formats. For example, the help page for the TRS format explains how all the additional information can be integrated into the input file of type *.trs.

Example cli command to analyze termination of a term rewrite system using the aprove.jar:

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

Example *.ari Input

(format TRS)

(fun |0| 0)
(fun s 1)
(fun plus 2)

(rule (plus |0| y) y)
(rule (plus (s x) y) (s (plus x y)))

Example *.xml Input

TBA

Example *.trs Input

(VAR x y)
(GOAL COMPLEXITY)
(RULES
    plus(0,y) -> y
    plus(s(x),y) -> s(plus(x,y))
)

Example *.tes Input

[x,y]
plus(0,y) -> y
plus(s(x),y) -> s(plus(x,y))

String Rewrite Systems

String rewriting is the restriction of term rewriting where every function symbol takes exactly one argument. Since this leads to many unnecessary brackets, there exists additional input formats for string rewrite systems.
Possible input formats:

*.ari – ARI format currently used in the termination competition.
*.xml – XML format previously used in the termination competition.
*.srs – SRS format previously used in the termination competition.
*.ses – AProVE's own human-readable SRS format.

Once again, all possible extensions can be integrated into the input file. For example, the help page for the SRS format explains how all the additional information can be integrated into the input file of type *.srs.

Example *.ari Input

(format TRS)

(fun a 1)
(fun b 1)

(rule (a (b x)) (b (a (a x))))

Example *.xml Input

TBA

Example *.srs Input

(VAR x)
(RULES
    a(b(x)) -> b(a(a(x)))
)

Example *.ses Input

[x]
a(b(x)) -> b(a(a(x)))

Integer Term Rewrite Systems

Integer Term Rewrite Systems explanation
Possible input format: *.inttrs – Integer Term Rewrite Systems. Here, each line has the format f1(s1, ..., sn) -> f2(t1, ..., tm) [cond], where f1 and f2 are function symbols, s1, ..., sn, t1, ..., tm are arbitrary terms (in particular, t1, ..., tm can also be/contain arithmetic expressions in infix notation). Moreover, we require n > 0. The constraint cond is a conjunction of arithmetic expressions where the relations >=, <=, >, <, and = are allowed.

Example *.inttrs Input

outer(x, r) -> inner(1, 1, x, r) [ x >= 0 && r <= 100000]
inner(f, i, x, r) -> inner(f + i, i+1, x, r) [ i <= x ]
inner(f, i, x, r) -> outer(x - 1, r + f) [ i > x ]
g(cons(x, xs), y)   -> g(xs, y + 1)
h(xs, y)  -> h(cons(0, xs), y - 1) [y  > 0]

Integer Term Rewrite Systems 2

Integer Term Rewrite Systems explanation
Possible input format: *.itrs – Integer Term Rewrite Systems representing the variant of Integer Term Rewrite Systems described in our paper at RTA '09. In *.itrs files, arithmetic and free function symbols can be mixed arbitrarily and rewriting can take place at any position. However, the evaluation strategy is restricted to innermost rewriting. So the system f(x) -> g(f(x)) does not terminate as an *.itrs system, but it would terminate as an *.inttrs system, because there is no possible infinite sequence of root rewrite steps. In contrast, the system with the two rules f(g(x)) -> f(g(x)) and g(x) -> h(x) terminates as an *.itrs system due to the innermost strategy, but it does not terminate as an *.inttrs system, because there is an infinite sequence of top-level rewrite steps.

Example *.itrs Input

# "sum" example to illustrate Def. 1 in the RTA'09 paper
# "Proving Termination of Integer Term Rewriting"
(VAR x y)
(RULES
sum(x, y) -> sif(x >= y, x, y)
sif(TRUE, x, y) -> y + sum(x, y+1)
sif(FALSE, x, y) -> 0
)

Complexity Integer Term Rewrite Systems (CInt)

These represent integer Term Rewrite Systems for complexity analysis, cf. our paper at TACAS '14.
Possible input format: *.cint – Complexity Integer Term Rewrite Systems. Each line has the format f(s) -> Com_k(g₁(t₁), ..., g_k(t_k)) :|: cond , where

k is a natural number greater than 0,
Com_k is a k-ary function symbol
f, g₁, ..., g_k are function symbols that are not contained in {Com_1, Com_2, ...}
s is a vector of variables,
t₁, ..., t_k are vectors of arithmetic expressions in infix notation and
cond is a conjunction of arithmetic expressions.

Example *.cint Input

f(x) -> Com_2(f(x - 1), g(x)) :|: x > 0 && x < 100
g(x) -> Com_1(g(x - 1)) :|: x > 0

Command-Line Usage

To use aprove as a command line tool, download AProVE and install all important dependencies.

Basic command & CLI Flags

The most basic command to call AProVE on an example file example.ari is:

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

CLI Flags

-b – used to select bitvector semantics for C programs. If not set, all integers are treated as unbounded mathematical integers.
-C MODE – restricts AProVE in such a way that only certifiable techniques are applied.
Possible parameters for MODE:
- ceta prints a proof readable by the certifier ceta.
-m MODE – set the output format of the result in the very first line
Possible parameters for MODE:
- wst For termination analysis AProVE prints YES, NO, MAYBE, ERROR, or TIMEOUT.
  For complexity analysis AProVE prints WORST_CASE(f(n),g(n)) where f(n) and g(n) are lower and upper complexity bounds, respectively, or '?'.
- benchmark prints slightly more specific output, e.g., more specific complexity classes that are not supported in the termination competition.
- smtlib prints output for the SMTLIB2 frontend for the QF_NIA theory.
-p MODE – set the overall output format of AProVE
Possible parameters for MODE: plain, html, cpf lets AProVE print out proofs in HTML-, ASCII-, or CPF-format, respectively.
-q QUERY – specify a query, e.g., to analyze arbitrary methods or to provide information about the method's arguments.
-s PATH_TO_STRATEGY – may be used to use a custom strategy.
-t TIMEOUT – specifies the timeout in seconds.
-v MODE – sets the verbosity level of the ouput.
Possible parameters for MODE from highest to lowest level:
- SEVERE, WARNING, INFO, FINER, FINEST
-w NUM_THREADS – sets the number of threads.
-Z DIRECTORY_NAME – enables online-certification where problematic proof steps are logged in the given directory.

Call specific Entrypoints of AProVE

AProVE also provides an SMTLIB2 frontend for the QF_NIA theory. To access this frontend, one has to provide the input in SMTLIB2 format and use the following flags.
The flag -m OUTPUT_FORMAT lets AProVE print sat or unknown as a very first output, if smtlib is given as the format. Alternatively, wst may be used as above.
The flag -d diologic stands for Diophantine Logic and means QF_NIA. Here, the search space is determined by iterative deepening.
Alternatively, it is also possible to use -d dioconstraints for an input problem in CiME2 format, which uses a conjunction of (in)equalities and an explicit range to determine the search space.
To use AProVE in server mode, enter the command java -ea jar aprove.jar -u srv. Then, a client can open a network connection to port 5250 and dispatch queries of the following form:
Line 1 indicates the number of following lines. To specify both an input file and a timeout, enter 2 here.
Line 2 contains the path to the input file.
Line 3 specifies the timeout in seconds.
Run java -ea -cp aprove.jar aprove.CommandLineInterface.JBCFrontendMain to invoke the Java Bytecode front-end of AProVE, allowing to output (integer) term rewrite systems whose termination implies termination of the original program. A number of options exist (to configure the output directory and output format), and can be displayed with the command line option --help.
To run it on an example file example.jar, execute java -ea -cp aprove.jar aprove.CommandLineInterface.JBCFrontendMain example.jar. The default output are .inttrs (standard case) and .qdp (for problems that do not use any integers) files. Using the command line options, input files for the T2 termination analyzer can also be obtained instead.
To output the symbolic execution graph as a dot-file that can be processed by Graphviz, use the command line option -g true. To output the graph in json format, use the option -j true instead. Use -o DIR to specify the output directory, where the respective graph or rewrite systems are dumped.
Run java -ea -cp aprove.jar aprove.CommandLineInterface.HaskellFrontendMain to invoke the Haskell front-end of AProVE, allowing to output term rewrite systems whose termination implies termination of the original program. A number of options exist (to configure the output directory), and can displayed with the command line option --help.
To run it on an example file example.hs, execute java -ea -cp aprove.jar aprove.CommandLineInterface.HaskellFrontendMain example.hs. The output formats are .qdp files.
To output the symbolic execution graph as a dot-file that can be processed by Graphviz, use the command line option -g true. To output the graph in json format, use the option -j true instead. Use -o DIR to specify the output directory, where the respective graph or rewrite systems are dumped.
Run java -ea -cp aprove.jar aprove.CommandLineInterface.PrologFrontendMain to invoke the Prolog front-end of AProVE, allowing to output rewrite systems whose termination implies termination of the original program. A number of options exist (to configure the output directory), and can displayed with the command line option --help.
To run it on an example file example.pl, execute java -ea -cp aprove.jar aprove.CommandLineInterface.PrologFrontendMain example.pl. The output formats are .qdp files.
To output the symbolic execution graph as a dot-file that can be processed by Graphviz, use the command line option -g true. To output the graph in json format, use the option -j true instead. Use -o DIR to specify the output directory, where the respective graph or rewrite systems are dumped.
Run java -ea -cp aprove.jar aprove.CommandLineInterface.CFrontendMain to invoke the C front-end of AProVE, allowing to output term rewrite systems whose termination implies termination of the original program. A number of options exist (to configure the output directory), and can displayed with the command line option --help.
To run it on an example file example.c, execute java -ea -cp aprove.jar aprove.CommandLineInterface.CFrontendMain example.c. The output formats are .inttrs files.
To output the symbolic execution graph as a dot-file that can be processed by Graphviz, use the command line option -g true. To output the graph in json format, use the option -j true instead. Use -o DIR to specify the output directory, where the respective graph or rewrite systems are dumped.
Run java -ea -cp aprove.jar aprove.CommandLineInterface.LLVMFrontendMain to invoke the LLVM front-end of AProVE, allowing to output term rewrite systems whose termination implies termination of the original program. A number of options exist (to configure the output directory), and can displayed with the command line option --help.
To run it on an example file example.llvm, execute java -ea -cp aprove.jar aprove.CommandLineInterface.LLVMFrontendMain example.llvm. The output formats are .inttrs files.
To output the symbolic execution graph as a dot-file that can be processed by Graphviz, use the command line option -g true. To output the graph in json format, use the option -j true instead. Use -o DIR to specify the output directory, where the respective graph or rewrite systems are dumped.

AProVE GUI (Eclipse Plugin)

AProVE is available as a plug-in for the Eclipse software development environment. To install the AProVE GUI for Eclipse, please install all dependencies and then follow the instructions below:

Start Eclipse, go to the work bench (or main menu), and select Help → Install New Software....
Press the Add... button in the upper right corner and enter AProVE as the name and https://aprove-developers.github.io/aprove-eclipse-updatesite/ as the location.
You now see a category Verification. Expand it and select the AProVE GUI checkbox.
To install, press Next followed by Next. If you agree to our license, select I accept the terms of the license agreement and continue with Finish.
Finally, close the warning about unsigned data using the OK button and restart Eclipse by pressing Yes.
Select AProVE → Create example projects from the main menu. Feel free to ignore EGit related warning popups.

Interacting with proofs and the prover

A number of buttons in the "Proof Tree View" of the AProVE GUI allow to interact with the AProVE system in the background:

Icon Meaning

treerepr Switches between two different views of the proof tree.

treeswitch Switches between proof trees if AProVE was invoked several times.

stop Aborts a running analysis. The (unfinished) proof stays available.

CPF Saves the current proof as a CPF file.

CeTA Calls CeTA in order to certify the current proof. This requires an additional installation of CeTA.

remove Removes the current proof tree and its background process.

removeall Removes all proof trees and background processes.

Icon	Meaning
	Switches between two different views of the proof tree.
	Switches between proof trees if AProVE was invoked several times.
	Aborts a running analysis. The (unfinished) proof stays available.
	Saves the current proof as a CPF file.
	Calls CeTA in order to certify the current proof. This requires an additional installation of CeTA.
	Removes the current proof tree and its background process.
	Removes all proof trees and background processes.

Analyzing files outside a workspace

To analyze files outside of the current Eclipse workspace, one can create so-called launch configurations. By right-clicking in the project explorer and choosing either ''Run As'' or ''Run Configurations...'', and then double-clicking on ''AProVE Launch'', one can create a new launch configuration. This allows to select any file for termination analysis.