Download

Supported Input Formats:

• *.xml files representing Term Rewrite Systems in XML format, as documented on the website of the Termination Competition.
  
  
• *.trs files representing Term Rewrite Systems in human-readable format, as documented on the (previous) website of the Termination Competition.
  
  
• *.pl files representing Prolog programs, using the Termination Competition format.
  
  
• *.hs files representing Haskell programs, using the Termination Competition format.
  
  
• *.jar files representing Java programs, using the Termination Competition format. In addition, Java 7 programs are allowed as well. In the GUI, one can also analyze individual methods with fine-grained control over the shapes of the data objects in the input arguments.
  
  
• *.inttrs files representing 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. Hence, an example system looks like this:

  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]
  

  Their semantics are defined by standard (constraint) top-level term rewriting. A rule l -> r [c] can be applied to a term t if there is a substitution σ such that lσ = t and cσ are valid in integer arithmetic. Thus, pre-defined arithmetic operations can always be evaluated, but rewriting is only allowed at the root position. Hence, defined subterms introduced in a right-hand side of a rule below the root are not evaluated. The application then results in the term rσ.
  
  Proving termination for Integer Term Rewrite Systems delegates to existing techniques. For this, integer/term parts of the problem are filtered away, allowing to treat it like a pure TRS/integer system problem.
  
  
• *.itrs files 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.
  
  
• *.cint files representing Integer Term Rewrite Systems for complexity analysis, cf. our paper at TACAS '14. Here, 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.
  Hence, an example system looks like this:

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

  Their semantics is similar to *.inttrs files, but rewriting is not only allowed at the root position, but at every position.
  
  
• *.llvm files representing LLVM programs. The main function without arguments is analyzed for termination.
  
  
• *.c files representing C programs. These are compiled to LLVM programs using Clang and then analyzed as described above.

Limitations

• Similar to many other termination provers, AProVE does not consider the finite-bitvector semantics of numeric Java types like long, int, short, ... but treats them as the infinite set of all mathematical integers. For executions which do not involve integer overflows, a termination (dis)proof by AProVE corresponds to the actual Java semantics.
• The restrictions used for the termination competition also imply that only selected libraries shipped with the Java Runtime Environment may be used, and all other Java Bytecode libraries (e.g., java.util.*) must be given explicitly by the user). Moreover, multi-threading is not supported.
• AProVE currently cannot prove termination of Java Bytecode programs whose termination is due to floating-point arithmetic. Predicates on such values are abstracted away.
• Similar to Java, the Haskell type Int is treated as the infinite set of all mathematical integers.

AProVE GUI as Eclipse plug-in:

• 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

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

AProVE Command-Line Version

• To prove termination for a given input file example, run java -ea -jar aprove.jar -m wst example.
  The flag -m wst is used so that AProVE prints YES, NO, MAYBE, or TIMEOUT as a very first output.
  The flag -p html, -p plain, or -p cpf lets AProVE print out proofs in HTML-, ASCII-, or CPF-format.
  The flag -C ceta restricts AProVE in such a way that only certifiable techniques are applied.
  The flag -Z directory_name enables online-certification where problematic proof steps are logged in the given directory.
  The flag -v specifies the logging level. The levels from highest to lowest are SEVERE, WARNING, INFO, CONFIG, FINE, FINER, and FINEST.
  The flag -s PATH_TO_STRATEGY may be used to apply a custom strategy.
  The flag -t TIMEOUT specifies the timeout in seconds.
  The flag -w NUM_THREADS sets the number of threads.
  The flag -q QUERY is used to specify a query, e.g., to analyze arbitrary methods or to provide information about the method's arguments.
  The flag -b is used to select bitvector semantics for C programs. If not set, all integers are treated as unbounded mathematical integers.
• 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.

Installing dependencies:

• Java 8
  AProVE is a Java application and needs the Java 8 Development Kit to run. Download and install the current version of the Java JDK. Please make sure to install the JDK, as the JRE does not suffice.
• Eclipse
  To use the GUI, download and install the current version (at least 4.5.0) of Eclipse. The package Eclipse IDE for Java Developers is a good choice, but most other packages work as well. Installing the AProVE GUI also works with an already existing (current) Eclipse installation.
• Graphviz
  In order to view graphs inside the GUI, please also download and install the Graphviz tools (containing dot) from http://www.graphviz.org/. For Debian and Ubuntu it suffices to install the graphviz package.
  
• CeTA
  In order to invoke CeTA from the GUI one needs to install CeTA (version >= 2.22). It is available at http://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, which is included in the Haskell Platform. After installing CeTA, please make sure that ceta is accessible, by adjusting your path environment as described below.
  
• Satisfiability checkers
  For (non)termination proofs you also need the satisfiability checkers Z3, Yices, and MiniSat:
  
  
  • Z3
    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
    AProVE works with Yices 1 (e.g., Yices 1.0.40 released December 4, 2013), but not Yices 2. 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
    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 http:/www.cygwin.com.
    • Re-run setup.exe and select the following packages:
      • Devel → make
      • Devel → zlib-devel
      • Devel → gcc-g++
    • Download and unzip http://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 http://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
  To be able to prove upper bounds on the complexity of Integer Term Rewrite 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 for Windows 7, 64 bit, 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
  To be able to prove lower bounds on the complexity of Integer Term Rewrite 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
  Some complexity analysis techniques for Term Rewriting require CoFloCo. Please follow the installation instructions from the CoFloCo website.
  
  
• Clang
  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).
  
  
• Path environment
  Extending your path environment is necessary so that AProVE is able to find the corresponding programs.
  • Windows: Please follow the instructions on http://www.computerhope.com/issues/ch000549.htm. After adding an entry, please restart Eclipse.
  • Linux: In case you run bash, please follow the instructions on http://www.troubleshooters.com/linux/prepostpath.htm. For other shells please consult the corresponding man page. After adding an entry, please logout and login again (or reboot your system).

"APROVE" SOFTWARE LICENSE AGREEMENT

Nonexclusive Binary Code License

Please read the terms and conditions of this software license agreement ("LICENSE") prior to downloading the AProVE software. By downloading you agree to be bound by the terms of this LICENSE.

1. General
   The AProVE software and accompanying documentation, whether on disk, in read only memory, on any other media or in any other form, are licensed, not sold, to you by RWTH Aachen University. Accepting this nonexclusive license from RWTH Aachen University will permit you to download a copy of the AProVE program code in binary format ("APROVE") and the related documentation ("DOCUMENTATION") and to use the copy of the code and documentation in accordance with the following terms and conditions. RWTH Aachen University retains ownership of APROVE and DOCUMENTATION itself, which is protected by copyright law.
2. Use and Transfer of the Software
   This LICENSE allows you to install and use copies of APROVE on your computer(s). You may not decompile, reverse engineer, disassemble or modify APROVE or parts thereof. Parts of APROVE which are third party software elements integrated into the program may fall under comparable restrictions by their respective licenses (refer to VI below). APROVE and its DOCUMENTATION are being licensed for non-commercial use only. Without executing an applicable commercial license with RWTH Aachen University, no part of APROVE may be sold, offered for sale, or made accessible via commercial services. However, APROVE may be made accessible to third parties on external computer networks for non-commercial use, provided that credit is given to RWTH Aachen University.
3. Disclaimer of Warranties
   You acknowledge and agree that use of APROVE is at your own risk and that the entire risk as to satisfactory quality, performance, accuracy and effort is with you. RWTH Aachen University has no obligation to provide technical support for APROVE and/or its DOCUMENTATION under this LICENSE. RWTH Aachen University is licensing APROVE and accompanying documentation "as is", with no express or implied warranties of any kind, including, but not limited to, any implied warranties of merchantability or fitness for any particular purpose or warranties against infringement of any proprietary rights of a third party.
4. Limitation of Liability
   RWTH Aachen University shall not be liable for any incidental, special, indirect or consequential damages whatsoever (including, but not limited to, damages for loss of profits, loss of data or business interruption) arising out of or related to your use of or inability to use APROVE. This limitation of liability does not apply to personal injuries, injuries to life or health or to damages caused willfully or by gross negligence attributable to RWTH Aachen University.
5. Transfer of Interest
   RWTH Aachen University may at any time assign or transfer all or part of its interest in any rights to APROVE and documentation, and to this license, to an affiliated or unaffiliated company or person.
6. Third Party Licenses
   APROVE contains third party software and icons protected by copyright laws and provided under the terms of the following other licenses, not to be infringed by this LICENSE:
   1. Under Lesser General Public License:
      1. getopt, http://www.urbanophile.com/arenn/hacking/download.html
      2. FindBugs, http://findbugs.sourceforge.net/
   2. Under Berkeley Software Distribution:
      1. ASM Bytecode Outline Plugin, http://andrei.gmxhome.de/bytecode/
      2. ASM, http://forge.ow2.org/projects/asm/
      3. Timing Framework, http://java.net/projects/timingframework (see also VI. d) 3.)
      4. ANTLR, http://www.antlr.org/
   3. Under Mozilla Public License:
      1. Saxon, http://saxon.sourceforge.net/
   4. Under Apache:
      1. Apache Commons, http://commons.apache.org/
      2. JDOM, http://www.jdom.org/
      3. Timing Framework, http://java.net/projects/timingframework
   5. Under Eclipse Public License:
      1. Eclipse icons, http://www.iconlet.com/
      2. Albireo, http://wiki.eclipse.org/Albireo_Project
         The Albireo source code is available for download at http://aprove.informatik.rwth-aachen.de/downloads/org.eclipse.albireo.core_0.0.3.v20081031-src.zip
   APROVE uses two third party software packages provided under LGPL license which have been altered:
   1. Sat4j, http://www.sat4j.org. The modified source code is available at http://aprove.informatik.rwth-aachen.de/downloads/sat4j.tar.gz
   2. ZGRViewer (part of ZVTM), http://zvtm.sourceforge.net. The modified source code is available at http://aprove.informatik.rwth-aachen.de/downloads/zgrviewer.tar.gz
7. Controlling Law and Severability The LICENSE will be governed by and construed in accordance with the laws of Germany and shall be subject to the exclusive jurisdiction of the German courts. If for any reason a court of competent jurisdiction finds any provision, or portion thereof, to be unenforceable, the remainder of the LICENSE shall continue in full force and effect.
8. Complete Agreement; Governing Language This LICENSE constitutes the entire agreement between the parties with respect to the use of APROVE licensed hereunder and supersedes all prior or contemporaneous understandings regarding such subject matter. No amendment to or modification of this LICENSE will be binding unless in writing and signed by RWTH Aachen University. Any translation of this LICENSE is done for local requirements only. In the event of a dispute between the English and any non-English versions, the English version shall prevail.