Here, you can download AProVE. By downloading AProVE, you accept the license agreement below.

If you encounter problems, want to perform experiments with AProVE, or would like to download older versions of AProVE, please contact us.

Supported Input Formats:

AProVE supports a number of input formats (detected by the file extension). The most important ones are


AProVE GUI as Eclipse plug-in:

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:

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.

AProVE Command-Line Version

Here you can find the latest releases of AProVE. If you are not sure which version you should use, please contact us.
All releases handle Java Bytecode, C, LLVM IR, Haskell 98, Prolog, and term rewriting fully automatically. It is able to output symbolic execution graphs and term rewrite systems (and related formalisms) for Java Bytecode, C, LLVM, Haskell, and Prolog programs.
To use it, install all dependencies (you do not need Eclipse and you only need Graphviz if you want to render symbolic execution graphs).

Installing dependencies:


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.