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.
Product's homepage
Find us on Google+
