AProVE 07

AProVE is a system for automated termination and innermost termination proofs of term rewrite systems (TRSs).
AProVE - Automated Program Verification Environment - is a system for automated termination and innermost termination proofs of term rewrite systems (TRSs). Moreover, AProVE also handles several other formalisms, e.g., logic programs (Prolog), functional programs (Haskell 98), conditional TRSs, TRSs modulo AC, context-sensitive TRSs, etc. The power of AProVE is demonstrated in the annual International Competition of Termination Tools, where AProVE was the most powerful tool for termination of TRSs in 2004, 2005, 2006, and 2007.

AProVE is based on the dependency pair framework and offers a wide variety of different termination proof techniques. These techniques can be freely configured and combined by the user via a graphical user interface. Moreover, AProVE also offers a "fully automatic" mode where suitable termination techniques are applied in a certain fixed order that often turns out to be successful in practice.

Requirements:

Java runtime system version 1.5 or newer



INSTALLATION:

Untar the archive.

Start AProVE with

java -jar AProVE.jar

If AProVE crashes because of not enough memory, you should start AProVE with the -XmxNm option which allows java and therefore AProVE to use N megabytes of memory. For example,

java -Xmx400m -jar AProVE.jar

starts AProVE with a memory limit of 400 megabytes. Without this option the default limit is used which is quite low.

last updated on:
March 15th, 2008, 5:22 GMT
price:
FREE!
developed by:
AProVE Team
homepage:
aprove.informatik.rwth-aachen.de
license type:
Other/Proprietary License
category:
ROOT \ Programming \ Debuggers

FREE!

In a hurry? Add it to your Download Basket!

user rating 20

3.1/5
 

0/5

Rate it!
2 Screenshots
AProVEAProVE

Add your review!

SUBMIT