Automated Program Verification Environment

AProVE is a system for automated termination and complexity proofs of term rewrite systems (TRSs) and several variations of TRSs. Moreover, AProVE also handles several other formalisms, e.g., imperative programs (Java Bytecode and C / LLVM), functional programs (Haskell 98), and logic programs (Prolog). The power of AProVE is demonstrated in the annual International Competition of Termination Tools and International Competition on Software Verification. AProVE also won two Kurt Gödel medals at VSL 2014 (report in German).

There are two possibilities to use AProVE:

• Web Interface: This web interface runs AProVE directly via the web on a parallel computer.
• Download: You can download the full version of AProVE.