AProVE - 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. AProVE is open source. You can try it in the web interface without installing anything, pull the Docker image, run the jar from the command line, embed it in your Java application, or use it inside Eclipse.

Web Interface Get AProVE Eclipse Plugin

Powerful Verification Capabilities

⟶

Advanced analysis and verification for term rewrite systems including multiple variations.

{ }

Support for Java Bytecode and C/LLVM program analysis with relation to termination, complexity, and safety.

ℤ

Analysis and verification for integer transition systems via the tools KoAT and LoAT.

Verification for Haskell 98 programs with specialized analysis techniques for functional paradigms.

Verification of probabilistic programs that allow for probabilistic branches and flipping coins.

⊢

Verification for Prolog programs with specialized analysis techniques for logical paradigms.

Paste or upload an input and get the proof in your browser. No installation. Ideal for a single example or for teaching.

One docker pull gives you AProVE with all SAT and SMT solvers preconfigured. Ideal for reproducible benchmarking.

Run aprove.jar on a file from a terminal or a script and tailor the analysis via its flags.

Construct rewrite systems programmatically and run the analysis asynchronously from your own application.

Edit, analyze, and inspect the proof tree interactively inside the IDE while developing your program.

Multiple first places in the annual international competition of termination tools

Two prestigious Kurt Gödel medals awarded at VSL 2014

Strong results in the international competition on software verification