Automated Program Verification Environment
AProVE is a powerful system for automated termination, complexity, and safety proofs of several variations of term rewrite systems, as well as other formalisms including imperative, functional, and logic programs. You can use our web interface to test all capabilities, download AProVE and run it on your own machine, or integrate AProVE into the Eclipse IDE for convenient program verification during development.
Powerful Verification Capabilities
Term Rewrite Systems
Advanced analysis and verification for term rewrite systems including multiple variations.
Imperative Programs
Support for Java Bytecode and C/LLVM program analysis with relation to termination, complexity, and safety.
Integer Transition Systems
Analysis and verification for integer transition systems via the tools KoAT and LoAT.
Functional Programs
Verification for Haskell 98 programs with specialized analysis techniques for functional paradigms.
Probabilistic Programs
Verification of probabilistic programs that allow for probabilistic branches and flipping coins.
Logic Programs
Verification for Prolog programs with specialized analysis techniques for logical paradigms.
Awards & Achievements
Termination Competition
Multiple first places in the annual international competition of termination tools
Software Verification Competition
Strong results in the international competition on software verification
Kurt Gödel Medals
Two prestigious Kurt Gödel medals awarded at VSL 2014