AProVE

AProVE - Automated Program Verification Environment - is a powerful system designed for automated termination and innermost termination proofs of term rewrite systems (TRSs). Its capabilities extend beyond TRSs to include other formalisms such as logic programs (Prolog), functional programs (Haskell 98), conditional TRSs, TRSs modulo AC, context-sensitive TRSs, and more.

One of AProVE's strengths is its success in the annual International Competition of Termination Tools, where it was the most powerful tool for termination of TRSs in 2004, 2005, 2006, and 2007. This program is based on the dependency pair framework, offering a wide variety of different termination proof techniques that can be freely configured and combined by the user via a graphical user interface.

Furthermore, AProVE also provides a "fully automatic" mode, in which suitable termination techniques are applied in a certain fixed order that often leads to successful results in practice. This program is ideal for users seeking a comprehensive, powerful, and easy-to-use system for automated termination and innermost termination proofs.

System requirements for AProVE include a Java runtime system version 1.5 or newer. Installation is simple - the user can untar the archive and start AProVE via the java -jar AProVE.jar command. If the program crashes due to insufficient memory, users can start AProVE with the -XmxNm option. This allows Java and AProVE to use N megabytes of memory. For example, the command java -Xmx400m -jar AProVE.jar starts AProVE with a memory limit of 400 megabytes, whereas without this option, the default limit is utilized, which is quite low.