Using AProVE in Practice

This page lists all input formats that AProVE can parse and analyze, and explains how to use AProVE from the command line, from Docker, from your own Java code, and inside Eclipse. If you just want to try an example, use the web interface instead.

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 recursive algorithms.
Important Limitation:
  • Java numeric integer 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 pointer arithmetic and 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 pointer arithmetic and data structures like lists and integers. These are compiled to LLVM programs using Clang (see the dependencies) 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 (including features like the cut and negation) given an additional query that we want to analyze for termination.
    Important Limitation: The Integer type is treated as unbounded mathematical integers.
    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., AProVE shows termination of 1294 out of 1676 functions from the Haskell Prelude.
    Important Limitation: The Int type is treated as unbounded mathematical integers.
    Possible input format: *.hs – Haskell 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. We use it 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: There are many different extensions of term rewrite systems, e.g., equational rewriting, context-sensitive 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 these uniform input formats 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 *.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 
    <?xml version="1.0" encoding="UTF-8"?>
<?xml-stylesheet type="text/xsl" href="../../xml/xtcHTML.xsl"?>
<problem xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:noNamespaceSchemaLocation="../../xml/xtc.xsd" type="termination">
<trs>
<rules>
<rule>
<lhs>
<funapp>
<name>minus</name>
<arg>
<var>x</var>
</arg>
<arg>
<funapp>
<name>0</name>
</funapp>
</arg>
</funapp>
</lhs>
<rhs>
<var>x</var>
</rhs>
</rule>
<rule>
<lhs>
<funapp>
<name>minus</name>
<arg>
<funapp>
<name>s</name>
<arg>
<var>x</var>
</arg>
</funapp>
</arg>
<arg>
<funapp>
<name>s</name>
<arg>
<var>y</var>
</arg>
</funapp>
</arg>
</funapp>
</lhs>
<rhs>
<funapp>
<name>minus</name>
<arg>
<var>x</var>
</arg>
<arg>
<var>y</var>
</arg>
</funapp>
</rhs>
</rule>
<rule>
<lhs>
<funapp>
<name>quot</name>
<arg>
<funapp>
<name>0</name>
</funapp>
</arg>
<arg>
<funapp>
<name>s</name>
<arg>
<var>y</var>
</arg>
</funapp>
</arg>
</funapp>
</lhs>
<rhs>
<funapp>
<name>0</name>
</funapp>
</rhs>
</rule>
<rule>
<lhs>
<funapp>
<name>quot</name>
<arg>
<funapp>
<name>s</name>
<arg>
<var>x</var>
</arg>
</funapp>
</arg>
<arg>
<funapp>
<name>s</name>
<arg>
<var>y</var>
</arg>
</funapp>
</arg>
</funapp>
</lhs>
<rhs>
<funapp>
<name>s</name>
<arg>
<funapp>
<name>quot</name>
<arg>
<funapp>
<name>minus</name>
<arg>
<var>x</var>
</arg>
<arg>
<var>y</var>
</arg>
</funapp>
</arg>
<arg>
<funapp>
<name>s</name>
<arg>
<var>y</var>
</arg>
</funapp>
</arg>
</funapp>
</arg>
</funapp>
</rhs>
</rule>
</rules>
<signature>
<funcsym>
<name>minus</name>
<arity>2</arity>
</funcsym>
<funcsym>
<name>0</name>
<arity>0</arity>
</funcsym>
<funcsym>
<name>s</name>
<arity>1</arity>
</funcsym>
<funcsym>
<name>quot</name>
<arity>2</arity>
</funcsym>
</signature>
</trs>
<strategy>FULL</strategy>
<metainformation>
<originalfilename>./TRS/AG01/#3.1.trs</originalfilename>
</metainformation>
</problem>
    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 exist additional input formats for string rewrite systems.
    Possible input formats: Again, many 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 
    <?xml version="1.0" encoding="UTF-8"?>
<?xml-stylesheet type="text/xsl" href="../../xml/xtcHTML.xsl"?>
<problem xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xsi:noNamespaceSchemaLocation="../../xml/xtc.xsd" type="termination">
<trs>
<rules>
<rule>
<lhs>
<funapp>
<name>0</name>
<arg>
<funapp>
<name>0</name>
<arg>
<funapp>
<name>0</name>
<arg>
<funapp>
<name>0</name>
<arg>
<var>x1</var>
</arg>
</funapp>
</arg>
</funapp>
</arg>
</funapp>
</arg>
</funapp>
</lhs>
<rhs>
<funapp>
<name>0</name>
<arg>
<funapp>
<name>0</name>
<arg>
<funapp>
<name>0</name>
<arg>
<funapp>
<name>1</name>
<arg>
<var>x1</var>
</arg>
</funapp>
</arg>
</funapp>
</arg>
</funapp>
</arg>
</funapp>
</rhs>
</rule>
<rule>
<lhs>
<funapp>
<name>1</name>
<arg>
<funapp>
<name>0</name>
<arg>
<funapp>
<name>0</name>
<arg>
<funapp>
<name>1</name>
<arg>
<var>x1</var>
</arg>
</funapp>
</arg>
</funapp>
</arg>
</funapp>
</arg>
</funapp>
</lhs>
<rhs>
<funapp>
<name>0</name>
<arg>
<funapp>
<name>0</name>
<arg>
<funapp>
<name>1</name>
<arg>
<funapp>
<name>0</name>
<arg>
<var>x1</var>
</arg>
</funapp>
</arg>
</funapp>
</arg>
</funapp>
</arg>
</funapp>
</rhs>
</rule>
</rules>
<signature>
<funcsym>
<name>0</name>
<arity>1</arity>
</funcsym>
<funcsym>
<name>1</name>
<arity>1</arity>
</funcsym>
</signature>
</trs>
<strategy>FULL</strategy>
<metainformation>
<originalfilename>./SRS/Gebhardt/01.srs</originalfilename>
</metainformation>
</problem>
    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

    These represent Integer Term Rewrite Systems (ITRSs) for termination analysis, see our paper at RTA '09. We use them as a backend language to analyze, e.g., Java programs that contain both integers and data structures like lists.
    Possible input format: *.itrs –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
)

    Integer Rewrite Systems with Terms

    Integer Rewrite Systems with Terms (IRSwTs) are another backend language used for termination analysis of Java programs, see the system description of AProVE paper at JAR '17.
    Possible input format: *.inttrs – 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]


    Command-Line Usage

    To use AProVE as a command line tool, download aprove.jar and install the dependencies, or use the Docker image, which has everything preinstalled.

    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.

    Overriding Declarations of the Input File

    The following flags override declarations made inside an .ari file without editing it:
    • --goal GOAL (or -G) – overrides the analysis goal, e.g., termination, complexity, or (S)AST for probabilistic systems.
    • --rewrite-strategy STRATEGY (or -R) – overrides the rewrite strategy, e.g., full or innermost rewriting.
    • --startterm TERM (or -S) – overrides the restriction on start terms.
    The complete list of options is maintained on the Using the CLI wiki page.

    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 outputs 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 be 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 format 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 format 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 be 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 format 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 be 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 format 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.

    Docker

    The official Docker image bundles AProVE with all external tools it relies on, e.g., the SAT and SMT solvers and the backend solvers KoAT and LoAT, so AProVE runs in an isolated and reproducible environment without any further installation. It 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.

    How to obtain the image is described on the download page. How to run AProVE inside the container and how to use the benchmarking pipeline is explained in detail on the Benchmarking wiki page.

    Java API

    For developers who want to embed AProVE into their own Java applications, aprove.jar provides a programmatic API in the package aprove.api. Instead of writing input files, you construct (probabilistic) rewrite systems programmatically, configure a proof tree (timeout, strategy, certification options), and run it asynchronously. The analysis returns YES, NO, or MAYBE, and the proof can be retrieved in several formats, e.g., as plain text or HTML.

    Example: Termination of a Term Rewrite System

    The following program builds the TRS with the rules f(s(x)) → f(x) and f(0) → 0 and proves its termination. 
    import aprove.api.*;
import aprove.api.prooftree.*;
import aprove.verification.dpframework.BasicStructures.*;
import aprove.verification.oldframework.BasicStructures.*;

FunctionSymbol f    = FunctionSymbol.create("f", 1);
FunctionSymbol succ = FunctionSymbol.create("s", 1);
FunctionSymbol zero = FunctionSymbol.create("0", 0);
TRSVariable    x    = TRSVariable.createVariable("x");

TRSFunctionApplication lhs1 = TRSTerm.createFunctionApplication(f,
    TRSTerm.createFunctionApplication(succ, x));
TRSFunctionApplication rhs1 = TRSTerm.createFunctionApplication(f, x);
Rule stepRule = Rule.create(lhs1, rhs1);

TRSFunctionApplication zeroTerm = TRSTerm.createFunctionApplication(zero);
TRSFunctionApplication lhs2     = TRSTerm.createFunctionApplication(f, zeroTerm);
Rule baseRule = Rule.create(lhs2, zeroTerm);

AnalyzableProblemInput input = AproveApi.newInstance()
    .newTrsInput()
    .add(stepRule)
    .add(baseRule)
    .name("looped minus one")
    .build();

ProofTree tree = input.newProofTreeBuilder()
    .onlineCertificationPath(Optional.empty())
    .onlyCertifiableTechniquesIfPossible(false)
    .strategy(Optional.empty())
    .timeout(Timeout.positiveOrInfinite(60_000))
    .construct();

String result = tree.runAsync().get();
System.out.println(result); // "YES", "NO", or "MAYBE"
    For probabilistic term rewrite systems, use newPtrsInput(Goal) with a goal such as Goal.AST, Goal.SAST, or Goal.TERMINATION, and add ProbabilisticRules instead of Rules.

    Complete, runnable examples are contained in the source repository under src/aprove/api/examples/. The full reference is available on the Using the API wiki page.

    AProVE GUI (Eclipse Plugin)

    The AProVE GUI is a plug-in for the Eclipse software development environment. Installation instructions are on the Get AProVE page. After installing, select AProVE → Create example projects from the main menu to get a workspace with example inputs (EGit related warning popups can be ignored).

    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.

    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.