AProVE - EuroProofNet/ProgramVerification GitHub Wiki

Short description of AProVE.

What inputs are supported?

The following input formats are supported:

• Java Bytecode
• C
• LLVM IR
• Haskell
• Prolog
• Term Rewrite Systems
• Integer Transition Systems

For Term Rewrite Systems (TRSs), several variations of standard TRSs are supported as inputs:

• Rewriting with specific strategies (innermost rewriting, context-sensitive rewriting, outermost rewriting, (max-)parallel-innermost rewriting)
• Equational rewriting with associative or commutative operators
• Relative rewriting
• Integer term rewrite systems, both in a format following a RTA 2009 paper and in a format for top-level rewrite systems described in a JAR 2017 paper
• Probabilistic term rewrite systems

What properties can be verified?

Termination, non-termination, upper complexity bounds, lower complexity bounds, almost-sure termination.

What are the tool’s main techniques for the supported (input, property) pairs?

Dependency Pair framework, polynomial interpretations, ranking functions, ...

What external tools are used? (e.g., compilers, SMT solvers)

• SAT solvers: MiniSat, SAT4J
• SMT solvers: Z3, Yices, SMTInterpol
• Compilers: clang (for the step from C to LLVM IR)
• Termination backend: T2 (for Integer Transition Systems with restricted initial states), LoAT (for non-termination of Integer Transition Systems)
• Complexity analysis backends: KoAT (upper bounds for Integer Transition Systems), CoFloCo (upper bounds for Integer Transition Systems), LoAT (lower bounds for Integer Transition Systems)

What is the tool’s URL?

https://aprove.informatik.rwth-aachen.de/

AProVE can be used via a web interface or downloaded and run locally.

Example(s)

For an exhaustive example collection, consider the Termination Problem DataBase with thousands of example inputs for the supported languages for termination and complexity. Additionally, the web interface provides examples.

Other relevant information

A local installation of AProVE can be used both via the command line and as a plug-in for the Eclipse IDE.

References

The primary system description for AProVE is:

J. Giesl, C. Aschermann, M. Brockschmidt, F. Emmes, F. Frohn, C. Fuhs, J. Hensel, C. Otto, M. Plücker, P. Schneider-Kamp, T. Ströder, S. Swiderski, and R. Thiemann Analyzing Program Termination and Complexity Automatically with AProVE Journal of Automated Reasoning, 58(1):3-31, 2017. DOI