Automated Program Verification Environment Web Interface

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 the International Competition on Software Verification. AProVE also won two Kurt Gödel medals at VSL 2014.

There are two possibilities to use AProVE:

• Web Interface: This web interface runs AProVE directly via the web on a virtual machine assigned eight cores of a Broadwell CPU. The web interface uses Docker containers to isolate the AProVE instances.
• Download: You can download the full version of AProVE.